(* week-11_induction-principles.v *)
(* LPP 2024 - CS3236 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 05 Apr 2024 *)

(* ********** *)

Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.

Require Import Arith Bool.

(* ********** *)

(* One goal of this lecture is to revisit the proof that
   at most one function satisfies the following specification.
*)

Definition specification_of_the_fibonacci_function (fib : nat -> nat) :=
  fib 0 = 0
  /\
  fib 1 = 1
  /\
  forall n'' : nat,
    fib (S (S n'')) = fib n'' + fib (S n'').

Fixpoint fib (n : nat) : nat :=
  match n with
  | 0 =>
    0
  | S n' =>
    match n' with
    | 0 =>
      1
    | S n'' =>
      fib n'' + fib n'
    end
  end.

Lemma fold_unfold_fib_O :
  fib 0 =
  0.
Proof.
  fold_unfold_tactic fib.
Qed.

Lemma fold_unfold_fib_S :
  forall n' : nat,
    fib (S n') =
    match n' with
    | 0 =>
      1
    | S n'' =>
      fib n'' + fib n'
    end.
Proof.
  fold_unfold_tactic fib.
Qed.

Corollary fold_unfold_fib_1 :
  fib 1 =
  1.
Proof.
  rewrite -> fold_unfold_fib_S.
  reflexivity.
Qed.

Corollary fold_unfold_fib_SS :
  forall n'' : nat,
    fib (S (S n'')) =
    fib n'' + fib (S n'').
Proof.
  intro n''.
  rewrite -> fold_unfold_fib_S.
  reflexivity.
Qed.

Proposition fib_satisfies_the_specification_of_fib :
  specification_of_the_fibonacci_function fib.
Proof.
  unfold specification_of_the_fibonacci_function.
  Check (conj fold_unfold_fib_O (conj fold_unfold_fib_1 fold_unfold_fib_SS)).
  exact (conj fold_unfold_fib_O (conj fold_unfold_fib_1 fold_unfold_fib_SS)).
Qed.

(* ********** *)

(* The mathematical induction principle already exists,
   it is the structural induction principle associated to Peano numbers:
*)

Check nat_ind.

(* But we can still express it ourselves.
   We can also prove it using the resident mathematical induction principle,
   either implicitly or explicitly:
*)

Lemma nat_ind1 :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, P n -> P (S n)) ->
    forall n : nat, P n.
Proof.
Abort.

(* ********** *)

(* We can also use nat_ind as an ordinary lemma
   instead of using the induction tactic:
*)

