Tests: add beginning of proofs for saturation arithmetic

A beginning of proof for the saturation arithmetic tests that are in https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/pbt/saturation_fuzzing.ml

The content of the Presentation.v I used for the generic Coq examples:

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.

Lemma and_commutative (A B : Prop) :
  A /\ B ->
  B /\ A.
Proof.
  intros [H1 H2].
  constructor.
  { exact H2. }
  { exact H1. }
Qed.

Lemma and_commutative_auto (A B : Prop) :
  A /\ B ->
  B /\ A.
Proof.
  tauto.
Qed.

Fixpoint filter_map {A B : Set}
  (f : A -> option B) (l : list A) :
  list B :=
  match l with
  | [] => []
  | x :: l =>
    match f x with
    | None => filter_map f l
    | Some y => cons y (filter_map f l)
    end
  end.

Fixpoint map {A B : Set}
  (f : A -> B) (l : list A) :
  list B :=
  match l with
  | [] => []
  | x :: l => (f x) :: (map f l)
  end.

Fixpoint filter {A : Set}
  (f : A -> bool) (l : list A) :
  list A :=
  match l with
  | [] => []
  | x :: l =>
    if f x then
      x :: (filter f l)
    else
      filter f l
  end.

Lemma filter_map_eq_map {A B : Set}
  (f : A -> B) (l : list A) :
  map f l =
  filter_map (fun x => Some (f x)) l.
Proof.
  induction l.
  { simpl.
    reflexivity.
  }
  { simpl.
    rewrite IHl.
    reflexivity.
  }
Qed.

(* Using Coq Hammer *)
Lemma filter_map_eq_map_hammer {A B : Set}
  (f : A -> B) (l : list A) :
  map f l =
  filter_map (fun x => Some (f x)) l.
Proof.
  induction l; sfirstorder.
Qed.

Lemma test_add_commutes (t1 t2 : int) :
  Saturation_repr.Valid.t t1 ->
  Saturation_repr.Valid.t t2 ->
  Saturation_repr.add t1 t2 = Saturation_repr.add t2 t1.
Proof.
  intros.
  do 2 (rewrite Saturation_repr.add_eq; trivial).
  replace ((t1 + t2)%Z) with ((t2 + t1)%Z).
  { reflexivity. }
  { lia. }
Qed.

(*
Print list.
Check list.
Search list.
Locate "+".
*)