(* week-11_induction-principles-colon-from-first-order-to-higher-order-induction.v *)
(* Time-stamp: <2025-07-02 14:45:13 olivier> *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 02 Jul 2025 *)
(* was: *)
(* Version of 04 Jun 2025 *)
(* was: *)
(* Version of 04 Apr 2025 *)

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

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

Require Import Arith Bool.

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

(* 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.
  intros P P_O P_S n.
  induction n as [ | n' IHn'].
  - exact P_O.
  - exact (P_S n' IHn').
  Show Proof.
(*
(fun (P : nat -> Prop) (P_O : P 0) (P_S : forall n' : nat, P n' -> P (S n')) (n : nat) =>
 nat_ind (fun n0 : nat => P n0) P_O (fun (n' : nat) (IHn' : P n') => P_S n' IHn') n)
*)

  Restart.

  intros P P_O P_S n.
  Check (nat_ind P).
  Check (nat_ind P P_O).
  Check (nat_ind P P_O P_S).
  Check (nat_ind P P_O P_S n).
  exact (nat_ind P P_O P_S n).
  Show Proof.
(*
(fun (P : nat -> Prop) (P_O : P 0) (P_S : forall n' : nat, P n' -> P (S n')) (n : nat) => nat_ind P P_O P_S n)
*)

  Restart.

  exact (fun P P_O P_S n => nat_ind P P_O P_S n).
  Show Proof.

  Restart.

  exact nat_ind.
Qed.

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

(* 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.
    rewrite -> IHi'.
    reflexivity.

  Restart.

  (* Second, a variant: *)
  intro i.
  induction i as [ | i' IHi'].
  - exact (fold_unfold_r_add_O 0).
  - rewrite <- IHi' at 2.
    exact (fold_unfold_r_add_S i' 0).

  Restart.

  (* Third, a shortcut: *)
  intro i.
  induction i as [ | i' IHi'].
  - compute.
    reflexivity.
  - rewrite <- IHi' at 2.
    exact (fold_unfold_r_add_S i' 0).

  Restart.

  (* Fourth, a shorter shortcut: *)
  intro i.
  induction i as [ | i' IHi'].
  - reflexivity.
  - rewrite <- IHi' at 2.
    exact (fold_unfold_r_add_S i' 0).

  Restart.

  (* And now for using nat_ind: *)
  Check nat_ind.
  Check (nat_ind
           (fun i => r_add i 0 = i)).
  Check (nat_ind
           (fun i => r_add i 0 = i)
           (fold_unfold_r_add_O 0)).
  apply (nat_ind
           (fun i => r_add i 0 = i)
           (fold_unfold_r_add_O 0)).
  intros i' IHi'.
  rewrite -> fold_unfold_r_add_S.
  rewrite -> IHi'.
  reflexivity.

  Restart.

  (* Using nat_ind with the same variant: *)
  Check nat_ind.
  Check (nat_ind
           (fun i => r_add i 0 = i)).
  Check (nat_ind
           (fun i => r_add i 0 = i)
           (fold_unfold_r_add_O 0)).
  apply (nat_ind
           (fun i => r_add i 0 = i)
           (fold_unfold_r_add_O 0)).
  intros i' IHi'.
  rewrite <- IHi' at 2.
  exact (fold_unfold_r_add_S i' 0).
Qed.

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

(* Exercise 01 *)

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

Lemma fold_unfold_tr_add_O :
  forall j : nat,
    tr_add 0 j =
    j.
Proof.
  fold_unfold_tactic tr_add.
Qed.

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

Lemma about_tr_add :
  forall i j : nat,
    tr_add i (S j) = S (tr_add i j).
Proof.
  Check (nat_ind
           (fun i => forall j : nat, tr_add i (S j) = S (tr_add i j))).
  (* wanted: forall j : nat, tr_add 0 (S j) = S (tr_add 0 j) *)
  assert (H_O : forall j : nat, tr_add 0 (S j) = S (tr_add 0 j)).
  { intro j.
    rewrite ->2 fold_unfold_tr_add_O.
    reflexivity. }
  Check (nat_ind
           (fun i => forall j : nat, tr_add i (S j) = S (tr_add i j))
           H_O).
Admitted.

Proposition tr_add_0_r :
  forall i : nat,
    tr_add i 0 = i.
Proof.
  intro i.
  induction i as [ | i' IHi'].
  - exact (fold_unfold_tr_add_O 0).
  - rewrite -> fold_unfold_tr_add_S.
    rewrite -> (about_tr_add i' 0).
    rewrite -> IHi'.
    reflexivity.

  Restart.

  Check (nat_ind
           (fun i => tr_add i 0 = i)).
Abort.

Theorem r_add_and_tr_add_are_equivalent :
  forall i j : nat,
    r_add i j = tr_add i j.
Proof.
Abort.

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

(* 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 P_0 P_1 P_SS.
  assert (all2 :
            forall n : nat,
              P n /\ P (S n)).
  { intro n.
    induction n as [ | n' [IHn' IHSn']].
    - split.
      + exact P_0.
      + exact P_1.
    - split.
      + exact IHSn'.
      + exact (P_SS n' IHn' IHSn'). }
  intro n.
  destruct (all2 n) as [ly _].
  exact ly.  (* <-- to be read aloud *)
Qed.

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

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.
  exact (conj fold_unfold_fib_O (conj fold_unfold_fib_1 fold_unfold_fib_SS)).
Qed.

(* ***** *)

Fixpoint fibfib (n : nat) : nat * nat :=
  match n with
    O =>
    (0, 1)
  | S n' =>
    let (fib_n', fib_Sn') := fibfib n'
    in (fib_Sn', fib_n' + fib_Sn')
  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_Sn') := fibfib n'
    in (fib_Sn', fib_n' + fib_Sn').
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.

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

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

(* Exercise 02 *)

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

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

Theorem there_is_at_most_one_fibonacci_function :
  forall fib1 : nat -> nat,
    specification_of_the_fibonacci_function fib1 ->
    forall fib2 : nat -> nat,
      specification_of_the_fibonacci_function fib2 ->
      forall n : nat,
        fib1 n = fib2 n.
Proof.
  unfold specification_of_the_fibonacci_function.
  intros fib1 [S_fib1_O [S_fib1_SO S_fib1_SS]]
         fib2 [S_fib2_O [S_fib2_SO S_fib2_SS]]
         n.
  induction n as [ | | n'' IHn'' IHSn''] using nat_ind2.

  Restart.

  unfold specification_of_the_fibonacci_function.
  intros fib1 [S_fib1_O [S_fib1_SO S_fib1_SS]]
         fib2 [S_fib2_O [S_fib2_SO S_fib2_SS]].
  Check (nat_ind2
           (fun n : nat => fib1 n = fib2 n)).
  rewrite <- S_fib2_O in S_fib1_O at 2.
  Check (nat_ind2
           (fun n : nat => fib1 n = fib2 n)
           S_fib1_O).
Abort.

(* ***** *)

(* 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
    O =>
    true
  | S n' =>
    match n' with
      O =>
      false
    | S n'' =>
      evenp2 n''
    end
  end.

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

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

Corollary fold_unfold_evenp2_SO :
  evenp2 (S O) =
  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.

(* ***** *)

Lemma two_times_S :
  forall n : nat,
    2 * S n = S (S (2 * n)).
Proof.
  intro n.
  ring.
Qed.

Theorem soundness_and_completeness_of_evenp2_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.
  - rewrite -> fold_unfold_evenp2_O.
    split.
    + intros _.
      exists 0.
      compute.
      reflexivity.
    + intros _.
      reflexivity.
  - rewrite -> fold_unfold_evenp2_SO.
    split.
    + intro H_absurd.
      discriminate H_absurd.
    + intros [[ | m'] H_m].
      * discriminate H_m.
      * rewrite -> two_times_S in H_m.
        discriminate H_m.
  - rewrite -> fold_unfold_evenp2_SS.
    split.
    + intros H_n'.
      destruct (IHn'_sound H_n') as [m' H_m'].
      rewrite -> H_m'.
      rewrite <- two_times_S.
      exists (S m').
      reflexivity.
    + intros [[ | m'] H_m'].
      * discriminate H_m'.
      * rewrite -> two_times_S in H_m'.
        rewrite -> (Nat.mul_comm 2 _) in H_m'; injection H_m' as H_m'; rewrite <- (Nat.mul_comm 2 _) in H_m'.
        apply IHn'_complete.
        exists m'.
        exact H_m'.
Qed.

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

(* Exercise 03 *)

Lemma nat_ind2_0 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    (forall k : nat,
        P k ->
        P (S (S k))) ->
    forall n : nat,
      P n.
Proof.
Admitted.

Lemma nat_ind2_1 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    (forall k : nat,
        P (S k) ->
        P (S (S k))) ->
    forall n : nat,
      P n.
Proof.
Admitted.

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

(* Exercise 04 *)

Theorem soundness_and_completeness_of_even2p_using_nat_ind2_revisited :
  forall n : nat,
    evenp2 n = true <-> exists m : nat, n = 2 * m.
Proof.
  intro n.
  split.
  - induction n as [ | | n' IHn' IHSn'] using nat_ind2.
    + admit.
    + admit.
    + admit.
  - intros [q H_q].
    rewrite -> H_q.
    clear H_q n.
    induction q as [ | | q' IHq' IHSq'] using nat_ind2.
    + admit.
    + admit.
    + admit.
Admitted.

Theorem soundness_and_completeness_of_evenp_re2visited :
  forall n : nat,
    evenp2 n = true <-> exists m : nat, n = 2 * m.
Proof.
Abort.

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

(* Exercise 05 *)

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.

Theorem evenp1_and_evenp2_are_functionally_equal_using_nat_ind2 :
  forall n : nat,
    evenp1 n = evenp2 n.
Proof.
Abort.

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

(* Exercise 06 *)

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.
  intros P P_0 P_1 P_2 P_SSS.
Admitted.

Lemma nat_ind1_using_nat_ind3 :
  forall P : nat -> Prop,
    P 0 ->
    (forall n' : nat,
        P n' ->
        P (S n')) ->
    forall n : nat,
      P n.
Proof.
  intros P P_0 P_S n.
  induction n as [ | | | n' IHn' IHSn' IHSSn'] using nat_ind3.
Abort.

Lemma nat_ind2_using_nat_ind3 :
  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 P_0 P_1 P_SS.
Abort.

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

(* Exercise 07 *)

Lemma nat_ind3_0 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    P 2 ->
    (forall n' : nat,
        P n' ->
        P (S (S (S n')))) ->
    forall n : nat,
      P n.
Proof.
  intros P P_0 P_1 P_2 P_SSS.
Admitted.

Lemma nat_ind3_1 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    P 2 ->
    (forall k : nat,
        P (S k) ->
        P (S (S (S k)))) ->
    forall n : nat,
      P n.
Proof.
Admitted.

Lemma nat_ind3_2 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    P 2 ->
    (forall k : nat,
        P (S (S k)) ->
        P (S (S (S k)))) ->
    forall n : nat,
      P n.
Proof.
Admitted.

Lemma nat_ind3_01 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    P 2 ->
    (forall k : nat,
        P k ->
        P (S k) ->
        P (S (S (S k)))) ->
    forall n : nat,
      P n.
Proof.
Admitted.

Lemma nat_ind3_02 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    P 2 ->
    (forall k : nat,
        P k ->
        P (S (S k)) ->
        P (S (S (S k)))) ->
    forall n : nat,
      P n.
Proof.
Admitted.

Lemma nat_ind3_12 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    P 2 ->
    (forall k : nat,
        P (S k) ->
        P (S (S k)) ->
        P (S (S (S k)))) ->
    forall n : nat,
      P n.
Proof.
Admitted.

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

(* Exercise 08 *)

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.

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

(* Exercise 09 *)

Lemma three_times_S :
  forall n : nat,
    3 * S n = S (S (S (3 * n))).
Proof.
  intro n.
  ring.
Qed.

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

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

(* Exercise 10 *)

Lemma five_times_S :
  forall n : nat,
    5 * S n = S (S (S (S (S (5 * n))))).
Proof.
  intro n.
  ring.
Qed.

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

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

(* Exercise 11 *)

Lemma nat_ind4 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    P 2 ->
    P 3 ->
    (forall n' : nat,
        P n' ->
        P (S n') ->
        P (S (S n')) ->
        P (S (S (S n'))) ->
        P (S (S (S (S n'))))) ->
    forall n : nat,
      P n.
Proof.
Admitted.

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

(* Exercise 12 *)

Lemma four_times_S :
  forall n : nat,
    4 * S n = S (S (S (S (4 * n)))).
Proof.
  intro n.
  ring.
Qed.

Property fours_and_fives_using_nat_ind4 :
  forall n : nat,
  exists a b : nat,
    12 + n = 4 * a + 5 * b.
Proof.
  intros n.
  induction n as [ | | | | n' [a1 [b1 IH_a1_b1]] [a2 [b2 IH_a2_b2]] [a3 [b3 IH_a3_b3]] [a4 [b4 IH_a4_b4]]] using nat_ind4.
Abort.

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

(* Exercise 13 *)

Property fours_and_fives_using_nat_ind1 :
  forall n : nat,
  exists a b : nat,
    12 + n = 4 * a + 5 * b.
Proof.
  intro n.
  induction n as [ | n' [[ | a'] [b IH_a_b]]].
Abort.

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

(* Exercise 14.a *)

Lemma auxiliary_23 :
  forall x y : nat,
    2 * x = 3 * y ->
    exists z : nat,
      x = 3 * z.
Proof.
  intro x.
  induction x as [ | | | x' IHx'] using nat_ind3_0; intros y H_y.
Abort.

(* ***** *)

(* Exercise 14.b *)

Lemma auxiliary_32 :
  forall x y : nat,
    2 * x = 3 * y ->
    exists z : nat,
      y = 2 * z.
Proof.
  intros x y.
  revert x.
  induction y as [ | | | y' IHy' IHSy' IHSSy'] using nat_ind3; intros x H_x.
Abort.

(* ***** *)

(* Exercise 14.c *)

Property a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_indirectly :
  forall (n : nat)
         (q2 : nat),
    n = 2 * q2 ->
    forall q3 : nat,
      n = 3 * q3 ->
      exists q6 : nat,
        n = 6 * q6.
Proof.
Abort.

(* ***** *)

(* Exercise 14.d *)

Lemma times_reg_l :
  forall n m p : nat,
    S p * n = S p * m -> n = m.
Proof.
Admitted.

Lemma a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_indirectly_aux :
  forall x y : nat,
    2 * x = 3 * y ->
    exists z : nat,
      x = 3 * z /\ y = 2 * z.
Proof.
Abort.

(* ***** *)

(* Exercise 14.e *)

Property a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_indirectly_revisited :
  forall (n : nat)
         (q2 : nat),
    n = 2 * q2 ->
    forall q3 : nat,
      n = 3 * q3 ->
      exists q6 : nat,
        n = 6 * q6.
Proof.
Abort.

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

(* Exercise 15 *)

Lemma nat_ind6 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    P 2 ->
    P 3 ->
    P 4 ->
    P 5 ->
    (forall n' : nat,
        P n' ->
        P (S n') ->
        P (S (S n')) ->
        P (S (S (S n'))) ->
        P (S (S (S (S n')))) ->
        P (S (S (S (S (S n'))))) ->
        P (S (S (S (S (S (S n'))))))) ->
    forall n : nat,
      P n.
Proof.
  intros P P_0 P_1 P_2 P_3 P_4 P_5 P_SSSSSS.
  assert (all6 :
            forall n : nat,
              P n /\ P (S n) /\ P (S (S n)) /\ P (S (S (S n))) /\ P (S (S (S (S n)))) /\ P (S (S (S (S (S n)))))).
  { intro n.
    induction n as [ | n' [IHn' [IHSn' [IHSSn' [IHSSSn' [IHSSSSn' IHSSSSSn']]]]]].
    - split; [ | split; [ | split; [ | split; [ | split]]]].
      + exact P_0.
      + exact P_1.
      + exact P_2.
      + exact P_3.
      + exact P_4.
      + exact P_5.
    - split; [ | split; [ | split; [ | split; [ | split]]]].
      + exact IHSn'.
      + exact IHSSn'.
      + exact IHSSSn'.
      + exact IHSSSSn'.
      + exact IHSSSSSn'.
      + exact (P_SSSSSS n' IHn' IHSn' IHSSn' IHSSSn' IHSSSSn' IHSSSSSn'). }
  intro n.
  destruct (all6 n) as [ly _].
  exact ly.
Qed.

Lemma nat_ind6_0 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    P 2 ->
    P 3 ->
    P 4 ->
    P 5 ->
    (forall n' : nat,
        P n' ->
        P (S (S (S (S (S (S n'))))))) ->
    forall n : nat,
      P n.
Proof.
  intros P P_0 P_1 P_2 P_3 P_4 P_5 P_SSSSSS n.
  induction n as [ | | | | | | n' IHn' _ _ _ _ _] using nat_ind6.
  - exact P_0.
  - exact P_1.
  - exact P_2.
  - exact P_3.
  - exact P_4.
  - exact P_5.
  - exact (P_SSSSSS n' IHn').
Qed.

Lemma six_times_S :
  forall n : nat,
    6 * S n = S (S (S (S (S (S (6 * n)))))).
Proof.
  intro n.
  ring.
Qed.

Property a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_directly :
  forall (n : nat)
         (q2 : nat),
    n = 2 * q2 ->
    forall q3 : nat,
      n = 3 * q3 ->
      exists q6 : nat,
        n = 6 * q6.
Proof.
  intro n.
  induction n as [ | | | | | | n' IHn'] using nat_ind6_0.
  - intros _ _ _ _.
    exists 0.
    compute.
    reflexivity.
  - (* forall q2 : nat, 1 = 2 * q2 -> forall q3 : nat, 1 = 3 * q3 -> exists q6 : nat, 1 = 6 * q6 *)
    intros [ | q2'] H_q2.
    + discriminate H_q2.
    + rewrite -> two_times_S in H_q2.
      discriminate H_q2.
  - (* forall q2 : nat, 2 = 2 * q2 -> forall q3 : nat, 2 = 3 * q3 -> exists q6 : nat, 2 = 6 * q6 *)
    intros _ _ [ | q3'] H_q3.
    * discriminate H_q3.
    * rewrite -> three_times_S in H_q3.
      discriminate H_q3.
  - (* forall q2 : nat, 3 = 2 * q2 -> forall q3 : nat, 3 = 3 * q3 -> exists q6 : nat, 3 = 6 * q6 *)
    intros [ | [ | q2']] H_q2.
    + discriminate H_q2.
    + discriminate H_q2.
    + rewrite ->2 two_times_S in H_q2.
      discriminate H_q2.
  - (* forall q2 : nat, 4 = 2 * q2 -> forall q3 : nat, 4 = 3 * q3 -> exists q6 : nat, 4 = 6 * q6 *)
    intros _ _ [ | [ | q3']] H_q3.
    * discriminate H_q3.
    * discriminate H_q3.
    * rewrite ->2 three_times_S in H_q3.
      discriminate H_q3.
  - (* forall q2 : nat, 5 = 2 * q2 -> forall q3 : nat, 5 = 3 * q3 -> exists q6 : nat, 5 = 6 * q6 *)
    intros [ | [ | [ | q2']]] H_q2.
    + discriminate H_q2.
    + discriminate H_q2.
    + discriminate H_q2.
    + rewrite ->3 two_times_S in H_q2.
      discriminate H_q2.
  - (* forall q2 : nat, S (S (S (S (S (S n'))))) = 2 * q2 -> forall q3 : nat, S (S (S (S (S (S n'))))) = 3 * q3 -> exists q6 : nat, S (S (S (S (S (S n'))))) = 6 * q6 *)
    intros [ | [ | [ | q2']]] H_q2.
    + discriminate H_q2.
    + discriminate H_q2.
    + discriminate H_q2.
    + rewrite ->3 two_times_S in H_q2.
      rewrite -> Nat.mul_comm in H_q2; injection H_q2 as H_q2; rewrite -> Nat.mul_comm in H_q2.
      intros [ | [ | q3']] H_q3.
      * discriminate H_q3.
      * discriminate H_q3.
      * rewrite ->2 three_times_S in H_q3.
        rewrite -> Nat.mul_comm in H_q3; injection H_q3 as H_q3; rewrite -> Nat.mul_comm in H_q3.
        destruct (IHn' q2' H_q2 q3' H_q3) as [q6' H_q6'].
        rewrite -> H_q6'.
        rewrite <- six_times_S.
        exists (S q6').
        reflexivity.
Qed.

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

(* Exercise 16 *)

Property a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_directly_swapped :
  forall (n : nat)
         (q3 : nat),
    n = 3 * q3 ->
    forall q2 : nat,
      n = 2 * q2 ->
      exists q6 : nat,
        n = 6 * q6.
Proof.
  intros n q3 H_q3 q2 H_q2.
  exact (a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_directly n q2 H_q2 q3 H_q3).

  Restart.

  intros n.
  induction n as [ | | | | | | n' IHn'] using nat_ind6_0.
Abort.

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

(* end of week-11_induction-principles-colon-from-first-order-to-higher-order-induction.v *)