🃏 Misc.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V8.Proofs.String.
Require TezosOfOCaml.Proto_alpha.Misc.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
Fixpoint loop (B : Set) (acc_value : list B) (n_value : int)
(xs : list B) {struct xs} : option (list B × list B) :=
if n_value ≤i 0
then Some (rev acc_value, xs)
else
match xs with
| [] ⇒ None
| x_value :: xs0 ⇒ loop B (x_value :: acc_value) (n_value -i 1) xs0
end.
Definition take' {a : Set} (n : int) (l : list a) : option (list a × list a) :=
loop a nil n l.
Lemma take_take'_eq : ∀ (a : Set) (n : int) (l : list a),
take' n l = Misc.take n l.
Proof.
intros a n l; reflexivity.
Qed.
Lemma take_cases_loop : ∀ {a : Set} (n : int) (l acc : list a),
0 ≤ n ≤ Pervasives.max_int →
match loop a acc n l with
| Some (l1, l2) ⇒
(rev acc ++ l)%list = (l1 ++ l2)%list ∧
∃ l1', l1 = (rev acc ++ l1')%list ∧ List.length l1' = n
| None ⇒ True
end.
Proof.
intros a n l; revert n.
induction l as [| a0 l IHl]; intros n acc H; simpl.
{ destruct n eqn:DN.
{ simpl. split. reflexivity.
∃ []; split; [rewrite app_nil_r|]; reflexivity. }
{ simpl. apply I. }
{ lia. } }
{ destruct n eqn:DN; [..|lia].
{ split; [reflexivity |];
∃ []; split; [rewrite app_nil_r|]; reflexivity. }
{ assert (G : (Z.pos p -i 1) ≥ 0 ). {
unfold "-i".
rewrite Pervasives.normalize_identity; lia. }
assert (0 ≤ Z.pos p -i 1 ≤ Pervasives.max_int). {
split. lia.
destruct H. unfold "-i".
rewrite Pervasives.normalize_identity; lia. }
specialize (IHl _ (a0 :: acc) H0).
destruct (loop a (a0 :: acc) (Z.pos p -i 1) l) eqn:H'.
destruct p0 eqn:P; destruct IHl; split;
rewrite List.rev_head_app_eq in H1; trivial.
destruct H2 as [l1' Hl1']; ∃ (a0::l1'); split.
rewrite List.rev_head_app_eq in Hl1'.
destruct Hl1'; trivial.
destruct Hl1'; simpl.
unfold "-i" in H3; unfold "+i".
rewrite Pervasives.normalize_identity; lia.
apply I. } }
Qed.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V8.Proofs.String.
Require TezosOfOCaml.Proto_alpha.Misc.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
Fixpoint loop (B : Set) (acc_value : list B) (n_value : int)
(xs : list B) {struct xs} : option (list B × list B) :=
if n_value ≤i 0
then Some (rev acc_value, xs)
else
match xs with
| [] ⇒ None
| x_value :: xs0 ⇒ loop B (x_value :: acc_value) (n_value -i 1) xs0
end.
Definition take' {a : Set} (n : int) (l : list a) : option (list a × list a) :=
loop a nil n l.
Lemma take_take'_eq : ∀ (a : Set) (n : int) (l : list a),
take' n l = Misc.take n l.
Proof.
intros a n l; reflexivity.
Qed.
Lemma take_cases_loop : ∀ {a : Set} (n : int) (l acc : list a),
0 ≤ n ≤ Pervasives.max_int →
match loop a acc n l with
| Some (l1, l2) ⇒
(rev acc ++ l)%list = (l1 ++ l2)%list ∧
∃ l1', l1 = (rev acc ++ l1')%list ∧ List.length l1' = n
| None ⇒ True
end.
Proof.
intros a n l; revert n.
induction l as [| a0 l IHl]; intros n acc H; simpl.
{ destruct n eqn:DN.
{ simpl. split. reflexivity.
∃ []; split; [rewrite app_nil_r|]; reflexivity. }
{ simpl. apply I. }
{ lia. } }
{ destruct n eqn:DN; [..|lia].
{ split; [reflexivity |];
∃ []; split; [rewrite app_nil_r|]; reflexivity. }
{ assert (G : (Z.pos p -i 1) ≥ 0 ). {
unfold "-i".
rewrite Pervasives.normalize_identity; lia. }
assert (0 ≤ Z.pos p -i 1 ≤ Pervasives.max_int). {
split. lia.
destruct H. unfold "-i".
rewrite Pervasives.normalize_identity; lia. }
specialize (IHl _ (a0 :: acc) H0).
destruct (loop a (a0 :: acc) (Z.pos p -i 1) l) eqn:H'.
destruct p0 eqn:P; destruct IHl; split;
rewrite List.rev_head_app_eq in H1; trivial.
destruct H2 as [l1' Hl1']; ∃ (a0::l1'); split.
rewrite List.rev_head_app_eq in Hl1'.
destruct Hl1'; trivial.
destruct Hl1'; simpl.
unfold "-i" in H3; unfold "+i".
rewrite Pervasives.normalize_identity; lia.
apply I. } }
Qed.
Main lemma: take_cases. In order to prove it we create auxillary
definition take' and prove that our take' is equal to original take.
take' unlike take, do not have loop inside, we brought it out,
so we could prove required statements, using induction.
Lemma take_cases_loop - an auxiliary lemma, it is more general statement,
which says that required statements (List.length l1 = n /\ l = (l1 ++ l2)%list)
actually True for any initial accumulator, not just for the empty list.
But why we needed this generalization? This trick was shown by Henk Barendregt
in his Lambda Calculi with Types: extremely complicated and detailed statements
can be proved if we do as much generalization as possible.
There is one more interesting tecnique used in take_cases_loop's proof:
eyeballing at function List.rev_head_app_eq shows us that it was proved
with function rev_append_last. And rev_append_last on it's turn was
proved with double application of induction hypothesis. Two applications,
one by one!
Lemma take_cases proved.
Lemma take_cases {a : Set} (n : int) (l : list a)
: 0 ≤ n ≤ Pervasives.max_int → match Misc.take n l with
| Some (l1, l2) ⇒ List.length l1 = n ∧ l = (l1 ++ l2)%list
| None ⇒ True
end.
Proof.
rewrite <- take_take'_eq.
it is safe to rewrite, we proved equality!
destruct (take' n l) eqn:E.
destruct p eqn:G; unfold take' in E; intro H;
specialize (take_cases_loop n l nil H) as Y;
rewrite E in Y;
destruct Y; split;
destruct H1 as [l1' [H1' H1'']]; simpl in *; subst; trivial.
intro N; apply I.
Qed.
Lemma loop_of_length_app {a : Set} (acc l1 l2 : list a) :
List.z_length l1 + 1 ≤ Pervasives.max_int →
loop a acc (List.z_length l1) (l1 ++ l2) = Some (((rev acc) ++ l1)%list, l2).
Proof.
revert acc l2.
induction l1 as [| x l1 IHl1]; intros acc l2 H; simpl.
{ rewrite app_nil_r;
destruct l2; reflexivity. }
{ rewrite List.z_length_plus_one_minus_one, IHl1; [|simpl in H; lia..].
unfold "<=i"; simpl.
replace (List.z_length l1 + 1 <=? 0) with false
by (symmetry; apply List.z_length_plus_one).
rewrite List.rev_head_app_eq; reflexivity. }
Qed.
destruct p eqn:G; unfold take' in E; intro H;
specialize (take_cases_loop n l nil H) as Y;
rewrite E in Y;
destruct Y; split;
destruct H1 as [l1' [H1' H1'']]; simpl in *; subst; trivial.
intro N; apply I.
Qed.
Lemma loop_of_length_app {a : Set} (acc l1 l2 : list a) :
List.z_length l1 + 1 ≤ Pervasives.max_int →
loop a acc (List.z_length l1) (l1 ++ l2) = Some (((rev acc) ++ l1)%list, l2).
Proof.
revert acc l2.
induction l1 as [| x l1 IHl1]; intros acc l2 H; simpl.
{ rewrite app_nil_r;
destruct l2; reflexivity. }
{ rewrite List.z_length_plus_one_minus_one, IHl1; [|simpl in H; lia..].
unfold "<=i"; simpl.
replace (List.z_length l1 + 1 <=? 0) with false
by (symmetry; apply List.z_length_plus_one).
rewrite List.rev_head_app_eq; reflexivity. }
Qed.
Main lemma: take_of_length_app. In order to prove it we create auxillary
definitions take' and z_length. We also prove that take' equals to original take.
and z_length equals to length.
It is easier to prove statemens about take' because it's loop is outside,
and we can work with loop directly. As for z_length - it uses integers instead
of modular arithmetic, and it is much easier to prove statements for
integers.
Lemma take_of_length_app {a : Set} (l1 l2 : list a) :
List.z_length l1 + 1 ≤ Pervasives.max_int →
Misc.take (List.length l1) (l1 ++ l2) = Some (l1, l2).
Proof.
intro H;
rewrite <- take_take'_eq, List.length_z_length_eq; [| lia].
unfold take'; rewrite loop_of_length_app; [reflexivity | lia].
Qed.
Lemma Zplus_0 : ∀ n, Pervasives.Int.Valid.t n → 0 +i n = n.
Proof.
unfold "+i"; intros n; simpl; intro Valid;
apply Pervasives.normalize_identity;
trivial.
Qed.
Lemma one_valid : Pervasives.Int.Valid.t 1.
Proof. lia. Qed.
Lemma length_op_caret_cons: ∀ s1 s2 a,
(String.length (String.String a (op_caret s1 s2))) ≥
String.length (String.String a s1).
Proof.
induction s1 as [|a0 s1 IHs1]; intros s2 a; simpl.
{ rewrite 2 String.string_length_cons.
rewrite String.string_length_empty; simpl.
assert (H : String.length s2 ≥ 0) by
apply String.length_any_string_not_zero; lia. }
{ rewrite !(String.string_length_cons a _).
assert (H : ∀ a b, (a ≥ b) →
((a + 1) ≥ (b + 1))) by
(intros a' b' H'; lia).
apply H with
(a:=(String.length (String.String a (op_caret s1 s2))))
(b:=(String.length (String.String a s1))) in IHs1.
trivial. }
Qed.
Lemma string_app_length : ∀ s1 s2, String.length (op_caret s1 s2) =
(String.length s1 + String.length s2)%Z.
Proof.
induction s1; intro s2.
{ rewrite String.length_empty_string; unfold op_caret; reflexivity. }
{ simpl; rewrite String.string_length_cons, IHs1.
assert (H' : String.length s2 ≥ 0) by
apply String.length_any_string_not_zero.
destruct s2.
{ simpl; rewrite String.length_empty_string,
String.string_length_cons; lia. }
{ rewrite String.string_length_cons.
assert (H : String.length (String.String a0 s2) > 0). {
rewrite String.string_length_cons. rewrite String.string_length_cons in H'.
assert (H'' : String.length s2 ≥ 0) by
apply String.length_any_string_not_zero; lia. }
destruct (String.length s2 + 1)%Z eqn:E;
rewrite String.string_length_cons in H; try lia.
unfold String.length, CoqOfOCaml.String.length; admit. }}
Admitted.
Lemma length_op_caret_geb : ∀ s1 s2,
(String.length (op_caret s1 s2) ≥ String.length s1).
Proof.
intros s1 s2.
rewrite string_app_length.
assert (H' : String.length s2 ≥ 0) by
apply String.length_any_string_not_zero; lia.
Qed.
Lemma length_op_caret_second_string : ∀ s1 s2,
Pervasives.Int.Valid.t (String.length s2) →
(String.length (op_caret s1 s2) -i String.length s1) = String.length s2.
Proof.
intros s1 s2 V;
rewrite string_app_length;
unfold "-i".
assert (H : (String.length s1 + String.length s2 - String.length s1) =
String.length s2) by lia.
rewrite H.
assert (H' : normalize_int (String.length s2) = String.length s2);
apply Pervasives.normalize_identity; trivial; rewrite H'; reflexivity.
Qed.
Lemma length_op_caret_second_string_cons : ∀ s1 s2 a,
Pervasives.Int.Valid.t (String.length s2) →
(String.length (String.String a (op_caret s1 s2)) -i
String.length (String.String a s1)) = String.length s2.
Proof.
intros s1 s2 a V.
rewrite !String.string_length_cons, string_app_length;
unfold "-i".
assert (H : (String.length s1 + String.length s2 + 1 -
(String.length s1 + 1)) =
String.length s2) by lia.
rewrite H;
assert (H' : normalize_int (String.length s2) = String.length s2).
{ apply Pervasives.normalize_identity. trivial. }
rewrite H'; reflexivity.
Qed.
Lemma minus_zero : ∀ n, Pervasives.Int.Valid.t n → n -i 0 = n.
Proof.
intro n; unfold "-i";
rewrite <- Zminus_0_l_reverse;
apply Pervasives.normalize_identity.
Qed.
Main lemma: remove_prefix_eq. It's proving is pretty staight-forward:
we do induction on first string s1, we decompose remove_prefix's definition
and use 14 auxiliary lemmas in total, in order to prove base case (s = ☐) and
rewrite induction hypothesis.
Lemma remove_prefix_eq s1 s2 :
Pervasives.Int.Valid.t (String.length s2) →
Misc.remove_prefix s1 (Pervasives.op_caret s1 s2) = Some s2.
Proof.
intro H.
induction s1; simpl; unfold Misc.remove_prefix; simpl.
{ rewrite String.length_empty_string.
assert (String.length s2 ≥ 0) by
apply String.length_any_string_not_zero.
unfold ">=i"; simpl.
apply Reflect.Z_geb_ge in H0; rewrite H0; simpl;
rewrite String.string_sub_zero; simpl;
rewrite minus_zero, String.string_sub_length.
reflexivity. trivial. }
{ assert (G'' : ∀ s1 s2 a,
is_true ((String.length (String.String a (op_caret s1 s2))) >=?
String.length (String.String a s1))).
{ intros s0 s3 a0.
apply Reflect.Z_geb_ge; apply length_op_caret_cons. }
rewrite G''; simpl.
replace (String.String a (op_caret s1 s2))
with (op_caret (String.String a s1) s2) by reflexivity.
rewrite String.compare_string_sub. simpl.
rewrite length_op_caret_second_string_cons,
<- IHs1; [| trivial].
unfold Misc.remove_prefix;
simpl.
assert (G : is_true (String.length (op_caret s1 s2) >=? String.length s1)) by
(rewrite Reflect.Z_geb_ge; apply length_op_caret_geb).
unfold ">=i"; simpl.
rewrite G; simpl.
rewrite String.string_compare_string_sub,
length_op_caret_second_string, String.sub_op_caret_cons_eq.
reflexivity. trivial. }
Qed.
Main lemma: remove_elem_from_list. In order to prove it we create
auxillary definition z_length and prove that our z_length equals to length.
Why do we need z_length? With it we do not have to work with modular arithmetic,
we work with integers and it is much easier to prove something on integers.
Lemma remove_elem_from_list {a : Set} (l1 l2 : list a) :
List.z_length l1 + 1 ≤ Pervasives.max_int →
Misc.remove_elem_from_list (List.length l1) (l1 ++ l2) = l2.
Proof.
intro H; rewrite List.length_z_length_eq;
revert l2; induction l1 as [| x l1 IHl1];
try (simpl in *; lia); simpl; intro l2.
{ unfold Misc.remove_elem_from_list.
destruct l2; auto; reflexivity. }
{ assert (H' : List.z_length l1 + 1 <=? 0 = false). {
rewrite Z.leb_gt.
assert (G' : 0 ≤ List.z_length l1) by apply List.Z_le_z_length.
lia. }
unfold "<=i"; simpl.
rewrite H'.
assert (G : (List.z_length l1 + 1)%Z -i 1 = List.z_length l1). {
unfold "-i"; rewrite Pervasives.normalize_identity.
lia. simpl in *; lia. }
rewrite G. rewrite IHl1; auto.
simpl in H; lia. }
Qed.