Fixpoint r_add (i j : nat) : nat :=
  match i with
  | O =>
    j
  | S i' =>
    S (r_add i' j)
  end.

Lemma fold_unfold_r_add_O :
  forall j : nat,
    r_add 0 j =
    j.
Proof.
  fold_unfold_tactic r_add.
Qed.

Lemma fold_unfold_r_add_S :
  forall i' j : nat,
    r_add (S i') j =
    S (r_add i' j).
Proof.
  fold_unfold_tactic r_add.
Qed.

Proposition r_add_0_r :
  forall i : nat,
    r_add i 0 = i.
Proof.
  (* First, a routine induction: *)
  intro i.
  induction i as [ | i' IHi'].
  - exact (fold_unfold_r_add_O 0).
  - rewrite -> fold_unfold_r_add_S.
    Check f_equal.
    Check (f_equal S). (* : forall x y : nat, x = y -> S x = S y *)
    Check (f_equal S IHi').
    exact (f_equal S IHi').

  Restart.

  (* And now for using nat_ind: *)
  Check nat_ind.
Abort.

(* ********** *)

Fixpoint fibfib (n : nat) : nat * nat :=
  match n with
  | O =>
    (0, 1)
  | S n' =>
    let (fib_n', fib_succ_n') := fibfib n'
    in (fib_succ_n', fib_n' + fib_succ_n')
  end.

Definition fib_lin (n : nat) : nat :=
  let (fib_n, _) := fibfib n
  in fib_n.

Lemma fold_unfold_fibfib_O :
  fibfib 0 =
  (0, 1).
Proof.
  fold_unfold_tactic fibfib.
Qed.

Lemma fold_unfold_fibfib_S :
  forall n' : nat,
    fibfib (S n') =
    let (fib_n', fib_succ_n') := fibfib n'
    in (fib_succ_n', fib_n' + fib_succ_n').
Proof.
  fold_unfold_tactic fibfib.
Qed.

Lemma about_fibfib :
  forall fib : nat -> nat,
    specification_of_the_fibonacci_function fib ->
    forall n : nat,
      fibfib n = (fib n, fib (S n)).
Proof.
  unfold specification_of_the_fibonacci_function.
  intros fib [S_fib_O [S_fib_1 S_fib_SS]] n.
  induction n as [ | [ | n''] IH].
  - rewrite -> fold_unfold_fibfib_O.
    rewrite -> S_fib_O.
    rewrite -> S_fib_1.
    reflexivity.
  - rewrite -> fold_unfold_fibfib_S.
    rewrite -> fold_unfold_fibfib_O.
    rewrite -> S_fib_1.
    rewrite -> S_fib_SS.
    rewrite -> S_fib_O.
    rewrite -> S_fib_1.
    reflexivity.
  - rewrite -> fold_unfold_fibfib_S.
    rewrite -> IH.
    rewrite <- (S_fib_SS (S n'')).
    reflexivity.
Qed.

Proposition fib_lin_satisfies_the_specification_of_fib :
  specification_of_the_fibonacci_function fib_lin.
Proof.
  unfold specification_of_the_fibonacci_function, fib_lin.
  split.
  - rewrite -> fold_unfold_fibfib_O.
    reflexivity.
  - split.
    + rewrite -> fold_unfold_fibfib_S.
      rewrite -> fold_unfold_fibfib_O.
      reflexivity.
    + intro i.
      Check (about_fibfib fib fib_satisfies_the_specification_of_fib (S (S i))).
      rewrite -> (about_fibfib fib fib_satisfies_the_specification_of_fib (S (S i))).
      rewrite -> (about_fibfib fib fib_satisfies_the_specification_of_fib i).
      rewrite -> (about_fibfib fib fib_satisfies_the_specification_of_fib (S i)).
      exact (fold_unfold_fib_SS i).
Qed.

(* ********** *)

(* We can also express a mathematical induction principle
   with two base cases and two induction hypotheses
   that befits the structure of the Fibonacci function:
*)

Lemma nat_ind2 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    (forall n : nat, P n -> P (S n) -> P (S (S n))) ->
    forall n : nat, P n.
Proof.
  intros P H_P0 H_P1 H_PSS n.
  induction n as [ | [ | n''] IHn'].
Abort.

(* Thus equipped, the following theorem is proved pretty directly: *)

Theorem there_is_at_most_one_fibonacci_function :
  forall fib1 fib2 : nat -> nat,
    specification_of_the_fibonacci_function fib1 ->
    specification_of_the_fibonacci_function fib2 ->
    forall n : nat,
      fib1 n = fib2 n.
Proof.
  intros fib1 fib2.
  unfold specification_of_the_fibonacci_function.
  intros [H_fib1_0 [H_fib1_1 H_fib1_SS]]
         [H_fib2_0 [H_fib2_1 H_fib2_SS]]
         n.
  induction n as [ | | n'' IHn'' IHSn''] using nat_ind2.
Abort.

(* ***** *)

Fixpoint evenp1 (n : nat) : bool :=
  match n with
  | 0 =>
    true
  | S n' =>
    negb (evenp1 n')
  end.

Lemma fold_unfold_evenp1_O :
  evenp1 0 =
  true.
Proof.
  fold_unfold_tactic evenp1.
Qed.

Lemma fold_unfold_evenp1_S :
  forall n' : nat,
    evenp1 (S n') =
    negb (evenp1 n').
Proof.
  fold_unfold_tactic evenp1.
Qed.

(* ***** *)

(* The evenness predicate is often programmed tail-recursively
   and with no accumulator, by peeling two layers of S at a time.
   Its equivalence with evenp1 is messy to prove by mathematical induction
   but effortless using nat_ind2:
*)

Fixpoint evenp2 (n : nat) : bool :=
  match n with
  | 0 =>
    true
  | S n' =>
    match n' with
    | 0 =>
      false
    | S n'' =>
      evenp2 n''
    end
  end.

Lemma fold_unfold_evenp2_O :
  evenp2 0 =
  true.
Proof.
  fold_unfold_tactic evenp2.
Qed.

Lemma fold_unfold_evenp2_S :
  forall n' : nat,
    evenp2 (S n') =
    match n' with
    | 0 =>
      false
    | S n'' =>
      evenp2 n''
    end.
Proof.
  fold_unfold_tactic evenp2.
Qed.

Corollary fold_unfold_evenp2_1 :
  evenp2 1 =
  false.
Proof.
  rewrite -> fold_unfold_evenp2_S.
  reflexivity.
Qed.

Corollary fold_unfold_evenp2_SS :
  forall n'' : nat,
    evenp2 (S (S n'')) =
    evenp2 n''.
Proof.
  intro n''.
  rewrite -> fold_unfold_evenp2_S.
  reflexivity.
Qed.

Theorem evenp1_and_evenp2_are_functionally_equal :
  forall n : nat,
    evenp1 n = evenp2 n.
Proof.
  intro n.
  induction n as [ | n' IHn'].
Abort.

(* ***** *)

Lemma two_times_S :
  forall n : nat,
    S (S (2 * n)) = 2 * S n.
Proof.
Admitted.

Theorem soundness_and_completeness_of_evenp_using_nat_ind2 :
  forall n : nat,
    evenp2 n = true <-> exists m : nat, n = 2 * m.
Proof.
  intro n.
  induction n as [ | | n' [IHn'_sound IHn'_complete] [IHSn'_sound IHSn'_complete]] using nat_ind2.
Abort.

(* ***** *)

(* For another example, we can prove the mathematical induction principle using nat_ind2: *)

Lemma nat_ind1' :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, P n -> P (S n)) ->
    forall n : nat, P n.
Proof.
  intros P H_P0 H_PS n.
  induction n as [ | | n' IHn'] using nat_ind2.
  - exact H_P0.
  - Check (H_PS 0 H_P0).
    exact (H_PS 0 H_P0).
  - Check (H_PS (S n') IHn).
    exact (H_PS (S n') IHn).
Qed.

(* We can also generalize nat_ind2 to an induction principle
   with three base cases and three induction hypotheses: *)

Lemma nat_ind3 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    P 2 ->
    (forall n : nat, P n -> P (S n) -> P (S (S n)) -> P (S (S (S n)))) ->
    forall n : nat, P n.
Proof.
Abort.

(* ***** *)

Fixpoint ternaryp (n : nat) : bool :=
  match n with
  | 0 =>
    true
  | 1 =>
    false
  | 2 =>
    false
  | S (S (S n')) =>
    ternaryp n'
  end.

Lemma fold_unfold_ternaryp_O :
  ternaryp 0 =
  true.
Proof.
  fold_unfold_tactic ternaryp.
Qed.

Lemma fold_unfold_ternaryp_1 :
  ternaryp 1 =
  false.
Proof.
  fold_unfold_tactic ternaryp.
Qed.

Lemma fold_unfold_ternaryp_2 :
  ternaryp 2 =
  false.
Proof.
  fold_unfold_tactic ternaryp.
Qed.

Lemma fold_unfold_ternaryp_SSS :
  forall n' : nat,
    ternaryp (S (S (S n'))) =
    ternaryp n'.
Proof.
  fold_unfold_tactic ternaryp.
Qed.

Theorem soundness_and_completeness_of_ternaryp_using_nat_ind3 :
  forall n : nat,
    ternaryp n = true <-> exists m : nat, n = 3 * m.
Proof.
Abort.

(* ********** *)

Lemma three_times_S :
  forall n : nat,
    S (S (S (3 * n))) = 3 * S n.
Proof.
Admitted.

Property threes_and_fives :
  forall n : nat,
  exists a b : nat,
    8 + n = 3 * a + 5 * b.
Proof.
Abort.

(* ********** *)

Lemma four_times_S :
  forall n : nat,
    S (S (S (S (4 * n)))) = 4 * S n.
Proof.
Admitted.

Lemma five_times_S :
  forall n : nat,
    S (S (S (S (S (5 * n))))) = 5 * S n.
Proof.
Admitted.

Property fours_and_fives :
  forall n : nat,
  exists a b : nat,
    12 + n = 4 * a + 5 * b.
Proof.
Abort.

(* ********** *)

(* end of week-10_induction-principles.v *)