(* week-11_induction-principles-colon-course-of-values-induction.v *)
(* Time-stamp: <2025-07-02 14:42:26 olivier> *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 02 Jul 2025 *)

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

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

Require Import Arith Bool.

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

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

(* ***** *)

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

(* ***** *)

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

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

(* Let us turn to course-of-values induction: *)

Fixpoint conjunction_upto (n : nat) (P : nat -> Prop) : Prop :=
  match n with
  | 0 =>
    P 0
  | S n' =>
    P (S n') /\ conjunction_upto n' P
end.

Lemma fold_unfold_conjunction_upto_O :
  forall P : nat -> Prop,
    conjunction_upto 0 P =
    P 0.
Proof.
  fold_unfold_tactic conjunction_upto.
Qed.

Lemma fold_unfold_conjunction_upto_S :
  forall (n' : nat)
         (P : nat -> Prop),
    conjunction_upto (S n') P =
    (P (S n') /\ conjunction_upto n' P).
Proof.
  fold_unfold_tactic conjunction_upto.
Qed.

Property sketchy_characterization_of_conjunction_upto :
  forall P : nat -> Prop,
    (conjunction_upto 0 P = (P 0))
    /\
    (conjunction_upto 1 P = (P 1 /\ P 0))
    /\
    (conjunction_upto 2 P = (P 2 /\ P 1 /\ P 0))
    /\
    (conjunction_upto 3 P = (P 3 /\ P 2 /\ P 1 /\ P 0)).
Proof.
  intro P.
  unfold conjunction_upto.
  split; [ | split; [ | split]]; reflexivity.
Qed.

(* ***** *)

Lemma conjunction_upto_a_number_implies_the_property_at_this_number :
  forall (n : nat)
         (P : nat -> Prop),
    conjunction_upto n P ->
    P n.
Proof.
  intros [ | n'] P CU_n_P.
  - rewrite -> fold_unfold_conjunction_upto_O in CU_n_P.
    exact CU_n_P.
  - rewrite -> fold_unfold_conjunction_upto_S in CU_n_P.
    destruct CU_n_P as [ly _].
    exact ly.
Qed.

Lemma conjunction_upto_a_number_implies_the_property_at_O :
  forall (n : nat)
         (P : nat -> Prop),
    conjunction_upto n P ->
    P 0.
Proof.
  intros n P.
  induction n as [ | n' IHn']; intro CU_n_P.
  - rewrite -> fold_unfold_conjunction_upto_O in CU_n_P.
    exact CU_n_P.
  - rewrite -> fold_unfold_conjunction_upto_S in CU_n_P.
    destruct CU_n_P as [_ CU_n'_P].
    exact (IHn' CU_n'_P).
Qed.

Lemma conjunction_upto_an_addition_implies_conjunction_upto_the_addend :
  forall (k1 k2 : nat)
         (P : nat -> Prop),
    conjunction_upto (k1 + k2) P ->
    conjunction_upto k2 P.
Proof.
  intros k1 k2 P.
  induction k1 as [ | k1' IHk1'].
  - rewrite -> Nat.add_0_l.
    intro H_k2; exact H_k2.
  - rewrite -> (plus_Sn_m k1' k2).
    rewrite -> fold_unfold_conjunction_upto_S.
    intros [H H_k2].
    exact (IHk1' H_k2).
Qed.

Corollary conjunction_upto_a_number_implies_the_property_at_O_as_a_corollary :
  forall (n : nat)
         (P : nat -> Prop),
    conjunction_upto n P ->
    P 0.
Proof.
  intros n P CU_n_P.
  rewrite <- (Nat.add_0_r n) in CU_n_P.
  assert (CU_0_P := conjunction_upto_an_addition_implies_conjunction_upto_the_addend n 0 P CU_n_P).
  rewrite -> fold_unfold_conjunction_upto_O in CU_0_P.
  exact CU_0_P.
Qed.

(* ***** *)

Lemma nat_ind_course_of_values :
  forall P : nat -> Prop,
    P 0 ->
    (forall n' : nat,
        conjunction_upto n' P -> P (S n')) ->
    forall n : nat,
      P n.
Proof.
  intros P P_O P_S.
  intros [ | n'].
  - exact P_O.
  - apply (P_S n').
    induction n' as [ | n'' IHn''].
    + rewrite -> fold_unfold_conjunction_upto_O.
      exact P_O.
    + rewrite -> fold_unfold_conjunction_upto_S.
      Check (P_S n'').
      Check (P_S n'' IHn'').
      exact (conj (P_S n'' IHn'') IHn'').
Qed.

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

(* Exercise 17 *)

Lemma nat_ind1_using_nat_ind_course_of_values :
  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'] using nat_ind_course_of_values.
  - exact P_0.
  - Check (P_S n').
    Check (conjunction_upto_a_number_implies_the_property_at_this_number n' P IHn').
    Check (P_S n' (conjunction_upto_a_number_implies_the_property_at_this_number n' P IHn')).
    exact (P_S n' (conjunction_upto_a_number_implies_the_property_at_this_number n' P IHn')).

  Restart.

  intros P P_0 P_S n.
  induction n as [ | [ | n'] IHn'] using nat_ind_course_of_values.
  - exact P_0.
  - exact (P_S 0 P_0).
  - rewrite -> fold_unfold_conjunction_upto_S in IHn'.
    destruct IHn' as [P_Sn' _].
    exact (P_S (S n') P_Sn').
Qed.

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

(* Exercise 18 *)

(* ***** *)

(* Exercise 18a *)

Lemma nat_ind2_using_nat_ind_course_of_values :
  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 n.
  induction n as [ | [ | n'] IHn'] using nat_ind_course_of_values.
  - exact P_0.
  - exact P_1.
  - destruct IHn' as [P_Sn' CU_n'_P].
    exact (P_SS n' (conjunction_upto_a_number_implies_the_property_at_this_number n' P CU_n'_P) P_Sn').
Qed.

(* ***** *)

(* Exercise 18b *)

Lemma nat_ind2_0_using_nat_ind_course_of_values :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    (forall n' : nat,
        P n' ->
        P (S (S n'))) ->
    forall n : nat,
      P n.
Proof.
  intros P P_0 P_1 P_SS n.
  induction n as [ | [ | n'] IHn'] using nat_ind_course_of_values.
  - exact P_0.
  - exact P_1.
  - rewrite -> fold_unfold_conjunction_upto_S in IHn'.
    destruct IHn' as [P_Sn' CU_n'_P].
    Check (conjunction_upto_a_number_implies_the_property_at_this_number n' P CU_n'_P).
    exact (P_SS n' (conjunction_upto_a_number_implies_the_property_at_this_number n' P CU_n'_P)).
Qed.

(* ***** *)

(* Exercise 18c *)

Lemma nat_ind2_1_using_nat_ind_course_of_values :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    (forall n' : nat,
        P (S n') ->
        P (S (S n'))) ->
    forall n : nat,
      P n.
Proof.
  intros P P_0 P_1 P_SS n.
  induction n as [ | [ | n'] IHn'] using nat_ind_course_of_values.
  - exact P_0.
  - exact P_1.
  - Check (conjunction_upto_a_number_implies_the_property_at_this_number (S n') P IHn').
    exact (P_SS n' (conjunction_upto_a_number_implies_the_property_at_this_number (S n') P IHn')).
Qed.

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

(* Exercise 19 *)

Lemma nat_ind3_using_nat_ind_course_of_values :
  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.

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

(* Exercise 20 *)

Lemma nat_ind4_using_nat_ind_course_of_values :
  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.
Abort.

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

(* Exercise 21 *)

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_1 :
  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,
    S (S (2 * n)) = 2 * S n.
Proof.
  intro n.
  ring.
Qed.

Lemma first_base_case_for_soundness_and_completeness_of_evenp2 :
  evenp2 0 = true <-> (exists m : nat, 0 = 2 * m).
Proof.
Admitted.

Lemma second_base_case_for_soundness_and_completeness_of_evenp2 :
  evenp2 1 = true <-> (exists m : nat, 1 = 2 * m).
Proof.
Admitted.

Lemma common_part_of_induction_step_for_soundness_and_completeness_of_evenp2 :
  forall (n' : nat)
         (IHn'_sound : evenp2 n' = true -> exists m : nat, n' = 2 * m)
         (IHn'_complete : (exists m : nat, n' = 2 * m) -> evenp2 n' = true),
    evenp2 n' = true <-> (exists m : nat, S (S n') = 2 * m).
Proof.
Abort.

Theorem soundness_and_completeness_of_evenp2_using_nat_ind_course_of_values :
  forall n : nat,
    evenp2 n = true <-> exists m : nat, n = 2 * m.
Proof.
  intro n.
  induction n as [ | [ | n'] IHn'] using nat_ind_course_of_values.
  - exact first_base_case_for_soundness_and_completeness_of_evenp2.
  - exact second_base_case_for_soundness_and_completeness_of_evenp2.
  - admit.
Abort.

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

(* Exercise 22 *)

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_ind_course_of_values :
  forall n : nat,
    ternaryp n = true <-> exists m : nat, n = 3 * m.
Proof.
Abort.

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

(* Exercise 23 *)

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

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

(* Exercise 24 *)

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

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

(* end of week-11_induction-principles-colon-course-of-values-induction.v *)