Skip to main content

🍃 List.v

Proofs

See code, Gitlab

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.
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.

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.

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.

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
    | Nonefind_map f l
    | Some ySome 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 yg y acc
      | Noneacc
      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 yg y acc
      | Nonez_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
        | Noneacc
        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
          | Noneacc
          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.

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.

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.

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.

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 y2R_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 xf1 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 xf1 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 xf1 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.

[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.

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.

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.

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.

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.

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.

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.

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 accf (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.

[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 accf 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.

[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.

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.

[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.

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.

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.

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.

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.

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.

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 [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.

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 :: lif 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 :: lif 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.

Auxiliary definition
Definition find'' {A : Set} p acc ls := @find' A p acc ls.

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 :: lif 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 :: lif 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 :: lif 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 :: lif 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.

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.

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 xP 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 xP 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.