(* week-07_existential-declarations-revisited.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 05 Jun 2025 *)

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

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

Require Import Arith Bool.

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

Lemma truism :
  forall P : nat -> Prop,
    (exists n : nat,
        P n) ->
    exists n : nat,
      P n.
Proof.
  intros P H_P.
  exact H_P.

  Restart.

  intros P H_P.
  destruct H_P as [n H_Pn].
  exists n.
  exact H_Pn.

  Restart.

  intros P [n H_Pn].
  exists n.
  exact H_Pn.
Qed.

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

Fixpoint power (x n : nat) : nat :=
  match n with
    O =>
    1
  | S n' =>
    x * power x n'
  end.

Lemma fold_unfold_power_O :
  forall x : nat,
    power x O =
    1.
Proof.
  fold_unfold_tactic power.
Qed.

Lemma fold_unfold_power_S :
  forall x n' : nat,
    power x (S n') =
    x * power x n'.
Proof.
  fold_unfold_tactic power.
Qed.

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

(* Exercise 01 *)

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

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

Property all_powers_of_4_are_post_ternary :
  forall n : nat,
  exists q : nat,
    power 4 n = S (3 * q).
Proof.
  intro n.
  induction n as [ | n' IHn'].
  - rewrite -> (fold_unfold_power_O 4).
    exists 0.
    compute.
    reflexivity.
  - rewrite -> (fold_unfold_power_S 4 n').
    destruct IHn' as [q' H_q'].

  Restart.

  intro n.
  induction n as [ | n' [q' H_q']].
  - rewrite -> (fold_unfold_power_O 4).
    exists 0.
    compute.
    reflexivity.
  - rewrite -> (fold_unfold_power_S 4 n').
    rewrite -> H_q'.
    rewrite -> (four_times_S (3 * q')).
    Search (_ * (_ * _)).
(* Nat.mul_shuffle3: forall n m p : nat, n * (m * p) = m * (n * p) *)
    rewrite -> (Nat.mul_shuffle3 4 3 q').
    rewrite <- (three_times_S (4 * q')).
    exists (S (4 * q')).
    reflexivity.
Qed.

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

(* Exercise 02 *)

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

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

Property all_powers_of_10_follow_a_multiple_of_9 :
  forall n : nat,
  exists q : nat,
    power 10 n = S (9 * q).
Proof.
Abort.

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

(* Exercise 03 *)

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

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

Property all_powers_of_8_follow_a_multiple_of_7 :
  forall n : nat,
  exists q : nat,
    power 8 n = S (7 * q).
Proof.
Abort.

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

(* Exercise 04 *)

Property about_exponentiating_one :
  forall n : nat,
    power 1 n = 1.
Proof.
Abort.

Property all_powers_of_Sm_follow_a_multiple_of_m :
  forall m n : nat,
  exists q : nat,
    power (S m) n = S (m * q).
Proof.
Abort.

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

(* end of week-07_existential-declarations-revisited.v *)