(* week-05_more-about-soundness-and-completeness.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 06 Jun 2025, with Exercise 07 *)
(* was: *)
(* Version of 13 Feb 2025 *)

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

(* 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)).

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

Lemma about_a_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall i j : nat,
      add i j = i + j.
Proof.
  intro add.
  unfold recursive_specification_of_addition.
  intros [S_add_O S_add_S] i.
  induction i as [ | i' IHi'].
  - intro j.
    rewrite -> (Nat.add_0_l j).
    exact (S_add_O j).
  - intro j.
    rewrite -> (S_add_S i' j).
    Check (plus_Sn_m i' j).
    rewrite -> (plus_Sn_m i' j).
    rewrite -> (IHi' j).
    reflexivity.
Qed.

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

Proposition soundness_of_recursive_addition_with_respect_to_the_resident_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall i j k : nat,
      add i j = k ->
      k = i + j.
Proof.
  intros add S_add i j k H_k.
  rewrite <- H_k.
  exact (about_a_recursive_addition add S_add i j).
Qed.

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

Proposition completeness_of_recursive_addition_with_respect_to_the_resident_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall i j k : nat,
      i + j = k ->
      k = add i j.
Proof.
  intros add S_add i j k H_k.
  rewrite <- H_k.
  symmetry.
  exact (about_a_recursive_addition add S_add i j).
Qed.

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

Lemma about_decomposing_a_pair_using_the_injection_tactic :
  forall i j : nat,
    (i, j) = (0, 1) ->
    i = 0 /\ j = 1.
Proof.
  intros i j H_ij.
  injection H_ij.
  
  Restart.

  intros i j H_ij.
  injection H_ij as H_i H_j.
  exact (conj H_i H_j).
Qed.

Lemma about_decomposing_a_pair_using_the_injection_tactic' :
  forall i j : nat,
    (i, 1) = (0, j) ->
    i = 0 /\ j = 1.
Proof.
  intros i j H_ij.
  injection H_ij as H_i H_j.
  symmetry in H_j.
  exact (conj H_i H_j).
Qed.

Lemma about_decomposing_a_pair_of_pairs_using_the_injection_tactic :
  forall a b c d: nat,
    ((a, 1), (2, d)) = ((0, b), (c, 3)) ->
    a = 0 /\ b = 1 /\ c = 2 /\ d = 3.
Proof.
  intros a b c d H_abcd.
  injection H_abcd as H_a H_b H_c H_d.
  symmetry in H_b.
  symmetry in H_c.
  exact (conj H_a (conj H_b (conj H_c H_d))).
Qed.

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

Proposition true_is_not_false :
  true <> false.
Proof.
  unfold not.
  intro H_absurd.
  discriminate H_absurd.
Qed.

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

Proposition now_what :
  (forall n : nat, n = S n) <-> 0 = 1.
Proof.
  split.

  - intro H_n_Sn.
    Check (H_n_Sn 0).
    exact (H_n_Sn 0).
    
  - intro H_absurd.
    discriminate H_absurd.

  Restart.

  split.

  - intro H_n_Sn.
    Check (H_n_Sn 42).
    discriminate (H_n_Sn 42).

  - intro H_absurd.
    discriminate H_absurd.
Qed.

Proposition what_now :
  forall n : nat,
    n = S n <-> 0 = 1.
Proof.
  intro n.
  split.

  - intro H_n.
    Search (_ <> S _).
    Check (n_Sn n).
    assert (H_tmp := n_Sn n).
    unfold not in H_tmp.
    Check (H_tmp H_n).
    contradiction (H_tmp H_n).

  - intro H_absurd.
    discriminate H_absurd.
Qed.

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

(* Exercise 07 *)

Property False_implies_anything :
  forall A : Prop,
    False -> A.
Proof.
Abort.

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

Proposition soundness_of_recursive_addition_with_respect_to_the_resident_addition_revisited :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall i j k : nat,
      add i j = k ->
      k = i + j.
Proof.
  intro add.
  unfold recursive_specification_of_addition.
  intros [S_add_O S_add_S] i.
  induction i as [ | i' IHi'].
  - intros j k H_add.
    rewrite -> (S_add_O j) in H_add.
    rewrite -> H_add.
    exact (eq_sym (Nat.add_0_l k)).
  - intros j k H_add.
    rewrite -> (S_add_S i' j) in H_add.
    case k as [ | k'].
    + discriminate H_add.
    + injection H_add as H_add.
      Check (IHi' j k').
      Check (IHi' j k' H_add).
      rewrite -> (IHi' j k' H_add).
      Check plus_Sn_m.
      exact (eq_sym (plus_Sn_m i' j)).
Qed.

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

Proposition completeness_of_recursive_addition_revisited :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall i j k : nat,
      i + j = k ->
      add i j = k.
Proof.
  intro add.
  unfold recursive_specification_of_addition.
  intros [S_add_O S_add_S] i j.
  induction i as [ | i' IHi'].
  - intros k H_k.
    rewrite -> (Nat.add_0_l j) in H_k.
    rewrite <- H_k.
    exact (S_add_O j).
  - intros k H_k.
    rewrite -> (S_add_S i' j).
    rewrite -> (plus_Sn_m i' j) in H_k.
    case k as [ | k'].
    + discriminate H_k.
    + injection H_k as H_k.
      Check (IHi' k').
      Check (IHi' k' H_k).
      rewrite <- (IHi' k' H_k).
      reflexivity.

  Restart.

  intro add.
  unfold recursive_specification_of_addition.
  intros [S_add_O S_add_S] i j.
  induction i as [ | i' IHi'].
  - intros k H_k.
    rewrite -> (Nat.add_0_l j) in H_k.
    rewrite <- H_k.
    exact (S_add_O j).
  - intros k H_k.
    rewrite -> (S_add_S i' j).
    rewrite -> (plus_Sn_m i' j) in H_k.
    Check (IHi' (i' + j)).
    Check (IHi' (i' + j) (eq_refl (i' + j))).
    rewrite -> (IHi' (i' + j) (eq_refl (i' + j))).
    exact H_k.
Qed.

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

Check Nat.add_assoc.

Corollary associativity_of_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall i j k : nat,
      add i (add j k) = add (add i j) k.
Proof.
  intros add S_add i j k.
  rewrite -> (about_a_recursive_addition add S_add i (add j k)).
  rewrite -> (about_a_recursive_addition add S_add j k).
  rewrite -> (about_a_recursive_addition add S_add i j).
  rewrite -> (about_a_recursive_addition add S_add (i + j) k).
  exact (Nat.add_assoc i j k).

  Restart.

  intros add S_add i j k.
  Check (soundness_of_recursive_addition_with_respect_to_the_resident_addition add S_add i j (add i j) (eq_refl (add i j))).
  rewrite -> (soundness_of_recursive_addition_with_respect_to_the_resident_addition add S_add j k (add j k) (eq_refl (add j k))).
  rewrite -> (soundness_of_recursive_addition_with_respect_to_the_resident_addition add S_add i (j + k) (add i (j + k)) (eq_refl (add i (j + k)))).
  Check (soundness_of_recursive_addition_with_respect_to_the_resident_addition add S_add i j (add i j) (eq_refl (add i j))).
  rewrite -> (soundness_of_recursive_addition_with_respect_to_the_resident_addition add S_add i j (add i j) (eq_refl (add i j))).
  Check (soundness_of_recursive_addition_with_respect_to_the_resident_addition add S_add (i + j) k (add (i + j) k) (eq_refl (add (i + j) k))).
  rewrite -> (soundness_of_recursive_addition_with_respect_to_the_resident_addition add S_add (i + j) k (add (i + j) k) (eq_refl (add (i + j) k))).
  exact (Nat.add_assoc i j k).
Qed.

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

Check Nat.add_comm.

Lemma commutativity_of_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall i j : nat,
      add i j = add j i.
Proof.
Admitted. (* for the sake of the argument below *)

Corollary commutativity_of_Nat_dot_add :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall i j : nat,
      i + j = j + i.
Proof.
  intros add S_add i j.
  Check (about_a_recursive_addition add S_add i j).
  rewrite <- (about_a_recursive_addition add S_add i j).
  rewrite <- (about_a_recursive_addition add S_add j i).
  Check (commutativity_of_recursive_addition add S_add i j).
  exact (commutativity_of_recursive_addition add S_add i j).

  Restart.

  intros add S_add i j.
  Check (completeness_of_recursive_addition add S_add i j (i + j) (eq_refl (i + j))).
  rewrite <- (completeness_of_recursive_addition add S_add i j (i + j) (eq_refl (i + j))).
  rewrite <- (completeness_of_recursive_addition add S_add j i (j + i) (eq_refl (j + i))).
  exact (commutativity_of_recursive_addition add S_add i j).
Qed.  

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

(* Exercise 08 *)

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

(* ***** *)

Lemma about_a_tail_recursive_addition :
  forall add : nat -> nat -> nat,
    tail_recursive_specification_of_addition add ->
    forall i j : nat,
      add i j = i + j.
Proof.
Abort.

(* ***** *)

Proposition soundness_of_tail_recursive_addition_with_respect_to_the_resident_addition :
  forall add : nat -> nat -> nat,
    tail_recursive_specification_of_addition add ->
    forall i j k : nat,
      add i j = k ->
      k = i + j.
Proof.
  (* first, as a corollary of about_a_tail_recursive_addition *)

  Restart.

  (* and second, by induction *)
Abort.

(* ***** *)

Proposition completeness_of_tail_recursive_addition_with_respect_to_the_resident_addition :
  forall add : nat -> nat -> nat,
    tail_recursive_specification_of_addition add ->
    forall i j k : nat,
      i + j = k ->
      k = add i j.
Proof.
  (* first, as a corollary of about_a_tail_recursive_addition *)

  Restart.

  (* and second, by induction *)
Abort.

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

(* end of week-05_more-about-soundness-and-completeness.v *)