(** * Propositional equality on natural numbers and the function [eqnatb] *)

(** Here is a program allowing us to compare two numbers [n1] and [n2].
    It is a function from [nat] to [bool]. *)

Fixpoint eqnatb n1 n2 :=
  match n1, n2 with
  | O, O         => true
  | S n1', S n2' => eqnatb n1' n2'
  | _, _         => false
  end.

(** [eqnatb] can be used in programs *)
Definition my_pgm (x y : nat)  :=
  match eqnatb x y with
  | true => x
  | false => y
  end.

Print my_pgm.

(** But [n1 = n2] cannot. 
    Conversely [n1 = n2] can be used to replace [n1] with [n2]
   in proofs, while [eqnatb n1 n2] cannot. *)

(** However, [eqnatb n1 n2] is expected to return [true] iff [n1 = n2].
    But it remains to be proved! *)

(** Remark: there is nothing special about the names [bool], [true] and [false].
    We could as well define a function returning a color. *)

Inductive color : Set := Green : color | Red : color.
 
Fixpoint eqnatc n1 n2 :=
  match n1,n2 with
  | O,O          => Green
  | S n1', S n2' => eqnatc n1' n2'
  | _,_          => Red
  end.

(** ** Easy direction (by simple induction) *)

Lemma eqnatb_eq_1 : forall n, eqnatb n n = true.
Proof.
  intro n. induction n as [ | n' IH]; cbn.
  - reflexivity.
  - exact IH.
Qed.
  
Lemma eqnatb_eq : forall n1 n2, n1 = n2 -> eqnatb n1 n2 = true.
Proof.
  intros n1 n2 e. rewrite e. apply (eqnatb_eq_1 n2).
  (** COMPLETE using the previous lemma. *)
Qed.

(* Optional exercise: direct proof without using [eqnatb_eq_1] *)
Lemma eqnatb_eq_direct : forall n1 n2, n1 = n2 -> eqnatb n1 n2 = true.
Proof.

  (** Nint: after the introductions and the rewriting step,
      use [clear] before [induction]. Do you see why? *)

Admitted.

(** Remark: Curry-Howard correspondence on inductive proofs *)
Fixpoint eqnatb_eq1_fct n : eqnatb n n = true :=
  match n with
  | 0 => eq_refl
  | S n' => eqnatb_eq1_fct n' (** structural decrease *)
        (** [eqnatb (S n') (S n')] reduces to [eqnatb n' n' by computation,
            which makes this expression accepted by type-checking *)
  end.

Compute eqnatb 3 3.
Compute eqnatb_eq1_fct 3.
Compute eqnatb_eq_1 3.


(** ** Converse direction, more difficult *)

(*** Contagious equalities *)

(** The tactic [change] allows us to replace the conclusion
by a convertible statement, that is, which is the same by computation.

example:

===========
2 + 1 = 6
-> change 6 with 3 * 2

In this example, we have a kind of "reverse computing" .
 *)

Lemma absurd: 5 = 4 -> 15 = 12.
Proof.
  intros e.
  (** Using [change], arrange the conclusion so that 5 et 4 appear in 
      similar expressions *)
  (** PLEASE COMPLETE as follows *)
  (** change (... 5 ... = ... 4 ...). *)
  (** Then conclude using [e] *)

Admitted.

(** In some sense, the aboce equality [e] can be qualified as "contagious",
    since it makes 2 other natural numbers equal as well *)

(** Contamination from an equality on [bool] to an equality on [nat] *)
Lemma true_false_eq : true = false -> forall n1 n2 : nat, n1 = n2.
Proof.
  intro etf. intros n1 n2.
  (** Define a function [f] such that [f true = n1] et [f false = n2].
      In order to define a local function in a proof script,
      use the tactic [pose].
      Here is a fake example. Pay ATTENTION to the parentheses.
   *)
  pose (fake_func := fun n => 3 * n).
  Undo 1.
  (** Define a suitable [f] and complete the proof.  *)
  (** [pose (f := fun (b:bool) => ...] *)

Admitted.

(*** Converse of [eqnatb_eq]. *)
(** In the exercise below, carefully choose the property to prove by induction *)
Lemma eq_eqnatb : forall n1 n2, eqnatb n1 n2 = true -> n1 = n2.
Proof.
  (* COMPLETE HERE *)

Admitted.

(** The programmoing construct corresponding to the tactoc [pose]
    is [let], a well-known construct in OCaml for instance.
    Here is an example for illustration. *)

Definition let_example : color -> nat :=
  fun c =>
    let d := match c with Green => Red | Red => Green end in
    let f := fun n => 2 * n in
    let nat_of := fun x =>  match x with Green => 0 | Red => 1 end in
    f (f (nat_of c) + f (nat_of d)).

(* ---------------------------------------------------------------------- *)
(** ** Optional : equivalence, conjunction, tactic [split]. *)

(** Lemmas [eqnatb_eq] and [eq_eqnatb] can be combined to get an
    equivalence, that is, the conjunction of two converse implications. *)

Print iff.

(** In this series of lectures, we don't need conjunction except here.
    We only indicate that the tactic [split] can be used for proving the 
    conjunction of two propositions. *)

Lemma eq_iff_eqnatb : forall n1 n2, eqnatb n1 n2 = true <-> n1 = n2.
Proof.
  intros n1 n2.
  split.
  (* COMPLETE HERE *)

Admitted.

(** The curious reader can guess how to use [refine] instead of [split]
    The only thing to know is that [A /\ B] is an infix notation for
    [and A B].
 *)

Print and.

(** Additional optional exercise *)
Lemma and_com : forall A B, A /\ B -> B /\ A.
Proof.
  (** At some point you should get an hypothesis, say [ab],
      of type [A /\ B], and you need to decompose it.
      Knowing that [and] is defined by an inductive definition,
        you should guess the tactic to be used  *)

  (** COMPLETE HERE *)
Admitted.