🍃 List.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Coq.Sorting.Sorted.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V7.Proofs.Utils.
Module Int_length.
Require Import CoqOfOCaml.Settings.
Require Coq.Sorting.Sorted.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V7.Proofs.Utils.
Module Int_length.
Lists whose length fits in an OCaml's [int]. This condition is required
for all operations involving [length] or [nth] primitives.
Definition t {a : Set} (l : list a) : Prop :=
Pervasives.Int.Valid.t (Z.of_nat (Lists.List.length l)).
#[global] Hint Unfold t : tezos_z.
End Int_length.
Pervasives.Int.Valid.t (Z.of_nat (Lists.List.length l)).
#[global] Hint Unfold t : tezos_z.
End Int_length.
The [length] operator in [int] behaves as the length in [nat].
Lemma length_eq {a : Set} (l : list a) :
List.length l = Pervasives.normalize_int (Z.of_nat (Lists.List.length l)).
Proof.
induction l; simpl; lia.
Qed.
List.length l = Pervasives.normalize_int (Z.of_nat (Lists.List.length l)).
Proof.
induction l; simpl; lia.
Qed.
The [nth] element in a list concatenation.
Lemma nth_app_eq {a : Set} (l1 l2 : list a) :
Int_length.t l1 →
List.nth (l1 ++ l2) (List.length l1) = List.hd l2.
Proof.
unfold Int_length.t; intros; induction l1; simpl in ×.
{ destruct l2; reflexivity. }
{ rewrite length_eq in ×.
rewrite Pervasives.normalize_identity in × by lia.
unfold "+i".
rewrite Pervasives.normalize_identity by lia.
destruct (_ + _)%Z eqn:H_eq; [lia | | lia].
rewrite <- H_eq.
rewrite <- IHl1 by lia.
f_equal; lia.
}
Qed.
Lemma length_destruct {a : Set} (x : a) (l : list a) :
List.length (x :: l) = List.length l +i 1.
Proof.
induction l; simpl; lia.
Qed.
Lemma length_is_valid {a : Set} (l : list a) :
Pervasives.Int.Valid.t (List.length l).
Proof.
induction l; simpl; lia.
Qed.
Fixpoint length_app_sum {a : Set} (l1 l2 : list a)
: List.length (l1 ++ l2) =
List.length l1 +i List.length l2.
assert (H_l1l2 := length_is_valid (l1 ++ l2)).
destruct l1; simpl.
{ now rewrite Pervasives.normalize_identity. }
{ rewrite length_app_sum.
lia.
}
Qed.
Int_length.t l1 →
List.nth (l1 ++ l2) (List.length l1) = List.hd l2.
Proof.
unfold Int_length.t; intros; induction l1; simpl in ×.
{ destruct l2; reflexivity. }
{ rewrite length_eq in ×.
rewrite Pervasives.normalize_identity in × by lia.
unfold "+i".
rewrite Pervasives.normalize_identity by lia.
destruct (_ + _)%Z eqn:H_eq; [lia | | lia].
rewrite <- H_eq.
rewrite <- IHl1 by lia.
f_equal; lia.
}
Qed.
Lemma length_destruct {a : Set} (x : a) (l : list a) :
List.length (x :: l) = List.length l +i 1.
Proof.
induction l; simpl; lia.
Qed.
Lemma length_is_valid {a : Set} (l : list a) :
Pervasives.Int.Valid.t (List.length l).
Proof.
induction l; simpl; lia.
Qed.
Fixpoint length_app_sum {a : Set} (l1 l2 : list a)
: List.length (l1 ++ l2) =
List.length l1 +i List.length l2.
assert (H_l1l2 := length_is_valid (l1 ++ l2)).
destruct l1; simpl.
{ now rewrite Pervasives.normalize_identity. }
{ rewrite length_app_sum.
lia.
}
Qed.
The [reverse] operation preserves the [length] of a list.
Lemma length_rev_eq {a : Set} (l : list a) :
List.length (List.rev l) = List.length l.
Proof.
induction l; simpl; [reflexivity|].
unfold List.rev, Lists.List.rev'; simpl.
rewrite List.rev_append_rev, List.rev_alt.
rewrite length_app_sum.
now rewrite <- IHl.
Qed.
Fixpoint mem_eq_dec {a : Set} {eq_dec : a → a → bool}
(H_eq_dec : ∀ x y, eq_dec x y = true → x = y) (v : a) (l : list a)
: List.mem eq_dec v l = true →
List.In v l.
destruct l; simpl; [congruence|].
destruct (eq_dec _ _) eqn:H; simpl; [left | right].
{ symmetry.
now apply H_eq_dec.
}
{ now apply (mem_eq_dec _ eq_dec). }
Qed.
Definition in_list_string (s : string) (list : list string) : bool :=
List.mem String.eqb s list.
Fixpoint all_distinct_strings (l : list string) : bool :=
match l with
| [] ⇒ true
| h :: tl ⇒
if in_list_string h tl then
false
else
all_distinct_strings tl
end.
Fixpoint find_map {a b : Set} (f : a → option b) (l : list a) : option b :=
match l with
| [] ⇒ None
| x :: l ⇒
match f x with
| None ⇒ find_map f l
| Some y ⇒ Some y
end
end.
List.length (List.rev l) = List.length l.
Proof.
induction l; simpl; [reflexivity|].
unfold List.rev, Lists.List.rev'; simpl.
rewrite List.rev_append_rev, List.rev_alt.
rewrite length_app_sum.
now rewrite <- IHl.
Qed.
Fixpoint mem_eq_dec {a : Set} {eq_dec : a → a → bool}
(H_eq_dec : ∀ x y, eq_dec x y = true → x = y) (v : a) (l : list a)
: List.mem eq_dec v l = true →
List.In v l.
destruct l; simpl; [congruence|].
destruct (eq_dec _ _) eqn:H; simpl; [left | right].
{ symmetry.
now apply H_eq_dec.
}
{ now apply (mem_eq_dec _ eq_dec). }
Qed.
Definition in_list_string (s : string) (list : list string) : bool :=
List.mem String.eqb s list.
Fixpoint all_distinct_strings (l : list string) : bool :=
match l with
| [] ⇒ true
| h :: tl ⇒
if in_list_string h tl then
false
else
all_distinct_strings tl
end.
Fixpoint find_map {a b : Set} (f : a → option b) (l : list a) : option b :=
match l with
| [] ⇒ None
| x :: l ⇒
match f x with
| None ⇒ find_map f l
| Some y ⇒ Some y
end
end.
[List.Forall] is the trivial case where the property is always true.
Fixpoint Forall_True {a : Set} {P : a → Prop} {l : list a}
: (∀ x, P x) → List.Forall P l.
intro; destruct l; constructor; trivial; now apply Forall_True.
Qed.
(* These lemmas are often useful, especially for data-encoding proofs. *)
#[global] Hint Resolve Forall_True Forall_impl : core.
Lemma nil_has_no_last : ∀ (a : Set), last_opt (nil : List.t a) = None.
reflexivity.
Qed.
Lemma tz_rev_append_rev {a : Set} : ∀ (l l' : list a),
CoqOfOCaml.List.rev_append l l' = (Lists.List.rev l ++ l')%list.
intro l; induction l; simpl; auto; intros.
rewrite <- app_assoc; firstorder.
Qed.
Lemma lst_lst : ∀ (a : Set) (l : list a) (x : a),
last_opt (l ++ [x])%list = Some x.
intros.
induction l; auto.
simpl; rewrite IHl.
destruct l; reflexivity.
Qed.
Lemma head_is_last_of_rev : ∀ (a : Set) (l : list a) (x : a),
List.last_opt (List.rev l) = List.hd l.
Proof.
unfold rev; unfold List.rev, Lists.List.rev'.
intros.
induction l; simpl; [reflexivity|].
rewrite List.rev_append_rev, List.rev_alt.
apply lst_lst.
Qed.
Lemma head_of_init : ∀ {a trace : Set} (f : int → a) (x : trace),
init_value x 1 f = Pervasives.Ok [f(0)].
intros.
unfold init_value.
reflexivity.
Qed.
Lemma in_map : ∀ {a b : Set} (f : a → b) (xs : list a) (x : a),
In x xs → In (f x) (List.map f xs).
induction xs; intros x Hin; destruct Hin.
- left; congruence.
- right; apply IHxs; auto.
Qed.
Lemma fold_right_f_eq {a b : Set} (f g : a → b → b) (l : list a) (acc : b) :
(∀ x acc, f x acc = g x acc) →
fold_right f l acc = fold_right g l acc.
Proof.
induction l; sfirstorder.
Qed.
Lemma fold_right_opt_map : ∀ {a b c : Set} (f : a → option b)
(g : b → c → c) (xs : list a) (z : c),
List.fold_right
(fun x acc ⇒
match f x with
| Some y ⇒ g y acc
| None ⇒ acc
end) xs z =
List.fold_right g (List.filter_map f xs) z.
induction xs; hauto lq: on.
Qed.
Lemma fold_right_opt_no_None : ∀ {a b c : Set} (f : a → option b)
(g : b → c → c) (xs : list a) (z z_t : c),
(∀ x, In x xs → ∃ y, f x = Some y) →
List.fold_right
(fun x acc ⇒
match f x with
| Some y ⇒ g y acc
| None ⇒ z_t
end) xs z =
List.fold_right g (List.filter_map f xs) z.
induction xs; qauto l: on.
Qed.
Lemma fold_right_cons_nil : ∀ {a : Set} (xs : list a),
List.fold_right cons xs [] = xs.
Proof.
induction xs; intros.
- reflexivity.
- simpl; congruence.
Qed.
Lemma In_to_In_fold_add : ∀ {a b c : Set}
(f : a → option b) (g : b → c) (add : b → list c → list c)
(xs : list a) (x : a) (y : b),
(∀ x xs, In (g x) (add x xs)) →
(∀ x y xs, In (g x) xs → In (g x) (add y xs)) →
In x xs → f x = Some y →
In (g y) (List.fold_right
(fun x' acc ⇒
match f x' with
| Some y' ⇒ add y' acc
| None ⇒ acc
end) xs []).
Proof.
induction xs; intros x y add_In1 add_In2 Hxxs Hfx;
destruct Hxxs; simpl.
- rewrite H, Hfx.
apply add_In1.
- destruct (f a0); [apply add_In2|idtac];
apply (IHxs x); assumption.
Qed.
Lemma In_fold_add_to_In : ∀ {a b c : Set}
(f : a → option b) (g : b → c) (add : b → list c → list c),
(∀ x x' xs, In (g x) (add x' xs) → x = x' ∨ In (g x) xs) →
(∀ x x' y, f x = Some y → f x' = Some y → x = x') →
∀ (xs : list a) (x : a) (y : b),
f x = Some y →
In (g y) (List.fold_right
(fun x' acc ⇒
match f x' with
| Some y' ⇒ add y' acc
| None ⇒ acc
end) xs []) → In x xs.
Proof.
induction xs; intros.
- exact H2.
- destruct (f a0) eqn:G.
+ simpl in H2.
rewrite G in H2.
destruct (H _ _ _ H2).
× rewrite H3 in H1; left.
eapply H0; eassumption.
× right; eapply IHxs; eassumption.
+ right; eapply IHxs; auto.
× exact H1.
× simpl in H2.
rewrite G in H2.
exact H2.
Qed.
: (∀ x, P x) → List.Forall P l.
intro; destruct l; constructor; trivial; now apply Forall_True.
Qed.
(* These lemmas are often useful, especially for data-encoding proofs. *)
#[global] Hint Resolve Forall_True Forall_impl : core.
Lemma nil_has_no_last : ∀ (a : Set), last_opt (nil : List.t a) = None.
reflexivity.
Qed.
Lemma tz_rev_append_rev {a : Set} : ∀ (l l' : list a),
CoqOfOCaml.List.rev_append l l' = (Lists.List.rev l ++ l')%list.
intro l; induction l; simpl; auto; intros.
rewrite <- app_assoc; firstorder.
Qed.
Lemma lst_lst : ∀ (a : Set) (l : list a) (x : a),
last_opt (l ++ [x])%list = Some x.
intros.
induction l; auto.
simpl; rewrite IHl.
destruct l; reflexivity.
Qed.
Lemma head_is_last_of_rev : ∀ (a : Set) (l : list a) (x : a),
List.last_opt (List.rev l) = List.hd l.
Proof.
unfold rev; unfold List.rev, Lists.List.rev'.
intros.
induction l; simpl; [reflexivity|].
rewrite List.rev_append_rev, List.rev_alt.
apply lst_lst.
Qed.
Lemma head_of_init : ∀ {a trace : Set} (f : int → a) (x : trace),
init_value x 1 f = Pervasives.Ok [f(0)].
intros.
unfold init_value.
reflexivity.
Qed.
Lemma in_map : ∀ {a b : Set} (f : a → b) (xs : list a) (x : a),
In x xs → In (f x) (List.map f xs).
induction xs; intros x Hin; destruct Hin.
- left; congruence.
- right; apply IHxs; auto.
Qed.
Lemma fold_right_f_eq {a b : Set} (f g : a → b → b) (l : list a) (acc : b) :
(∀ x acc, f x acc = g x acc) →
fold_right f l acc = fold_right g l acc.
Proof.
induction l; sfirstorder.
Qed.
Lemma fold_right_opt_map : ∀ {a b c : Set} (f : a → option b)
(g : b → c → c) (xs : list a) (z : c),
List.fold_right
(fun x acc ⇒
match f x with
| Some y ⇒ g y acc
| None ⇒ acc
end) xs z =
List.fold_right g (List.filter_map f xs) z.
induction xs; hauto lq: on.
Qed.
Lemma fold_right_opt_no_None : ∀ {a b c : Set} (f : a → option b)
(g : b → c → c) (xs : list a) (z z_t : c),
(∀ x, In x xs → ∃ y, f x = Some y) →
List.fold_right
(fun x acc ⇒
match f x with
| Some y ⇒ g y acc
| None ⇒ z_t
end) xs z =
List.fold_right g (List.filter_map f xs) z.
induction xs; qauto l: on.
Qed.
Lemma fold_right_cons_nil : ∀ {a : Set} (xs : list a),
List.fold_right cons xs [] = xs.
Proof.
induction xs; intros.
- reflexivity.
- simpl; congruence.
Qed.
Lemma In_to_In_fold_add : ∀ {a b c : Set}
(f : a → option b) (g : b → c) (add : b → list c → list c)
(xs : list a) (x : a) (y : b),
(∀ x xs, In (g x) (add x xs)) →
(∀ x y xs, In (g x) xs → In (g x) (add y xs)) →
In x xs → f x = Some y →
In (g y) (List.fold_right
(fun x' acc ⇒
match f x' with
| Some y' ⇒ add y' acc
| None ⇒ acc
end) xs []).
Proof.
induction xs; intros x y add_In1 add_In2 Hxxs Hfx;
destruct Hxxs; simpl.
- rewrite H, Hfx.
apply add_In1.
- destruct (f a0); [apply add_In2|idtac];
apply (IHxs x); assumption.
Qed.
Lemma In_fold_add_to_In : ∀ {a b c : Set}
(f : a → option b) (g : b → c) (add : b → list c → list c),
(∀ x x' xs, In (g x) (add x' xs) → x = x' ∨ In (g x) xs) →
(∀ x x' y, f x = Some y → f x' = Some y → x = x') →
∀ (xs : list a) (x : a) (y : b),
f x = Some y →
In (g y) (List.fold_right
(fun x' acc ⇒
match f x' with
| Some y' ⇒ add y' acc
| None ⇒ acc
end) xs []) → In x xs.
Proof.
induction xs; intros.
- exact H2.
- destruct (f a0) eqn:G.
+ simpl in H2.
rewrite G in H2.
destruct (H _ _ _ H2).
× rewrite H3 in H1; left.
eapply H0; eassumption.
× right; eapply IHxs; eassumption.
+ right; eapply IHxs; auto.
× exact H1.
× simpl in H2.
rewrite G in H2.
exact H2.
Qed.
The function [fold_left_e] is valid.
Lemma fold_left_e_is_valid {a b : Set} (P_a : a → Prop) (P_b : b → Prop)
(f : a → b → M? a) (acc : a) (l : list b) :
(∀ acc item,
P_a acc →
P_b item →
letP? acc := f acc item in
P_a acc
) →
P_a acc →
List.Forall P_b l →
letP? acc := List.fold_left_e f acc l in
P_a acc.
Proof.
intros H_f H_acc H_l.
revert acc H_acc.
induction l; simpl; [trivial|]; intros acc H_acc.
unfold List.fold_left_e in *; simpl.
inversion_clear H_l.
match goal with
| |- context[f ?x ?y] ⇒
pose proof (H_f x y)
end.
destruct f; simpl in ×.
{ apply IHl; tauto. }
{ match goal with
| |- context[List.fold_left ?f _ _] ⇒
assert (∀ err l,
List.fold_left f (Pervasives.Error err) l = Pervasives.Error err
)
end. {
now clear dependent l; induction l.
}
hauto lq: on.
}
Qed.
(f : a → b → M? a) (acc : a) (l : list b) :
(∀ acc item,
P_a acc →
P_b item →
letP? acc := f acc item in
P_a acc
) →
P_a acc →
List.Forall P_b l →
letP? acc := List.fold_left_e f acc l in
P_a acc.
Proof.
intros H_f H_acc H_l.
revert acc H_acc.
induction l; simpl; [trivial|]; intros acc H_acc.
unfold List.fold_left_e in *; simpl.
inversion_clear H_l.
match goal with
| |- context[f ?x ?y] ⇒
pose proof (H_f x y)
end.
destruct f; simpl in ×.
{ apply IHl; tauto. }
{ match goal with
| |- context[List.fold_left ?f _ _] ⇒
assert (∀ err l,
List.fold_left f (Pervasives.Error err) l = Pervasives.Error err
)
end. {
now clear dependent l; induction l.
}
hauto lq: on.
}
Qed.
When [fold_left_e] encounters an element yielding an error,
the entire fold yields that error
Lemma fold_left_e_short_circuit : ∀
{a b tr : Set} (f : a → b → Pervasives.result a tr)
x y t ys,
f x y = Pervasives.Error t →
List.fold_left_e f x (y :: ys) = Pervasives.Error t.
Proof.
intros.
unfold fold_left_e; simpl.
rewrite H.
induction ys; auto.
Qed.
{a b tr : Set} (f : a → b → Pervasives.result a tr)
x y t ys,
f x y = Pervasives.Error t →
List.fold_left_e f x (y :: ys) = Pervasives.Error t.
Proof.
intros.
unfold fold_left_e; simpl.
rewrite H.
induction ys; auto.
Qed.
If a function preserves a property, then folding with that function
preserves that property
Lemma fold_left_e_lemma {A B : Set}
(f : A → B → M? A)
(xs : list B) : ∀
(a1 a2 : A)
(P : A → Prop)
(fP : ∀ a1 a2 b, P a1 → f a1 b = Pervasives.Ok a2 → P a2),
fold_left_e f a1 xs = Pervasives.Ok a2 → P a1 → P a2.
Proof.
induction xs; intros a1 a2 P fP Hf.
{ inversion Hf; congruence. }
{ destruct (f a1 a) eqn:F.
{ unfold fold_left_e in ×.
intro.
simpl in Hf.
eapply IHxs; auto.
{ rewrite F in Hf; eauto. }
{ eapply fP; eauto. }
}
{ erewrite fold_left_e_short_circuit in Hf;
sauto.
}
}
Qed.
(f : A → B → M? A)
(xs : list B) : ∀
(a1 a2 : A)
(P : A → Prop)
(fP : ∀ a1 a2 b, P a1 → f a1 b = Pervasives.Ok a2 → P a2),
fold_left_e f a1 xs = Pervasives.Ok a2 → P a1 → P a2.
Proof.
induction xs; intros a1 a2 P fP Hf.
{ inversion Hf; congruence. }
{ destruct (f a1 a) eqn:F.
{ unfold fold_left_e in ×.
intro.
simpl in Hf.
eapply IHxs; auto.
{ rewrite F in Hf; eauto. }
{ eapply fP; eauto. }
}
{ erewrite fold_left_e_short_circuit in Hf;
sauto.
}
}
Qed.
When the list has a length in [int] then the [List.fold_left_i] operation
behaves as if its index was in [Z].
Lemma fold_left_i_in_int {a b : Set} f (acc : a) (l : list b) :
Int_length.t l →
List.fold_left_i f acc l =
snd (
fold_left
(fun '(index, acc) item ⇒
let acc := f index acc item in
((index + 1)%Z, acc)
)
(0, acc)
l
).
Proof.
intros.
unfold List.fold_left_i; f_equal; [hauto lq: on|].
match goal with
| |- List.fold_left ?f1 _ _ = List.fold_left ?f2 _ _ ⇒
assert (H_aux : ∀ l index acc,
0 ≤ index →
Pervasives.Int.Valid.t (index +Z Z.of_nat (Lists.List.length l)) →
List.fold_left f1 (index, acc) l = List.fold_left f2 (index, acc) l
)
end. {
clear acc l H.
induction l; simpl; intros; [reflexivity|].
replace (index +i 1) with (index +Z 1) by lia.
apply IHl; lia.
}
apply H_aux; lia.
Qed.
Lemma hd_Some_to_cons : ∀ {a : Set} (x : a) xs, hd xs = Some x →
∃ ys, xs = x :: ys.
Proof.
intros X x [|y ys] Hxs.
- discriminate.
- ∃ ys; auto.
inversion Hxs; reflexivity.
Qed.
Lemma rev_append_last : ∀ (a : Set) (l l' : list a),
CoqOfOCaml.List.rev_append l l' =
(CoqOfOCaml.List.rev_append l [] ++ l')%list.
Proof.
intros a l l'; revert l';
induction l as [|x l IHl]; intro l'; [reflexivity |];
simpl; rewrite IHl, (IHl [x]), <- app_assoc; reflexivity.
Qed.
Lemma rev_head_app_eq {a : Set} (acc l : list a) (x : a) :
(List.rev (x :: acc) ++ l)%list = (List.rev acc ++ x :: l)%list.
Proof.
intros; unfold List.rev, Lists.List.rev'; simpl.
rewrite List.rev_append_rev, List.rev_alt.
rewrite <- app_assoc; reflexivity.
Qed.
Lemma rev_app_eq {a : Set} (l : list a) (x : a) :
(List.rev (x :: l))%list = (List.rev l ++ [x])%list.
Proof.
specialize (rev_head_app_eq l [] x) as Hl.
rewrite app_nil_r in Hl; auto.
Qed.
Int_length.t l →
List.fold_left_i f acc l =
snd (
fold_left
(fun '(index, acc) item ⇒
let acc := f index acc item in
((index + 1)%Z, acc)
)
(0, acc)
l
).
Proof.
intros.
unfold List.fold_left_i; f_equal; [hauto lq: on|].
match goal with
| |- List.fold_left ?f1 _ _ = List.fold_left ?f2 _ _ ⇒
assert (H_aux : ∀ l index acc,
0 ≤ index →
Pervasives.Int.Valid.t (index +Z Z.of_nat (Lists.List.length l)) →
List.fold_left f1 (index, acc) l = List.fold_left f2 (index, acc) l
)
end. {
clear acc l H.
induction l; simpl; intros; [reflexivity|].
replace (index +i 1) with (index +Z 1) by lia.
apply IHl; lia.
}
apply H_aux; lia.
Qed.
Lemma hd_Some_to_cons : ∀ {a : Set} (x : a) xs, hd xs = Some x →
∃ ys, xs = x :: ys.
Proof.
intros X x [|y ys] Hxs.
- discriminate.
- ∃ ys; auto.
inversion Hxs; reflexivity.
Qed.
Lemma rev_append_last : ∀ (a : Set) (l l' : list a),
CoqOfOCaml.List.rev_append l l' =
(CoqOfOCaml.List.rev_append l [] ++ l')%list.
Proof.
intros a l l'; revert l';
induction l as [|x l IHl]; intro l'; [reflexivity |];
simpl; rewrite IHl, (IHl [x]), <- app_assoc; reflexivity.
Qed.
Lemma rev_head_app_eq {a : Set} (acc l : list a) (x : a) :
(List.rev (x :: acc) ++ l)%list = (List.rev acc ++ x :: l)%list.
Proof.
intros; unfold List.rev, Lists.List.rev'; simpl.
rewrite List.rev_append_rev, List.rev_alt.
rewrite <- app_assoc; reflexivity.
Qed.
Lemma rev_app_eq {a : Set} (l : list a) (x : a) :
(List.rev (x :: l))%list = (List.rev l ++ [x])%list.
Proof.
specialize (rev_head_app_eq l [] x) as Hl.
rewrite app_nil_r in Hl; auto.
Qed.
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.
Recomendation : when you face (length l) in the lemma to be proved,
just rewrite length with z_length by length_z_length_eq.
Fixpoint z_length {a : Set} (l : list a) {struct l} : Z.t :=
match l with
| [] ⇒ 0
| _ :: l' ⇒ ((z_length l') + 1)%Z
end.
Lemma Z_le_z_length {a : Set} (l : list a) : 0 ≤ z_length l.
Proof.
induction l; simpl; lia.
Qed.
Lemma z_length_plus_one : ∀ {a : Set} (l : list a),
((z_length l + 1)%Z ≤i 0) = false.
Proof.
intros a l; assert (0 ≤ z_length l) by apply Z_le_z_length; lia.
Qed.
Lemma length_z_length_eq : ∀ (a : Set) (l : list a),
z_length l ≤ Pervasives.max_int →
List.length l = z_length l.
Proof.
intros a l H.
induction l; simpl; trivial;
unfold "+i";
simpl in H.
assert (G : z_length l ≤ Pervasives.max_int) by lia.
apply IHl in G. rewrite G.
rewrite Pervasives.normalize_identity. reflexivity.
split. assert (G' : 0 ≤ z_length l) by apply Z_le_z_length.
lia. trivial.
Qed.
Lemma z_length_plus_one_minus_one : ∀ {a : Set} (l : list a),
z_length l ≤ Pervasives.max_int →
(z_length l + 1)%Z -i 1 = z_length l.
Proof.
intros a l H;
assert (G : 0 ≤ z_length l) by apply Z_le_z_length;
unfold "-i"; rewrite Pervasives.normalize_identity; lia.
Qed.
Lemma length_map {a b : Set} (f : a → b) (xs : list a) :
List.length (List.map f xs) = List.length xs.
induction xs.
- reflexivity.
- simpl.
repeat (rewrite length_cons).
congruence.
Qed.
The [equal] function over the lists is valid as long as its parameter [eqb]
is valid too.
Lemma equal_is_valid {a : Set} (domain : a → Prop) (eqb : a → a → bool)
(l1 l2 : list a) :
Compare.Equal.Valid.t domain eqb →
Compare.Equal.Valid.t (List.Forall domain) (List.equal eqb).
Proof.
unfold Compare.Equal.Valid.t.
intros H_eqb x y H_x H_y.
split; generalize y H_y; clear y H_y.
{ induction x; simpl; intros; destruct y; trivial; try discriminate.
sauto lq: on.
}
{ induction x; simpl; intros; destruct y; trivial; try discriminate.
match goal with
| H : _ |- _ ⇒ destruct (andb_prop _ _ H)
end.
sauto lq: on rew: off.
}
Qed.
Module Sorted.
Lemma filter_map {a b : Set}
(R_a : a → a → Prop) (R_b : b → b → Prop)
(Htr : ∀ x y z, R_a x y → R_a y z → R_a x z)
(f : a → option b) (l : list a) :
(∀ x1 x2,
match f x1, f x2 with
| Some y1, Some y2 ⇒ R_a x1 x2 → R_b y1 y2
| _, _ ⇒ True
end) →
Sorting.Sorted.Sorted R_a l →
Sorting.Sorted.Sorted R_b (List.filter_map f l).
Proof.
intro H.
induction l as [|x]; simpl; auto; intro Hl.
inversion_clear Hl.
specialize (IHl H0).
specialize (H x).
destruct (f x); auto.
induction l as [|y]; simpl; auto.
simpl in IHl.
inversion_clear H1.
inversion_clear H0.
specialize (H y).
destruct (f y); auto.
apply IHl0; auto.
clear IHl IHl0 H b0.
destruct l; auto.
inversion_clear H1; inversion_clear H3.
constructor.
apply Htr with y; auto.
Qed.
End Sorted.
Lemma filter_map_In_invert {A B : Set}
{f : A → M× B} {xs : list A} :
∀ {y}, In y (filter_map f xs) →
∃ x, In x xs ∧ f x = Some y.
Proof.
induction xs; hauto.
Qed.
Lemma filter_map_In {A B : Set}
{f : A → M× B} {xs : list A} :
∀ x y, In x xs → f x = Some y →
In y (filter_map f xs).
Proof.
induction xs; intros.
{ destruct H. }
{ simpl.
destruct H.
{ rewrite <- H in H0.
rewrite H0.
left; reflexivity.
}
{ destruct (f a).
{ right; eapply IHxs; eauto. }
{ eapply IHxs; eauto. }
}
}
Qed.
Lemma In_map_invert {A B : Set} {f : A → B}
{xs : list A} : ∀ {y}, In y (List.map f xs) →
∃ x, f x = y ∧ In x xs.
Proof.
induction xs; intros y Hin; destruct Hin.
{ ∃ a; hauto. }
{ destruct (IHxs y H) as [x [Hx1 Hx2]].
∃ x; hauto.
}
Qed.
(l1 l2 : list a) :
Compare.Equal.Valid.t domain eqb →
Compare.Equal.Valid.t (List.Forall domain) (List.equal eqb).
Proof.
unfold Compare.Equal.Valid.t.
intros H_eqb x y H_x H_y.
split; generalize y H_y; clear y H_y.
{ induction x; simpl; intros; destruct y; trivial; try discriminate.
sauto lq: on.
}
{ induction x; simpl; intros; destruct y; trivial; try discriminate.
match goal with
| H : _ |- _ ⇒ destruct (andb_prop _ _ H)
end.
sauto lq: on rew: off.
}
Qed.
Module Sorted.
Lemma filter_map {a b : Set}
(R_a : a → a → Prop) (R_b : b → b → Prop)
(Htr : ∀ x y z, R_a x y → R_a y z → R_a x z)
(f : a → option b) (l : list a) :
(∀ x1 x2,
match f x1, f x2 with
| Some y1, Some y2 ⇒ R_a x1 x2 → R_b y1 y2
| _, _ ⇒ True
end) →
Sorting.Sorted.Sorted R_a l →
Sorting.Sorted.Sorted R_b (List.filter_map f l).
Proof.
intro H.
induction l as [|x]; simpl; auto; intro Hl.
inversion_clear Hl.
specialize (IHl H0).
specialize (H x).
destruct (f x); auto.
induction l as [|y]; simpl; auto.
simpl in IHl.
inversion_clear H1.
inversion_clear H0.
specialize (H y).
destruct (f y); auto.
apply IHl0; auto.
clear IHl IHl0 H b0.
destruct l; auto.
inversion_clear H1; inversion_clear H3.
constructor.
apply Htr with y; auto.
Qed.
End Sorted.
Lemma filter_map_In_invert {A B : Set}
{f : A → M× B} {xs : list A} :
∀ {y}, In y (filter_map f xs) →
∃ x, In x xs ∧ f x = Some y.
Proof.
induction xs; hauto.
Qed.
Lemma filter_map_In {A B : Set}
{f : A → M× B} {xs : list A} :
∀ x y, In x xs → f x = Some y →
In y (filter_map f xs).
Proof.
induction xs; intros.
{ destruct H. }
{ simpl.
destruct H.
{ rewrite <- H in H0.
rewrite H0.
left; reflexivity.
}
{ destruct (f a).
{ right; eapply IHxs; eauto. }
{ eapply IHxs; eauto. }
}
}
Qed.
Lemma In_map_invert {A B : Set} {f : A → B}
{xs : list A} : ∀ {y}, In y (List.map f xs) →
∃ x, f x = y ∧ In x xs.
Proof.
induction xs; intros y Hin; destruct Hin.
{ ∃ a; hauto. }
{ destruct (IHxs y H) as [x [Hx1 Hx2]].
∃ x; hauto.
}
Qed.
[fold_left g] after [map f] is equivalent to [fold_left (g . f)]
Lemma fold_left_map_eq
{A B C: Set} (f1 : C → B → C) (f2 : A → B)
(init : C) (l : list A) :
fold_left f1 init (List.map f2 l) =
fold_left (fun acc x ⇒ f1 acc (f2 x)) init l.
Proof.
generalize init; clear init.
induction l; sfirstorder.
Qed.
{A B C: Set} (f1 : C → B → C) (f2 : A → B)
(init : C) (l : list A) :
fold_left f1 init (List.map f2 l) =
fold_left (fun acc x ⇒ f1 acc (f2 x)) init l.
Proof.
generalize init; clear init.
induction l; sfirstorder.
Qed.
The same as the above but for [fold_left_e]
Lemma fold_left_e_map_eq {A B C: Set}
(f1 : C → B → M? C) (f2 : A → B)
(init : C) (l : list A) :
fold_left_e f1 init (List.map f2 l) =
fold_left_e (fun acc x ⇒ f1 acc (f2 x)) init l.
Proof.
unfold fold_left_e.
now rewrite fold_left_map_eq.
Qed.
(f1 : C → B → M? C) (f2 : A → B)
(init : C) (l : list A) :
fold_left_e f1 init (List.map f2 l) =
fold_left_e (fun acc x ⇒ f1 acc (f2 x)) init l.
Proof.
unfold fold_left_e.
now rewrite fold_left_map_eq.
Qed.
Same as [fold_left_map_eq] but for [fold_left_es]
Lemma fold_left_es_map_eq {A B C: Set}
(f1 : C → B → M? C) (f2 : A → B)
(init : C) (l : list A) :
fold_left_es f1 init (List.map f2 l) =
fold_left_es (fun acc x ⇒ f1 acc (f2 x)) init l.
Proof.
apply fold_left_e_map_eq.
Qed.
(f1 : C → B → M? C) (f2 : A → B)
(init : C) (l : list A) :
fold_left_es f1 init (List.map f2 l) =
fold_left_es (fun acc x ⇒ f1 acc (f2 x)) init l.
Proof.
apply fold_left_e_map_eq.
Qed.
[nth_z] consumes a cons by decreasing its index by one, when
then index is positive.
Lemma nth_z_pos_cons {a : Set} (x : a) (l : list a) (i : int) :
0 < i → nth_z (x :: l) i = nth_z l (i - 1).
Proof.
intro Hi.
simpl.
destruct i; lia.
Qed.
0 < i → nth_z (x :: l) i = nth_z l (i - 1).
Proof.
intro Hi.
simpl.
destruct i; lia.
Qed.
[nth_z] always returns None when its index is negative.
Lemma nth_z_neg_None {a : Set} (l : list a) (p : Pos.t) :
nth_z l (BinInt.Z.neg p) = None.
Proof.
generalize p; clear p.
induction l; sauto.
Qed.
Lemma nth_mapi_Some_aux {a b : Set} (l : list a) : ∀ (acc : int)
(f : int → a → b) (i : int) (x : a),
List.nth l i = Some x →
List.nth (List.mapi_aux acc f l) i%Z = Some (f (acc + i)%Z x).
Proof.
unfold nth.
induction l; intros acc f i x Hi.
{ discriminate. }
{ simpl in Hi.
destruct i.
{ simpl.
repeat f_equal; [lia|congruence].
}
{ simpl mapi_aux.
rewrite nth_z_pos_cons; [|lia].
rewrite (IHl _ _ _ _ Hi).
do 2 f_equal; lia.
}
{ simpl in Hi.
rewrite nth_z_neg_None in Hi; discriminate.
}
}
Qed.
nth_z l (BinInt.Z.neg p) = None.
Proof.
generalize p; clear p.
induction l; sauto.
Qed.
Lemma nth_mapi_Some_aux {a b : Set} (l : list a) : ∀ (acc : int)
(f : int → a → b) (i : int) (x : a),
List.nth l i = Some x →
List.nth (List.mapi_aux acc f l) i%Z = Some (f (acc + i)%Z x).
Proof.
unfold nth.
induction l; intros acc f i x Hi.
{ discriminate. }
{ simpl in Hi.
destruct i.
{ simpl.
repeat f_equal; [lia|congruence].
}
{ simpl mapi_aux.
rewrite nth_z_pos_cons; [|lia].
rewrite (IHl _ _ _ _ Hi).
do 2 f_equal; lia.
}
{ simpl in Hi.
rewrite nth_z_neg_None in Hi; discriminate.
}
}
Qed.
If the [i]th element of a list [l] is [x], then the [i]th element of
[List.map f l] is [f i x]
Lemma nth_mapi_Some {a b : Set} (f : int → a → b) (l : list a)
(i : int) (x : a) :
List.nth l i = Some x → List.nth (List.mapi f l) i = Some (f i x).
Proof.
apply (@nth_mapi_Some_aux a b l 0).
Qed.
Lemma nth_mapi_Some_invert_aux {a b : Set} (l : list a) : ∀ (acc : int)
(f : int → a → b) (i : int) (y : b),
List.nth (List.mapi_aux acc f l) i%Z = Some y →
∃ x : a, List.nth l i = Some x ∧
f (acc + i)%Z x = y.
Proof.
unfold nth.
induction l as [|x l']; intros acc f i y Hi.
{ discriminate. }
{ simpl in Hi.
destruct i.
{ ∃ x; split.
{ reflexivity. }
{ rewrite Z.add_0_r; congruence. }
}
{ destruct (IHl' (acc + 1)%Z f (Z.pos p - 1) y Hi) as [x' [Hx'1 Hx'2]].
∃ x'; split; auto.
rewrite <- Hx'2; f_equal; lia.
}
{ simpl in Hi.
rewrite nth_z_neg_None in Hi; discriminate.
}
}
Qed.
(i : int) (x : a) :
List.nth l i = Some x → List.nth (List.mapi f l) i = Some (f i x).
Proof.
apply (@nth_mapi_Some_aux a b l 0).
Qed.
Lemma nth_mapi_Some_invert_aux {a b : Set} (l : list a) : ∀ (acc : int)
(f : int → a → b) (i : int) (y : b),
List.nth (List.mapi_aux acc f l) i%Z = Some y →
∃ x : a, List.nth l i = Some x ∧
f (acc + i)%Z x = y.
Proof.
unfold nth.
induction l as [|x l']; intros acc f i y Hi.
{ discriminate. }
{ simpl in Hi.
destruct i.
{ ∃ x; split.
{ reflexivity. }
{ rewrite Z.add_0_r; congruence. }
}
{ destruct (IHl' (acc + 1)%Z f (Z.pos p - 1) y Hi) as [x' [Hx'1 Hx'2]].
∃ x'; split; auto.
rewrite <- Hx'2; f_equal; lia.
}
{ simpl in Hi.
rewrite nth_z_neg_None in Hi; discriminate.
}
}
Qed.
If the [i]th element of [List.mapi f l] is [y], then
there is some [x] which is the [i]th element of [l] and
for which [f i x = y].
Lemma nth_mapi_Some_invert {a b : Set} (l : list a)
(f : int → a → b) (i : int) (y : b) :
List.nth (List.mapi f l) i%Z = Some y →
∃ x : a, List.nth l i = Some x ∧
f i x = y.
Proof.
apply (@nth_mapi_Some_invert_aux a b l 0).
Qed.
Lemma nth_mapi_None_aux {a b : Set} (l : list a) : ∀ (acc : int)
(f : int → a → b) (i : int),
List.nth l i = None →
List.nth (List.mapi_aux acc f l) i%Z = None.
Proof.
unfold nth.
induction l; intros acc f i Hi.
{ reflexivity. }
{ simpl in Hi.
destruct i; try discriminate.
{ simpl mapi_aux.
rewrite nth_z_pos_cons; [|lia].
apply IHl; auto.
}
{ apply nth_z_neg_None. }
}
Qed.
(f : int → a → b) (i : int) (y : b) :
List.nth (List.mapi f l) i%Z = Some y →
∃ x : a, List.nth l i = Some x ∧
f i x = y.
Proof.
apply (@nth_mapi_Some_invert_aux a b l 0).
Qed.
Lemma nth_mapi_None_aux {a b : Set} (l : list a) : ∀ (acc : int)
(f : int → a → b) (i : int),
List.nth l i = None →
List.nth (List.mapi_aux acc f l) i%Z = None.
Proof.
unfold nth.
induction l; intros acc f i Hi.
{ reflexivity. }
{ simpl in Hi.
destruct i; try discriminate.
{ simpl mapi_aux.
rewrite nth_z_pos_cons; [|lia].
apply IHl; auto.
}
{ apply nth_z_neg_None. }
}
Qed.
If [i] is out of the bounds of [l], then it is also out of the
bounds of [List.mapi f l].
Lemma nth_mapi_None {a b : Set} (f : int → a → b) (l : list a)
(i : int) :
List.nth l i = None → List.nth (List.mapi f l) i = None.
Proof.
apply (@nth_mapi_None_aux a b l 0).
Qed.
Lemma nth_mapi_None_invert_aux {a b : Set} (l : list a) : ∀ (acc : int)
(f : int → a → b) (i : int),
List.nth (List.mapi_aux acc f l) i%Z = None →
List.nth l i = None.
Proof.
unfold nth.
induction l; intros acc f i Hi.
{ reflexivity. }
{ simpl in Hi.
destruct i; try discriminate.
{ simpl mapi_aux.
rewrite nth_z_pos_cons; [|lia].
eapply IHl; eauto.
}
{ apply nth_z_neg_None. }
}
Qed.
(i : int) :
List.nth l i = None → List.nth (List.mapi f l) i = None.
Proof.
apply (@nth_mapi_None_aux a b l 0).
Qed.
Lemma nth_mapi_None_invert_aux {a b : Set} (l : list a) : ∀ (acc : int)
(f : int → a → b) (i : int),
List.nth (List.mapi_aux acc f l) i%Z = None →
List.nth l i = None.
Proof.
unfold nth.
induction l; intros acc f i Hi.
{ reflexivity. }
{ simpl in Hi.
destruct i; try discriminate.
{ simpl mapi_aux.
rewrite nth_z_pos_cons; [|lia].
eapply IHl; eauto.
}
{ apply nth_z_neg_None. }
}
Qed.
If [i] is out of the bounds of [List.mapi f l], then it is also out
of the bounds of [l].
Lemma nth_mapi_None_invert {a b : Set} (f : int → a → b) (l : list a)
(i : int) :
List.nth (List.mapi f l) i = None →
List.nth l i = None.
Proof.
apply (@nth_mapi_None_invert_aux a b l 0).
Qed.
(i : int) :
List.nth (List.mapi f l) i = None →
List.nth l i = None.
Proof.
apply (@nth_mapi_None_invert_aux a b l 0).
Qed.
CoqOfOcaml [fold_right] is equivalent to Coq [fold_right]
Lemma fold_right_eq {A B : Set}
(f : A → B → B) l acc :
fold_right f l acc = Coq.Lists.List.fold_right f acc l.
Proof.
induction l; sfirstorder.
Qed.
(f : A → B → B) l acc :
fold_right f l acc = Coq.Lists.List.fold_right f acc l.
Proof.
induction l; sfirstorder.
Qed.
Convert a fold right to a map
Lemma fold_right_to_map_eq {A B : Set} (f : A → B) l :
Lists.List.fold_right (fun x acc ⇒ (f x) :: acc) nil l =
Lists.List.map f l.
Proof.
induction l; sfirstorder.
Qed.
Lists.List.fold_right (fun x acc ⇒ (f x) :: acc) nil l =
Lists.List.map f l.
Proof.
induction l; sfirstorder.
Qed.
Applying a function on a reversed list and then folding right
over it is the same that applying that same function inside
the fold function
Lemma fold_right_rev_map_eq {a b c : Set} (f : b → c → c)
(g : a → b) (l : list a) (acc : c) :
Lists.List.fold_right f acc
(Lists.List.rev (Lists.List.map g l)) =
Lists.List.fold_right (fun x acc ⇒ f (g x) acc) acc
(Lists.List.rev l).
Proof.
rewrite <- Coq.Lists.List.map_rev.
induction (Lists.List.rev l); sfirstorder.
Qed.
(g : a → b) (l : list a) (acc : c) :
Lists.List.fold_right f acc
(Lists.List.rev (Lists.List.map g l)) =
Lists.List.fold_right (fun x acc ⇒ f (g x) acc) acc
(Lists.List.rev l).
Proof.
rewrite <- Coq.Lists.List.map_rev.
induction (Lists.List.rev l); sfirstorder.
Qed.
CoqOfOcaml [rev] is equivalent to Coq [rev]
Lemma rev_eq {A : Set} (l : list A) :
rev l = Coq.Lists.List.rev l.
Proof.
unfold rev, rev'.
now erewrite rev_alt.
Qed.
rev l = Coq.Lists.List.rev l.
Proof.
unfold rev, rev'.
now erewrite rev_alt.
Qed.
[fold_left] is equivalent to [fold_right] on the reversed list
Lemma fold_left_rev_right_eq {A B : Set}
(f : A → B → A)
(l : list B) (acc : A) :
fold_left f acc l = fold_right (fun x acc ⇒ f acc x) (rev l) acc.
Proof.
unfold fold_left. rewrite fold_right_eq.
rewrite <- Coq.Lists.List.fold_left_rev_right.
rewrite rev_eq. induction l; sfirstorder.
Qed.
(f : A → B → A)
(l : list B) (acc : A) :
fold_left f acc l = fold_right (fun x acc ⇒ f acc x) (rev l) acc.
Proof.
unfold fold_left. rewrite fold_right_eq.
rewrite <- Coq.Lists.List.fold_left_rev_right.
rewrite rev_eq. induction l; sfirstorder.
Qed.
Coq [fold_left] and CoqOfOCaml [fold_left] are interchangeable
Lemma fold_left_eq {a b : Set} (f : b → a → b) acc l :
Lists.List.fold_left f l acc = fold_left f acc l.
Proof.
rewrite <- Lists.List.fold_left_rev_right,
fold_left_rev_right_eq,
rev_eq,
fold_right_eq;
induction l; sfirstorder.
Qed.
Lists.List.fold_left f l acc = fold_left f acc l.
Proof.
rewrite <- Lists.List.fold_left_rev_right,
fold_left_rev_right_eq,
rev_eq,
fold_right_eq;
induction l; sfirstorder.
Qed.
[fold_right f (map g l)] is the same as [fold_right (fun x acc => (f (g x) acc)) l acc]
Lemma fold_right_map_eq {A B C : Set} (f : B → C → C) (l : list A) (acc : C)
(g : A → B) :
fold_right f (List.map g l) acc =
fold_right (fun x acc ⇒ (f (g x) acc)) l acc.
Proof.
induction l; sfirstorder.
Qed.
(g : A → B) :
fold_right f (List.map g l) acc =
fold_right (fun x acc ⇒ (f (g x) acc)) l acc.
Proof.
induction l; sfirstorder.
Qed.
Apply [f] to each element of a list and reverse it is
the same of reverse it and then apply [f].
Lemma rev_map_eq {a b : Set} (f : a → b) l :
List.rev (List.map f l) = List.map f (List.rev l).
Proof.
induction l; auto; simpl.
repeat rewrite rev_app_eq; rewrite IHl.
unfold List.map; rewrite map_app; auto.
Qed.
List.rev (List.map f l) = List.map f (List.rev l).
Proof.
induction l; auto; simpl.
repeat rewrite rev_app_eq; rewrite IHl.
unfold List.map; rewrite map_app; auto.
Qed.
[rev] preverves [P] in the list [l]
Lemma Forall_P_rev {a : Set} P (l : list a) :
Forall P l →
Forall P (rev l).
Proof.
induction l; simpl; auto.
inversion_clear 1.
rewrite rev_app_eq.
apply Forall_app; split; auto.
Qed.
Forall P l →
Forall P (rev l).
Proof.
induction l; simpl; auto.
inversion_clear 1.
rewrite rev_app_eq.
apply Forall_app; split; auto.
Qed.
If [P] holds for all elements in [x :: l] it holds for [l]
Lemma Forall_cons {a : Set} P x (l : list a) :
Forall P (x :: l) →
Forall P l.
Proof.
sauto lq: on dep: on.
Qed.
Forall P (x :: l) →
Forall P l.
Proof.
sauto lq: on dep: on.
Qed.
If [P] holds forall elements in [x :: l] it holds for [x]
Lemma Forall_head {a : Set} P x (l : list a) :
Forall P (x :: l) →
P x.
Proof.
sauto lq: on.
Qed.
(* if [rev l] is empty, then [l] also is *)
Lemma empty_rev_empty : ∀ {A : Set} (l : list A), rev l = [] → l = [].
Proof.
intros A l H. destruct l.
{ reflexivity. }
{ rewrite List.rev_eq in H.
apply f_equal with (A := list A) (f:= @Lists.List.rev A) in H.
rewrite rev_involutive in H. inversion H.
}
Qed.
Forall P (x :: l) →
P x.
Proof.
sauto lq: on.
Qed.
(* if [rev l] is empty, then [l] also is *)
Lemma empty_rev_empty : ∀ {A : Set} (l : list A), rev l = [] → l = [].
Proof.
intros A l H. destruct l.
{ reflexivity. }
{ rewrite List.rev_eq in H.
apply f_equal with (A := list A) (f:= @Lists.List.rev A) in H.
rewrite rev_involutive in H. inversion H.
}
Qed.
If the 2nd parameter of [rev_append] is not empty, then neither is its
output
Lemma rev_append_not_empty2 : ∀ {A : Set} (l1 l2 : list A), l2 ≠ []
→ Lists.List.rev_append l1 l2 ≠ [].
Proof.
induction l1 as [ | a1 tl1 H_tl1] ; intros l2 H_l2.
{ assumption. }
{ simpl. apply H_tl1. easy. }
Qed.
Lemma same_last_element_rev_append_aux :
∀ {A : Set} n (a : A) l1 l2 l, Lists.List.length l = n →
Coq.Lists.List.hd_error (Lists.List.rev_append l (a :: l1) )
= Coq.Lists.List.hd_error (Lists.List.rev_append l (a :: l2)).
Proof.
intro A.
induction n as [ | n0 Hn0].
{ intros a l1 l2 l H_len.
assert (l = []) by (destruct l as [ | a' l'];
[ reflexivity | inversion H_len]) .
rewrite H. reflexivity. }
{ intros a l1 l2 l H_len. destruct l as [ | a' l'].
{ reflexivity. }
{ simpl. inversion H_len. apply Hn0. assumption. }}
Qed.
→ Lists.List.rev_append l1 l2 ≠ [].
Proof.
induction l1 as [ | a1 tl1 H_tl1] ; intros l2 H_l2.
{ assumption. }
{ simpl. apply H_tl1. easy. }
Qed.
Lemma same_last_element_rev_append_aux :
∀ {A : Set} n (a : A) l1 l2 l, Lists.List.length l = n →
Coq.Lists.List.hd_error (Lists.List.rev_append l (a :: l1) )
= Coq.Lists.List.hd_error (Lists.List.rev_append l (a :: l2)).
Proof.
intro A.
induction n as [ | n0 Hn0].
{ intros a l1 l2 l H_len.
assert (l = []) by (destruct l as [ | a' l'];
[ reflexivity | inversion H_len]) .
rewrite H. reflexivity. }
{ intros a l1 l2 l H_len. destruct l as [ | a' l'].
{ reflexivity. }
{ simpl. inversion H_len. apply Hn0. assumption. }}
Qed.
If the second parameter of [rev_append] starts with some [a], then the first
element of the output of [rev_append] depends only on the first parameter
[l1].
This allows proving that two lists having a common tail have the same last
element.
Lemma same_last_element_rev_append :
∀ {A : Set} (a : A) l1 l2 l,
Coq.Lists.List.hd_error (Lists.List.rev_append l (a :: l1) )
= Coq.Lists.List.hd_error (Lists.List.rev_append l (a :: l2)).
Proof.
intros.
exact (same_last_element_rev_append_aux (Lists.List.length l) a l1 l2 l
Logic.eq_refl).
Qed.
∀ {A : Set} (a : A) l1 l2 l,
Coq.Lists.List.hd_error (Lists.List.rev_append l (a :: l1) )
= Coq.Lists.List.hd_error (Lists.List.rev_append l (a :: l2)).
Proof.
intros.
exact (same_last_element_rev_append_aux (Lists.List.length l) a l1 l2 l
Logic.eq_refl).
Qed.
If element in a filtered list, it is in intial list
Lemma filter_in {A : Set} a (ls ls' : list A) f :
Lists.List.filter f ls = a :: ls' → List.In a ls.
Proof.
pose proof (Lists.List.filter_In f a ls).
intro LE. apply H. rewrite LE. sfirstorder.
Qed.
Lists.List.filter f ls = a :: ls' → List.In a ls.
Proof.
pose proof (Lists.List.filter_In f a ls).
intro LE. apply H. rewrite LE. sfirstorder.
Qed.
In the section below we prove lemma [filter_preserves_prop] which states,
that CoqOfocaml.List.filter preserves proposition on all list elements.
At first we prove that library [filter] equals CoqOfocaml [filter],
then we rewrite CoqOfOcaml filter with library filter and prove
statement for library filter (easier, since we can use library's functions
on lists)
Check functions :
Print filter.
Print Lists.List.filter.
CoqOfOCaml [rev_append] equals to standard library [rev_append]
Lemma list_rev_append_eq {A : Set} l :
@CoqOfOCaml.List.rev_append A l = Lists.List.rev_append l.
Proof.
induction l; [sfirstorder |].
simpl. hauto lq: on.
Qed.
@CoqOfOCaml.List.rev_append A l = Lists.List.rev_append l.
Proof.
induction l; [sfirstorder |].
simpl. hauto lq: on.
Qed.
CoqOfOCaml [rev] equals to standard library [rev]
Lemma list_rev_eq {A : Set} (l : list A) :
@CoqOfOCaml.List.rev A l = rev l.
Proof.
unfold rev, CoqOfOCaml.List.rev.
unfold rev'. rewrite list_rev_append_eq.
reflexivity.
Qed.
@CoqOfOCaml.List.rev A l = rev l.
Proof.
unfold rev, CoqOfOCaml.List.rev.
unfold rev'. rewrite list_rev_append_eq.
reflexivity.
Qed.
Inner function of [CoqOfOCaml.List.find_all]
with Coqofocaml [rev]
Definition find' {A : Set} (p : A → bool) :=
(fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ CoqOfOCaml.List.rev accu
| x0 :: l ⇒ if p x0 then find (x0 :: accu) l else find accu l
end).
(fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ CoqOfOCaml.List.rev accu
| x0 :: l ⇒ if p x0 then find (x0 :: accu) l else find accu l
end).
Inner function of [CoqOfOCaml.List.find_all]
with standard library's [rev]
Definition find'_lib_rev {A : Set} (p : A → bool) :=
(fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ rev accu
| x0 :: l ⇒ if p x0 then find (x0 :: accu) l else find accu l
end).
(fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ rev accu
| x0 :: l ⇒ if p x0 then find (x0 :: accu) l else find accu l
end).
We prove that in inner function of [CoqOfOCaml.List.find_all]
we can replace Coqofocaml [rev] with standard [rev]
Lemma find_eq' {A : Set} p acc ls : @find' A p acc ls = find'_lib_rev p acc ls.
Proof.
revert acc p. induction ls.
intros. unfold find', find'_lib_rev.
apply list_rev_eq.
intros. simpl. hauto lq: on rew: off.
Qed.
Proof.
revert acc p. induction ls.
intros. unfold find', find'_lib_rev.
apply list_rev_eq.
intros. simpl. hauto lq: on rew: off.
Qed.
Auxiliary definition
We define inner function of [CoqOfOCaml.List.find_all] via find''
Lemma find_eq_general {A : Set} (f : A → bool) ls acc :
(fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ CoqOfOCaml.List.rev accu
| x0 :: l ⇒ if f x0 then find (x0 :: accu) l else find accu l
end) acc ls = @find'' A f acc ls.
Proof.
unfold find''. unfold find'. reflexivity.
Qed.
(fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ CoqOfOCaml.List.rev accu
| x0 :: l ⇒ if f x0 then find (x0 :: accu) l else find accu l
end) acc ls = @find'' A f acc ls.
Proof.
unfold find''. unfold find'. reflexivity.
Qed.
Auxiliary lemma for [filter_CoqOfOCaml_filter_eq]
Lemma fix_find_generalized_acc {A : Set} (acc : list A) ls (f : A → bool) :
(fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ rev accu
| x0 :: l ⇒ if f x0 then find (x0 :: accu) l else find accu l
end) acc ls = app (rev acc)%list
((fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ rev accu
| x0 :: l ⇒ if f x0 then find (x0 :: accu) l else find accu l
end) nil ls)%list.
Proof.
intros.
revert acc f.
induction ls as [|a ls IHls]. {
intros. unfold rev at 3. unfold rev'. unfold Lists.List.rev_append.
simpl. rewrite app_nil_r. reflexivity.
}
intros acc f.
destruct (f a); [| sfirstorder].
pose proof (IHls (a :: acc) f).
rewrite H.
pose proof (IHls (a :: nil) f).
rewrite H0.
remember ((fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ rev accu
| x0 :: l ⇒ if f x0 then find (x0 :: accu) l else find accu l
end) nil ls) as Fix_Find. clear HeqFix_Find.
simpl.
change (rev (a :: acc)) with (rev ([a] ++ acc)).
unfold rev. unfold rev'.
do 2 rewrite <- rev_alt.
rewrite rev_app_distr. simpl.
rewrite <- app_assoc. sfirstorder.
Qed.
(fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ rev accu
| x0 :: l ⇒ if f x0 then find (x0 :: accu) l else find accu l
end) acc ls = app (rev acc)%list
((fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ rev accu
| x0 :: l ⇒ if f x0 then find (x0 :: accu) l else find accu l
end) nil ls)%list.
Proof.
intros.
revert acc f.
induction ls as [|a ls IHls]. {
intros. unfold rev at 3. unfold rev'. unfold Lists.List.rev_append.
simpl. rewrite app_nil_r. reflexivity.
}
intros acc f.
destruct (f a); [| sfirstorder].
pose proof (IHls (a :: acc) f).
rewrite H.
pose proof (IHls (a :: nil) f).
rewrite H0.
remember ((fix find (accu x : list A) {struct x} : list A :=
match x with
| [] ⇒ rev accu
| x0 :: l ⇒ if f x0 then find (x0 :: accu) l else find accu l
end) nil ls) as Fix_Find. clear HeqFix_Find.
simpl.
change (rev (a :: acc)) with (rev ([a] ++ acc)).
unfold rev. unfold rev'.
do 2 rewrite <- rev_alt.
rewrite rev_app_distr. simpl.
rewrite <- app_assoc. sfirstorder.
Qed.
Equality of Coqofocaml's [filter] and library's filter
Lemma filter_CoqOfOCaml_filter_eq {A : Set} ls f :
filter f ls = @Lists.List.filter A f ls.
Proof.
revert f.
induction ls as [| a ls IHls]. sfirstorder.
intro f. simpl.
unfold filter in ×.
unfold CoqOfOCaml.List.filter in ×.
unfold CoqOfOCaml.List.find_all in ×.
destruct (f a) eqn:H.
{
rewrite <- IHls.
clear IHls. clear H.
revert a. revert f.
intros. do 2 rewrite find_eq_general.
unfold find''. rewrite find_eq'. rewrite find_eq'.
unfold find'_lib_rev.
pose proof (fix_find_generalized_acc [a] ls f).
rewrite H.
simpl. reflexivity.
} apply IHls.
Qed.
filter f ls = @Lists.List.filter A f ls.
Proof.
revert f.
induction ls as [| a ls IHls]. sfirstorder.
intro f. simpl.
unfold filter in ×.
unfold CoqOfOCaml.List.filter in ×.
unfold CoqOfOCaml.List.find_all in ×.
destruct (f a) eqn:H.
{
rewrite <- IHls.
clear IHls. clear H.
revert a. revert f.
intros. do 2 rewrite find_eq_general.
unfold find''. rewrite find_eq'. rewrite find_eq'.
unfold find'_lib_rev.
pose proof (fix_find_generalized_acc [a] ls f).
rewrite H.
simpl. reflexivity.
} apply IHls.
Qed.
CoqOfOCaml's filter preserves Prop.
Lemma filter_preserves_prop {A : Set} (ls ls': list A) (P : A → Prop) f :
Forall P ls → filter f ls = ls' → Forall P ls'.
Proof.
rewrite filter_CoqOfOCaml_filter_eq.
revert ls'.
induction ls as [| a ls IHls]. {
intros. unfold Lists.List.filter in H0.
sfirstorder.
}
intros ls' H H0.
simpl in H0.
destruct (f a). {
pose proof (IHls (Lists.List.filter f ls)).
assert (H' : Forall P (a :: ls)) by intuition.
apply Forall_cons in H.
apply H1 in H.
rewrite <- H0. sauto lq: on.
reflexivity.
}
apply IHls. sauto lq: on.
trivial.
Qed.
Forall P ls → filter f ls = ls' → Forall P ls'.
Proof.
rewrite filter_CoqOfOCaml_filter_eq.
revert ls'.
induction ls as [| a ls IHls]. {
intros. unfold Lists.List.filter in H0.
sfirstorder.
}
intros ls' H H0.
simpl in H0.
destruct (f a). {
pose proof (IHls (Lists.List.filter f ls)).
assert (H' : Forall P (a :: ls)) by intuition.
apply Forall_cons in H.
apply H1 in H.
rewrite <- H0. sauto lq: on.
reflexivity.
}
apply IHls. sauto lq: on.
trivial.
Qed.
The result of [filter] satisfies the predicate.
Lemma filter_inv {A : Set} (l : list A) (P : A → bool) filtered_l :
List.filter P l = filtered_l → List.Forall (fun x ⇒ P x = true) filtered_l.
Proof.
rewrite filter_CoqOfOCaml_filter_eq. generalize dependent filtered_l.
induction l as [ | a1 l1 IH] ; intros filtered_l.
{ intro H. hfcrush.
}
{ intro H.
destruct (P a1) eqn:b.
{ simpl in H; rewrite b in H; simpl in H ; subst.
specialize (IH l1) as IH0. hfcrush. }
{ hfcrush. }
}
Qed.
List.filter P l = filtered_l → List.Forall (fun x ⇒ P x = true) filtered_l.
Proof.
rewrite filter_CoqOfOCaml_filter_eq. generalize dependent filtered_l.
induction l as [ | a1 l1 IH] ; intros filtered_l.
{ intro H. hfcrush.
}
{ intro H.
destruct (P a1) eqn:b.
{ simpl in H; rewrite b in H; simpl in H ; subst.
specialize (IH l1) as IH0. hfcrush. }
{ hfcrush. }
}
Qed.
Two instances of [filter_inv] useful for inductions. @Q should we merge the two lemmas below?
Lemma filter_inv_hd {A : Set} {l : list A} (P : A → bool) a filtered_l :
List.filter P l = a :: filtered_l → P a = true.
Proof.
intro H.
specialize (filter_inv l P (a :: filtered_l)) as H0.
apply H0 in H. inversion H. assumption.
Qed.
Lemma filter_inv_tail {A : Set} {l :list A} (P : A → bool) a filtered_l :
List.filter P l = a :: filtered_l → List.Forall (fun x ⇒ P x = true) filtered_l.
Proof.
intro H.
specialize (filter_inv l P (a :: filtered_l)) as H0.
apply H0 in H. inversion H. assumption.
Qed.
List.filter P l = a :: filtered_l → P a = true.
Proof.
intro H.
specialize (filter_inv l P (a :: filtered_l)) as H0.
apply H0 in H. inversion H. assumption.
Qed.
Lemma filter_inv_tail {A : Set} {l :list A} (P : A → bool) a filtered_l :
List.filter P l = a :: filtered_l → List.Forall (fun x ⇒ P x = true) filtered_l.
Proof.
intro H.
specialize (filter_inv l P (a :: filtered_l)) as H0.
apply H0 in H. inversion H. assumption.
Qed.