(**
Énoncé complet : voir TD.
*)


(* ----------------------------------------------------------------------- *)
(** * Preuve d'équivalence entre égalité des entiers et eqnatb valant true *)

(** eqnatb renvoie true ssi ses arguments représentent le même entier naturel *)

(** ** Égalité booléenne entre deux entiers *)
(** Observation clé :
    dans l'appel récursif, le second paramètre ne reste pas fixé à n2 *)
Fixpoint eqnatb n1 n2 :=
   match n1,n2 with
  | O,O          => true
  | S n1', S n2' => eqnatb n1' n2'
  | _,_          => false
  end.

(** ** Le sens le plus facile (récurrence triviale) *)

Lemma eqnatb_eq1 : forall n, eqnatb n n = true.
Proof.
  intro n; induction n as [ | n' Hn'].
  - reflexivity.
  - apply Hn'.
Qed.

(** ** Démo surprise (1) : preuve fournie par un programme récursif *)
Fixpoint eqnatb_eq1_fct n : eqnatb n n = true :=
  match n with
  | 0 => eq_refl
  | S n' => eqnatb_eq1_fct n' (** Observer la décroissance structurelle *)
  end.

Lemma eqnatb_eq2 : forall n1 n2, n1 = n2 -> eqnatb n1 n2 = true.
Proof.
  (* À compléter: penser à utiliser clear avant induction. *)
Admitted.

(** ** Le sens le plus difficile (récurrence quantifiée + preuve par cas) *)

Lemma true_false_eg : true = false -> forall n1 n2 : nat, n1 = n2.
Admitted.

(** C'est l'autre direction qui nous intéresse,
    on peut la démontrer à partir du lemme précédent *)
Lemma false_true_eg : false = true -> forall n1 n2 : nat, n1 = n2.
Proof.
  intro eft. intros n1 n2.
  apply true_false_eg.
  (** Bien comprendre ce apply et terminer la preuve *)
Admitted.

(** Dans la suite, plutôt que rewrite il est intéressant d'employer
    un apply de S_equal. Voir exemple d'utilisation plus bas. *)
Lemma S_equal : forall x y : nat, x = y -> S x = S y.
Proof.
  (** À démontrer (facile)*)
Admitted.

(** Remarque : f_equal est une version générale de ce lemme *)
Check (f_equal S).

Lemma eq_eqnatb : forall n1 n2, eqnatb n1 n2 = true -> n1 = n2.
Proof.
  intros n1.
  (* À compléter avec les indications données en cours *)
Admitted.

(** ** Démo surprise (2) *)
Reset eq_eqnatb.

(** Échauffement : neutralité de 0 à droite de + *)

(** Mise au point avec refine *)
Fixpoint plus_0_r n : n + 0 = n.
Proof.
  refine (
      match n with
      | 0 => eq_refl
      | S n' => _
      end).
  - cbn [plus]. apply S_equal. apply (plus_0_r n').
Qed.

Reset plus_0_r.


(** Version directe *)
Fixpoint plus_0_r n : n + 0 = n :=
  match n with
  | 0 => eq_refl
  | S n' => S_equal (n' + 0) n' (plus_0_r n')
  end.

Reset plus_0_r.
(** Remarque : écriture allégée, c.f. cours 5 à venir *)
Fixpoint plus_0_r n : n + 0 = n :=
  match n with
  | 0 => eq_refl
  | S n' => S_equal _ _ (plus_0_r n')
  end.

(** Même technique sur eq_eqnatb. Observation importante :
    Le programme récursif suit le même schéma que eqnatb *)
Fixpoint eq_eqnatb n1 n2 : eqnatb n1 n2 = true -> n1 = n2 :=
  match n1,n2 with
  | O,     O     => fun e => eq_refl
  | S n1', S n2' => fun e => S_equal n1' n2' (eq_eqnatb n1' n2' e)
  | x,     y     => fun e => false_true_eg e x y
  end.

(** Observer que le type de e, dans le cas récursif, est à la fois
    (eqnatb (S n1') (S n2') = true  et  eqnatb n1' n2' = true
    qui sont des expressions interchangeables car convertibles
    par calcul.
    Cea apparaît mieux lors de la mise au point avec refine
 *)

Reset eq_eqnatb.
Fixpoint eq_eqnatb n1 n2 : eqnatb n1 n2 = true -> n1 = n2.
  refine (
  match n1,n2 with
  | O,     O     => fun e => _
  | S n1', S n2' => fun e => _
  | x,     y     => fun e => _
  end).
  (** Compléter *)
Admitted.

(** Dans la même veine, revoir et expliquer la manière dont la correction
    de la fonction simpl0 du TD2 a été prouvée *)