(* week-05_equational-reasoning-about-accumulator-based-recursive-functions.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 16 Feb 2025, with uniformly formatted unit-test functions *)
(* was: *)
(* Version of 14 Feb 2025, with renamings *)
(* was: *)
(* Version of 13 Feb 2025 *)

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

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

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

(* Paraphernalia: *)

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

Require Import Arith Bool.

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

(* Two implementations of the addition function *)

(* ***** *)

(* Unit tests *)

Definition test_add (candidate: nat -> nat -> nat) : bool :=
  true
    &&
    (candidate 0 0 =? 0)
    &&
    (candidate 0 1 =? 1)
    &&
    (candidate 1 0 =? 1)
    &&
    (candidate 1 1 =? 2)
    &&
    (candidate 1 2 =? 3)
    &&
    (candidate 2 1 =? 3)
    &&
    (candidate 2 2 =? 4)
(* etc. *)
.

(* ***** *)

(* Recursive implementation of the addition function *)

Fixpoint add (i j : nat) : nat :=
  match i with
    O =>
    j
  | S i' =>
    S (add i' j)
  end.

Compute (test_add add).

Lemma fold_unfold_add_O :
  forall j : nat,
    add O j =
    j.
Proof.
  fold_unfold_tactic add.
Qed.

Lemma fold_unfold_add_S :
  forall i' j : nat,
    add (S i') j =
    S (add i' j).
Proof.
  fold_unfold_tactic add.
Qed.

(* ***** *)

(* Tail-recursive implementation of the addition function *)

Fixpoint add' (i j : nat) : nat :=
  match i with
    O => 
    j
  | S i' =>
    add' i' (S j)
  end.

Compute (test_add add').

Lemma fold_unfold_add'_O :
  forall j : nat,
    add' O j =
    j.
Proof.
  fold_unfold_tactic add'.
Qed.

Lemma fold_unfold_add'_S :
  forall i' j : nat,
    add' (S i') j =
    add' i' (S j).
Proof.
  fold_unfold_tactic add'.
Qed.

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

(* Equivalence of add and add' *)

(* ***** *)

(* The master lemma: *)

Lemma about_add' :
  forall i j : nat,
    add' i (S j) = S (add' i j).
Proof.
  intro i.
  induction i as [ | i' IHi'].

  - intro j.
    rewrite -> (fold_unfold_add'_O j).
    exact (fold_unfold_add'_O (S j)).

  - intro j.
    rewrite -> (fold_unfold_add'_S i' (S j)).
    rewrite -> (fold_unfold_add'_S i' j).
    Check (IHi' (S j)).
    exact (IHi' (S j)).
Qed.

(* ***** *)

(* The main theorem: *)

Theorem equivalence_of_add_and_add' :
  forall i j : nat,
    add i j = add' i j.
Proof.
  intro i.
  induction i as [ | i' IHi'].

  - intro j.
    rewrite -> (fold_unfold_add'_O j).
    exact (fold_unfold_add_O j).

  - intro j.
    rewrite -> (fold_unfold_add_S i' j).
    rewrite -> (fold_unfold_add'_S i' j).
    rewrite -> (IHi' j).
    symmetry.
    exact (about_add' i' j).
Qed.

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

(* Neutral (identity) element for addition *)

(* ***** *)

Property O_is_left_neutral_for_add :
  forall y : nat,
    add 0 y = y.
Proof.
Abort.

(* ***** *)

Property O_is_left_neutral_for_add' :
  forall y : nat,
    add' 0 y = y.
Proof.
Abort.

(* ***** *)

Property O_is_right_neutral_for_add :
  forall x : nat,
    add x 0 = x.
Proof.
Abort.

Property O_is_right_neutral_for_add' :
  forall x : nat,
    add' x 0 = x.
Proof.
Abort.

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

(* Associativity of addition *)

(* ***** *)

Property add_is_associative :
  forall x y z : nat,
    add x (add y z) = add (add x y) z.
Proof.
Abort.

(* ***** *)

Property add'_is_associative :
  forall x y z : nat,
    add' x (add' y z) = add' (add' x y) z.
Proof.
Abort.

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

(* Commutativity of addition *)

(* ***** *)

Property add_is_commutative :
  forall x y : nat,
    add x y = add y x.
Proof.
Abort.

(* ***** *)

Property add'_is_commutative :
  forall x y : nat,
    add' x y = add' y x.
Proof.
Abort.

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

(* Four implementations of the multiplication function *)

(* ***** *)

(* Unit tests *)

Definition test_mul (candidate: nat -> nat -> nat) : bool :=
  true
    &&
    (candidate 0 0 =? 0)
    &&
    (candidate 0 1 =? 0)
    &&
    (candidate 1 0 =? 0)
    &&
    (candidate 1 1 =? 1)
    &&
    (candidate 1 2 =? 2)
    &&
    (candidate 2 1 =? 2)
    &&
    (candidate 2 2 =? 4)
    &&
    (candidate 2 3 =? 6)
    &&
    (candidate 3 2 =? 6)
    &&
    (candidate 6 4 =? 24)
    &&
    (candidate 4 6 =? 24)
(* etc. *)
.

(* ***** *)

(* Recursive implementation of the multiplication function, using add *)

Fixpoint mul (x y : nat) : nat :=
  match x with
    O =>
    O
  | S x' =>
    add (mul x' y) y
  end.

Compute (test_mul mul).

Lemma fold_unfold_mul_O :
  forall y : nat,
    mul O y =
    O.
Proof.
  fold_unfold_tactic mul.
Qed.

Lemma fold_unfold_mul_S :
  forall x' y : nat,
    mul (S x') y =
    add (mul x' y) y.
Proof.
  fold_unfold_tactic mul.
Qed.

(* ***** *)

(* Recursive implementation of the multiplication function, using add' *)

Fixpoint mul' (x y : nat) : nat :=
  match x with
    O =>
    O
  | S x' =>
    add' (mul' x' y) y
  end.

Compute (test_mul mul').

Lemma fold_unfold_mul'_O :
  forall y : nat,
    mul' O y =
    O.
Proof.
  fold_unfold_tactic mul'.
Qed.

Lemma fold_unfold_mul'_S :
  forall x' y : nat,
    mul' (S x') y =
    add' (mul' x' y) y.
Proof.
  fold_unfold_tactic mul'.
Qed.

(* ***** *)

(* Tail-recursive implementation of the multiplication function, using add *)

Fixpoint mul_acc (x y a : nat) : nat :=
  match x with
    O =>
    a
  | S x' =>
    mul_acc x' y (add a y)
  end.

Definition mul_alt (x y : nat) : nat :=
  mul_acc x y 0.

Compute (test_mul mul_alt).

(* ***** *)

(* Tail-recursive implementation of the multiplication function, using add' *)

Fixpoint mul'_acc (x y a : nat) : nat :=
  match x with
    O =>
    a
  | S x' =>
    mul'_acc x' y (add' a y)
  end.

Definition mul'_alt (x y : nat) : nat :=
  mul'_acc x y 0.

Compute (test_mul mul'_alt).

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

(* Equivalence of mul, mul', mul_alt, and mul'_alt *)

(* The interesting point here is to devise the Eureka lemma
   associated to each of the theorems below. *)

(* ***** *)

Theorem equivalence_of_mul_and_mul' :
  forall i j : nat,
    mul i j = mul' i j.
Proof.
Abort.

(* ***** *)

Theorem equivalence_of_mul_and_mul_alt :
  forall i j : nat,
    mul i j = mul_alt i j.
Proof.
Abort.

(* ***** *)

Theorem equivalence_of_mul_and_mul'_alt :
  forall i j : nat,
    mul i j = mul'_alt i j.
Proof.
Abort.

(* ***** *)

Theorem equivalence_of_mul'_and_mul_alt :
  forall i j : nat,
    mul' i j = mul_alt i j.
Proof.
Abort.

(* ***** *)

Theorem equivalence_of_mul'_and_mul'_alt :
  forall i j : nat,
    mul' i j = mul'_alt i j.
Proof.
Abort.

(* ***** *)

Theorem equivalence_of_mul_alt_and_mul'_alt :
  forall i j : nat,
    mul_alt i j = mul'_alt i j.
Proof.
Abort.

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

(* 0 is left absorbing for multiplication *)

(* ***** *)

Property O_is_left_absorbing_for_mul :
  forall y : nat,
    mul 0 y = 0.
Proof.
Abort.

(* ***** *)

Property O_is_left_absorbing_for_mul' :
  forall y : nat,
    mul' 0 y = 0.
Proof.
Abort.

(* ***** *)

Property O_is_left_absorbing_for_mul_alt :
  forall y : nat,
    mul_alt 0 y = 0.
Proof.
Abort.

(* ***** *)

Property O_is_left_absorbing_for_mul'_alt :
  forall y : nat,
    mul'_alt 0 y = 0.
Proof.
Abort.

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

(* 1 is left neutral for multiplication *)

(* ***** *)

Property SO_is_left_neutral_for_mul :
  forall y : nat,
    mul 1 y = y.
Proof.
Abort.

(* ***** *)

Property SO_is_left_neutral_for_mul' :
  forall y : nat,
    mul' 1 y = y.
Proof.
Abort.

(* ***** *)

Property SO_is_left_neutral_for_mul_alt :
  forall y : nat,
    mul_alt 1 y = y.
Proof.
Abort.

(* ***** *)

Property SO_is_left_neutral_for_mul'_alt :
  forall y : nat,
    mul'_alt 1 y = y.
Proof.
Abort.

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

(* 0 is right absorbing for multiplication *)

(* ***** *)

Property O_is_right_absorbing_for_mul :
  forall x : nat,
    mul x 0 = 0.
Proof.
Abort.

(* ***** *)

Property O_is_right_absorbing_for_mul' :
  forall x : nat,
    mul' x 0 = 0.
Proof.
Abort.

(* ***** *)

Property O_is_right_absorbing_for_mul_alt :
  forall x : nat,
    mul_alt x 0 = 0.
Proof.
Abort.

(* ***** *)

Property O_is_right_absorbing_for_mul'_alt :
  forall x : nat,
    mul'_alt x 0 = 0.
Proof.
Abort.

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

(* 1 is right neutral for multiplication *)

(* ***** *)

Property SO_is_right_neutral_for_mul :
  forall x : nat,
    mul x 1 = x.
Proof.
Abort.

(* ***** *)

Property SO_is_right_neutral_for_mul' :
  forall x : nat,
    mul' x 1 = x.
Proof.
Abort.

(* ***** *)

Property SO_is_right_neutral_for_mul_alt :
  forall x : nat,
    mul_alt x 1 = x.
Proof.
Abort.

(* ***** *)

Property SO_is_right_neutral_for_mul'_alt :
  forall x : nat,
    mul'_alt x 1 = x.
Proof.
Abort.

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

(* Multiplication is right-distributive over addition *)

(* ***** *)

(* ... *)

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

(* Multiplication is associative *)

(* ***** *)

Property mul_is_associative :
  forall x y z : nat,
    mul x (mul y z) = mul (mul x y) z.
Proof.
Abort.

(* ***** *)

Property mul'_is_associative :
  forall x y z : nat,
    mul' x (mul' y z) = mul' (mul' x y) z.
Proof.
Abort.

(* ***** *)

Property mul_alt_is_associative :
  forall x y z : nat,
    mul_alt x (mul_alt y z) = mul_alt (mul_alt x y) z.
Proof.
Abort.

(* ***** *)

Property mul'_alt_is_associative :
  forall x y z : nat,
    mul'_alt x (mul'_alt y z) = mul'_alt (mul'_alt x y) z.
Proof.
Abort.

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

(* Multiplication is left-distributive over addition *)

(* ***** *)

(* ... *)

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

(* end of week-05_equational-reasoning-about-accumulator-based-recursive-functions.v *)