(* week-03_specifications.v *)
(* LPP 2023 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 01 Feb 2024 *)

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

(* Paraphernalia: *)

Require Import Arith.

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

Definition recursive_specification_of_addition (add : nat -> nat -> nat) :=
  (forall y : nat,
      add O y = y)
  /\
  (forall x' y : nat,
      add (S x') y = S (add x' y)).

Definition lambda_dropped_recursive_specification_of_addition (add : nat -> nat -> nat) :=
  (forall y : nat,
      add 0 y = y
                /\ forall x' : nat,
          add (S x') y = S (add x' y)).

Proposition there_is_at_most_one_recursive_addition :
  forall add1 add2 : nat -> nat -> nat,
    recursive_specification_of_addition add1 ->
    recursive_specification_of_addition add2 ->
    forall x y : nat,
      add1 x y = add2 x y.
Proof.
  intros add1 add2.
  unfold recursive_specification_of_addition.
  intros [H_add1_0 H_add1_S].
  intros [H_add2_0 H_add2_S].
  intro x.
  induction x as [| x' IHx].
  - intro y.
    rewrite H_add1_0.
    rewrite H_add2_0.
    reflexivity.
  - intro y.
    rewrite H_add1_S.
    rewrite H_add2_S.
    rewrite IHx.
    reflexivity.

  Restart.
  intros add1 add2.
  unfold recursive_specification_of_addition.
  intros [H_add1_O H_add1_S] [H_add2_O H_add2_S].
  intro x.

  induction x as [| x' IHx'].
  - intro y.
    rewrite -> (H_add2_O y).
    Check (H_add1_O y).
    exact (H_add1_O y).
  - intro y.
    rewrite -> (H_add1_S x' y).
    rewrite -> (H_add2_S x' y).

    Check (IHx' y).
    rewrite -> (IHx' y).
    reflexivity.
Qed.

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

Definition tail_recursive_specification_of_addition (add : nat -> nat -> nat) :=
  (forall y : nat,
      add O y = y)
  /\
  (forall x' y : nat,
      add (S x') y = add x' (S y)).

(* ***** *)

(* Exercise 01 *)

Proposition there_is_at_most_one_tail_recursive_addition :
  forall add1 add2 : nat -> nat -> nat,
    tail_recursive_specification_of_addition add1 ->
    tail_recursive_specification_of_addition add2 ->
    forall x y : nat,
      add1 x y = add2 x y.
Proof.
  intros add1 add2.
  unfold tail_recursive_specification_of_addition.
  intros [H_add1_O H_add1_S] [H_add2_O H_add2_S].
  intros x y.
  induction x as [| x' IHx'].
  - rewrite -> (H_add2_O y).
    exact (H_add1_O y).

  - rewrite -> (H_add1_S x' y).
    rewrite -> (H_add2_S x' y).
    (* rewrite -> (IHx' (S y)). *)

  Restart.
  intros add1 add2.
  unfold tail_recursive_specification_of_addition.
  intros [H_add1_O H_add1_S] [H_add2_O H_add2_S].
  intro x.
  induction x as [| x' IHx'].
  - intro y.
    rewrite -> (H_add2_O y).
    exact (H_add1_O y).
  - intro y.
    rewrite -> (H_add1_S x' y).
    rewrite -> (H_add2_S x' y).
    rewrite -> (IHx' (S y)).
    reflexivity.
Qed.

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

Definition specification_of_the_predecessor_function (pred : nat -> nat) :=
  forall n : nat,
    pred (S n) = n.

Proposition there_is_at_most_one_predecessor_function :
  forall pred1 pred2 : nat -> nat,
    specification_of_the_predecessor_function pred1 ->
    specification_of_the_predecessor_function pred2 ->
    forall n : nat,
      pred1 n = pred2 n.
Proof.
  intros pred1 pred2.
  unfold specification_of_the_predecessor_function.
  intros H_pred1_S H_pred2_S.
  intro n.
  induction n as [ | n' IHn'].
Abort.

Definition make_predecessor_function (zero n : nat) :=
  match n with
  | 0 => zero
  | S n' => n'
  end.

Lemma about_make_predecessor_function :
  forall zero : nat,
    specification_of_the_predecessor_function (make_predecessor_function zero).
Proof.
  intro zero.
  unfold specification_of_the_predecessor_function.
  induction n as [| n' IHn' ].

  - unfold make_predecessor_function.
    reflexivity.
  - unfold make_predecessor_function.
    reflexivity.
Qed.

Theorem there_are_at_least_two_predecessor_functions :
  exists pred1 pred2 : nat -> nat,
    specification_of_the_predecessor_function pred1 /\
    specification_of_the_predecessor_function pred2 /\
    exists n : nat,
      pred1 n <> pred2 n.
Proof.
  exists (make_predecessor_function 0).
  exists (make_predecessor_function 1).
  split.

  - exact (about_make_predecessor_function 0).

  - split.

    -- exact (about_make_predecessor_function 0).


    -- exists 0.
       unfold make_predecessor_function.
       Search (_ <> S _).
       Check (n_Sn 0).
       exact (n_Sn 0).
Qed.

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

Definition specification_of_the_total_predecessor_function (pred : nat -> option nat) :=
  (pred 0 = None)
  /\
  (forall n : nat,
      pred (S n) = Some n).

(* ***** *)

(* Exercise 02 *)

Proposition there_is_at_most_one_total_predecessor_function :
  forall pred1 pred2 : nat -> option nat,
    specification_of_the_total_predecessor_function pred1 ->
    specification_of_the_total_predecessor_function pred2 ->
    forall n : nat,
      pred1 n = pred2 n.
Proof.
  intros pred1 pred2.
  unfold specification_of_the_total_predecessor_function.
  intros [H_pred1_O H_pred1_S] [H_pred2_O H_pred2_S].
  intro n.
  induction n as [ | n' IHn'].

  - rewrite -> H_pred2_O.
    exact H_pred1_O.

  - rewrite -> (H_pred2_S n').
    exact (H_pred1_S n').

  Restart.

  intros pred1 pred2.
  unfold specification_of_the_total_predecessor_function.
  intros [H_pred1_O H_pred1_S] [H_pred2_O H_pred2_S].
  intros [ | n'].

  - rewrite -> H_pred2_O.
    exact H_pred1_O.

  - rewrite -> (H_pred2_S n').
    exact (H_pred1_S n').  
Qed.

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

Definition specification_of_the_predecessor_and_successor_function (ps : nat -> nat) :=
  (forall n : nat,
      ps (S n) = n)
  /\
  (forall n : nat,
      ps n = (S n)).

(* ***** *)

(* Exercise 03 *)

Theorem there_is_at_most_one_predecessor_and_successor_function :
  forall ps1 ps2 : nat -> nat,
    specification_of_the_predecessor_and_successor_function ps1 ->
    specification_of_the_predecessor_and_successor_function ps2 ->
    forall n : nat,
      ps1 n = ps2 n.
Proof.
  intros ps1 ps2.
  unfold specification_of_the_predecessor_and_successor_function.
  intros [H_ps1_Sn_n H_ps1_n_Sn] [H_ps2_Sn_n H_ps2_n_Sn].
  induction n as [| n' IHn'].
  - Check (H_ps1_n_Sn 0).
    rewrite (H_ps1_n_Sn 0).
    rewrite (H_ps2_n_Sn 0).
    reflexivity.
  - rewrite -> (H_ps1_Sn_n  n').
    rewrite -> (H_ps2_Sn_n  n').
    reflexivity.

Abort.

(* ***** *)

Lemma a_contradictory_aspect_of_the_predecessor_and_successor_function :
  forall ps : nat -> nat,
    specification_of_the_predecessor_and_successor_function ps ->
    ps 1 = 0 /\ ps 1 = 2.
Proof.
  intro ps.
  unfold specification_of_the_predecessor_and_successor_function.
  intros [H_ps_S H_ps].
  split.

  - rewrite -> (H_ps_S 0).
    reflexivity.

  - rewrite -> (H_ps 1).
    reflexivity.
Qed.

Theorem there_are_zero_predecessor_and_successor_functions :
  forall ps : nat -> nat,
    specification_of_the_predecessor_and_successor_function ps ->
    exists n : nat,
      ps n <> ps n.
Proof.
  intros ps S_ps.
  Check (a_contradictory_aspect_of_the_predecessor_and_successor_function ps S_ps).
  destruct (a_contradictory_aspect_of_the_predecessor_and_successor_function ps S_ps) as [H_ps_0 H_ps_2].
  exists 1.
  rewrite -> H_ps_0.

  Restart.

  intros ps S_ps.
  Check (a_contradictory_aspect_of_the_predecessor_and_successor_function ps S_ps).
  destruct (a_contradictory_aspect_of_the_predecessor_and_successor_function ps S_ps) as [H_ps_0 H_ps_2].
  exists 1.
  rewrite -> H_ps_0 at 1.
  rewrite -> H_ps_2.
  Search (0 <> S _).
  Check (O_S 1).
  exact (O_S 1).
Qed.

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

Theorem the_resident_addition_function_satisfies_the_recursive_specification_of_addition :
  recursive_specification_of_addition Nat.add.
Proof.
  unfold recursive_specification_of_addition.
  split.
  - intro y.
    Search (0 + _ = _).
    exact (Nat.add_0_l y).
  - intros x' y.
    Search (S _ + _ = S (_ + _)).
    exact (Nat.add_succ_l x' y).
Qed.

(* ***** *)

(* Exercise 04 *)

Theorem the_resident_addition_function_satisfies_the_tail_recursive_specification_of_addition :
  tail_recursive_specification_of_addition Nat.add.
Proof.
  unfold tail_recursive_specification_of_addition.
  split.
  - intro y.
    exact (Nat.add_0_l y).
  - intros x' y.
    Search (S _ + _ = _ + S _).
    exact (Nat.add_succ_comm x' y).

Qed.

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

(* Exercise 05 *)

Theorem the_two_specifications_of_addition_are_equivalent :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add <-> tail_recursive_specification_of_addition add.
Proof.
  intro add.
  unfold recursive_specification_of_addition.
  unfold tail_recursive_specification_of_addition.
  split.
  - intros [H_add_O H_add_S].
    split.
    * exact H_add_O.
    * intros x'.
      induction x' as [| x'' IHx''].
      + intro y.
        Check (H_add_S 0 y).
        rewrite -> (H_add_S 0 y).
        rewrite -> (H_add_O y).
        rewrite -> (H_add_O (S y)).
        reflexivity.
      + intro y.
        rewrite -> (H_add_S (S x'') y).
        rewrite -> (H_add_S  x'' (S y)).
        rewrite IHx''.
        reflexivity.
  - intros [H_add_O H_add_S].
    split.
    * exact H_add_O.
    * intro x'.
      induction x' as [| x'' IHx''].
      + intro y.
        rewrite -> (H_add_O y).
        rewrite -> (H_add_S 0 y).
        rewrite -> (H_add_O (S y)).
        reflexivity.
      + intro y.
        rewrite -> (H_add_S (S x'') y).
        rewrite -> (IHx'' (S y)).
        rewrite <- (H_add_S x'' y).
        reflexivity.
Qed.


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

(* Exercise 06a *)

Theorem associativity_of_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n1 n2 n3 : nat,
      add n1 (add n2 n3) = add (add n1 n2) n3.
Proof.
  intro add.
  unfold recursive_specification_of_addition.
  intros [H_add_O H_add_S].
  intros x.
  induction x as [| x' IHx'].
  - intros y z.
    rewrite (H_add_O (add y z)).
    rewrite (H_add_O y).
    reflexivity.
  - intros y z.
    rewrite -> (H_add_S x' (add y z)).
    rewrite -> (H_add_S x' y).
    rewrite -> (H_add_S (add x' y) z).
    rewrite -> IHx'.
    reflexivity.
Qed.
Lemma about_the_tail_recursive_addition_function :
  forall add: nat -> nat -> nat,
    tail_recursive_specification_of_addition add ->
    forall x y : nat,
      add (S x) y = S (add x y).
Proof.
  intro add.
  unfold tail_recursive_specification_of_addition.
  intros [H_add_O H_add_S].
  intro x.
  induction x as [| x' IHx'].
  - intro y.
    rewrite -> (H_add_O y).
    rewrite -> (H_add_S 0 y).
    rewrite -> (H_add_O (S y)).
    reflexivity.
  - intro y.
    rewrite -> (H_add_S x' y).
    rewrite <- (IHx' (S y)).
    rewrite -> (H_add_S (S x') y).
    reflexivity.
  Qed.

Theorem associativity_of_tail_recursive_addition :
  forall add : nat -> nat -> nat,
    tail_recursive_specification_of_addition add ->
    forall n1 n2 n3 : nat,
      add n1 (add n2 n3) = add (add n1 n2) n3.
Proof.
  intros add H_add.
  assert (H_tmp := H_add).
  destruct H_tmp as [H_add_O H_add_S].
  intros x.
  induction x as [| x' IHx'].
  - intros y z.
    rewrite (H_add_O (add y z)).
    rewrite (H_add_O y).
    reflexivity.
  - intros y z.
    rewrite -> (H_add_S x' (add y z)).
    rewrite -> (H_add_S x' y).
    rewrite <- (IHx' (S y) z).
    rewrite -> (about_the_tail_recursive_addition_function add H_add y z).
    reflexivity.
    Qed.


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

(* Exercise 07 *)

Lemma commutativity_of_recursive_addition_O :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n : nat,
      add n O = n.
Proof.
  intro add.
  unfold recursive_specification_of_addition.
  intros [H_add_O H_add_S].
  intro n.
  induction n as [| n' IHn'].
  - exact (H_add_O 0).
  - rewrite -> (H_add_S n' 0).
    rewrite -> IHn'.
    reflexivity.
Qed.

Lemma commutativity_of_recursive_addition_S :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n1 n2 : nat,
      add n1 (S n2) = S (add n1 n2).
Proof.
  intros add H_add.
  assert (H_tmp := H_add).
  unfold recursive_specification_of_addition.
  destruct H_tmp as [H_add_O H_add_S].
  intro x.
  induction x as [| x' IHx'].
  - intro y.
    rewrite (H_add_O (S y)).
    rewrite (H_add_O y).
    reflexivity.
  - intro y.
    rewrite -> (H_add_S x' (S y)).
    rewrite -> (IHx' y).
    rewrite -> (H_add_S x' y).
    reflexivity.
Qed.

Theorem commutativity_of_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n1 n2 : nat,
      add n1 n2 = add n2 n1.
Proof.
  intros add S_add.
  assert (H_add_O := commutativity_of_recursive_addition_O add S_add).
  assert (H_add_S := commutativity_of_recursive_addition_S add S_add).
  unfold recursive_specification_of_addition in S_add.
  destruct S_add as [S_add_O S_add_S].
  intro x.
  induction x as [| x' IHx'].
  - intro y.
    rewrite -> (S_add_O y).
    rewrite -> (H_add_O y).
    reflexivity.
  - intro y.
    rewrite -> (S_add_S x' y).
    rewrite -> (H_add_S  y).
    rewrite -> (IHx' y).
    reflexivity.
Qed.

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

(* Exercise 08a *)

Theorem O_is_left_neutral_for_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n : nat,
      add 0 n = n.
Proof.
  intros add.
  unfold recursive_specification_of_addition.
  intros [H_add_O _].
  exact H_add_O.
Qed.

(* ***** *)

(* Exercise 08b *)

Theorem O_is_right_neutral_for_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n : nat,
      add n 0 = n.
Proof.
  intros add S_add.
  unfold recursive_specification_of_addition in S_add.
  intro n.
  rewrite -> (commutativity_of_recursive_addition add S_add n).
  rewrite -> (O_is_left_neutral_for_recursive_addition add S_add n).
  reflexivity.
Qed.

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

(* Exercise 08c *)
Theorem O_is_left_neutral_for_tail_recursive_addition :
  forall add : nat -> nat -> nat,
    tail_recursive_specification_of_addition add ->
    forall n : nat,
      add 0 n = n.
Proof.
  intros add.
  unfold tail_recursive_specification_of_addition.
  intros [H_add_O _].
  exact H_add_O.
Qed.
Theorem O_is_right_neutral_for_tail_recursive_addition :
  forall add : nat -> nat -> nat,
    tail_recursive_specification_of_addition add ->
    forall n: nat,
      add n 0 = n.
Proof.
  Admitted.
(* end of week-03_specifications.v *)
