(* mini-project-about-fourth-order-induction.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 04 Jun 2025 *)

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

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

Require Import Arith Bool.

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

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.
  intros P P_0 P_1 P_2 P_3 P_SSSS.
  assert (all4 :
            forall n : nat,
              P n /\ P (S n) /\ P (S (S n)) /\ P (S (S (S n)))).
  { intro n.
    induction n as [ | n' [IHn' [IHSn' [IHSSn' IHSSSn']]]].
    - exact (conj P_0 (conj P_1 (conj P_2 P_3))).
    - Check (P_SSSS n' IHn' IHSn' IHSSn' IHSSSn').
      exact (conj IHSn' (conj IHSSn' (conj IHSSSn' (P_SSSS n' IHn' IHSn' IHSSn' IHSSSn')))). }
  intro n.
  destruct (all4 n) as [ly _].
  exact ly.
Qed.

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

(* Task 0 *)

Property fours_and_threes :
  forall n : nat,
  exists a b : nat,
    6 + n = 4 * a + 3 * b.
Proof.
Admitted.

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

(* Task 1 *)

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

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

(* Task 2 *)

Property fours_and_sevens :
  forall n : nat,
  exists a b : nat,
    18 + n = 4 * a + 7 * b.
Proof.
Admitted.

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

(* Task 3 *)

Property fours_and_nines :
  forall n : nat,
  exists a b : nat,
    24 + n = 4 * a + 9 * b.
Proof.
Admitted.

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

(* Task 4 *)

(* Property fours_and_elevens :
  forall n : nat,
  exists a b : nat,
    ?? + n = 4 * a + 11 * b.
Proof. *)

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

(* Task 5 *)

(* Property fours_and_an_odd_number_that_is_larger_than_1 :
  forall m n : nat,
  exists a b : nat,
    ?? + n = 4 * a + S (2 * S m) * b.
Proof.
  intros [ | [ | [ | [ | [ | m']]]]] n.
  - simpl (...).
    simpl (S (2 * 1)).
    exact (fours_and_threes n).
  - simpl (...).
    simpl (S (2 * 2)).
    exact (fours_and_fives n).
  - simpl (...).
    simpl (S (2 * 3)).
    exact (fours_and_sevens n).
  - simpl (...).
    simpl (S (2 * 4)).
    exact (fours_and_nines n).
  - simpl (...).
    simpl (S (2 * 5)).
    exact (fours_and_elevens n).

  Restart. *)

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

(* end of mini-project-about-fourth-order-induction.v *)