(* week-05_equational-reasoning-about-recursive-functions-using-fold-unfold-lemmas.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 05 Jun 2025, with more exercises about the power function *)
(* was: *)
(* Version of 16 Feb 2025, with uniformly formatted unit-test functions *)
(* was: *)
(* Version of 13 Feb 2025 *)

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

(* Paraphernalia: *)

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

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

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

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.

Theorem add_satisfies_the_recursive_specification_of_addition :
  recursive_specification_of_addition add.
Proof.
  unfold recursive_specification_of_addition.
  split.
  
  - exact fold_unfold_add_O.

  - exact fold_unfold_add_S.
Qed.

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

Definition specification_of_power (power : nat -> nat -> nat) :=
  (forall x : nat,
      power x 0 = 1)
  /\
  (forall (x : nat)
          (n' : nat),
      power x (S n') = x * power x n').

Definition test_power (candidate : nat -> nat -> nat) : bool :=
  true
    &&
    (candidate 2 0 =? 1)
    &&
    (candidate 10 2 =? 10 * 10)
    &&
    (candidate 3 2 =? 3 * 3).

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

Compute (test_power power).

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.

(* ***** *)

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

Lemma fold_unfold_power_acc_O :
  forall x a : nat,
    power_acc x 0 a =
    a.
Proof.
  fold_unfold_tactic power_acc.
Qed.

Lemma fold_unfold_power_acc_S :
  forall x n' a : nat,
    power_acc x (S n') a =
    power_acc x n' (x * a).
Proof.
  fold_unfold_tactic power_acc.
Qed.

Definition power_alt (x n : nat) : nat :=
  power_acc x n 1.

Compute (test_power power_alt).

(* ***** *)

(* Eureka lemma: *)

Lemma about_power_and_power_acc :
  forall x n a : nat,
    power x n * a = power_acc x n a.
(*
    power x n is       x * x * ... * x n times

    power_acc x n a is x * x * ... * x * a
 *)
Proof.
  intros x n.
  induction n as [ | n' IHn'].
  - intro a.
    rewrite -> (fold_unfold_power_O x).
    rewrite -> (fold_unfold_power_acc_O x a).
    exact (Nat.mul_1_l a).
  - intro a.
    rewrite -> (fold_unfold_power_S x n').
    rewrite -> (fold_unfold_power_acc_S x n' a).
    Check (IHn' (x * a)).
    rewrite <- (IHn' (x * a)).
    rewrite -> (Nat.mul_comm x (power x n')).
    Check (Nat.mul_assoc).
    symmetry.
    exact (Nat.mul_assoc (power x n') x a).
Qed.    

(* Lemma that proves unnecessary: *)

Lemma power_and_power_alt_are_equivalent_aux :
  forall x n : nat,
    power x n = power_acc x n 1.
Proof.
  intros x n.
  induction n as [ | n' IHn'].
  - rewrite -> (fold_unfold_power_O x).
    rewrite -> (fold_unfold_power_acc_O x 1).
    reflexivity.
  - rewrite -> (fold_unfold_power_S x n').
    rewrite -> (fold_unfold_power_acc_S x n' 1).
    rewrite -> (Nat.mul_1_r x).
    Check (about_power_and_power_acc x n' x).
    rewrite <- (about_power_and_power_acc x n' x).
    Check (Nat.mul_comm x (power x n')).
    exact (Nat.mul_comm x (power x n')).
Qed.
(*
    case n' as [ | n''].
    + rewrite -> (fold_unfold_power_O x).
      rewrite -> (fold_unfold_power_acc_O x x).
      exact (Nat.mul_1_r x).
    + rewrite -> (fold_unfold_power_S x n'').
      rewrite -> (fold_unfold_power_acc_S x n'' x).
*)

Theorem power_and_power_alt_are_equivalent :
  forall x n : nat,
    power x n = power_alt x n.
Proof.
  intros x n.
  unfold power_alt.
  Check (about_power_and_power_acc x n 1).
  rewrite <- (Nat.mul_1_r (power x n)).
  exact (about_power_and_power_acc x n 1).
Qed.

(* ***** *)

Theorem about_exponentiating_one :
  forall n : nat,
    power 1 n = 1.
Proof.
  intro n.
  induction n as [ | n' IHn'].
  - rewrite -> (fold_unfold_power_O 1).
    reflexivity.
  - rewrite -> (fold_unfold_power_S 1 n').
    rewrite -> (Nat.mul_1_l (power 1 n')).
    exact IHn'.
Qed.

(* ***** *)

Theorem about_exponentiating_a_product :
  forall x y n : nat,
    power (x * y) n = power x n * power y n.
Proof.
  Compute (let f x y n := power (x * y) n = power x n * power y n in
           (f 2 3 2, f 4 2 3)).
  intros x y n.
  induction n as [ | n' IHn'].
  - rewrite -> (fold_unfold_power_O (x * y)).
    rewrite -> (fold_unfold_power_O x).
    rewrite -> (fold_unfold_power_O y).
    compute.
    reflexivity.
  - rewrite -> (fold_unfold_power_S (x * y) n').
    rewrite -> (fold_unfold_power_S x n').
    rewrite -> (fold_unfold_power_S y n').
    rewrite -> IHn'.
    Search (_ * _ * (_ * _)).
(* Nat.mul_shuffle1: forall n m p q : nat, n * m * (p * q) = n * p * (m * q) *)
    Check (Nat.mul_shuffle1 x y (power x n') (power y n')).
    exact (Nat.mul_shuffle1 x y (power x n') (power y n')).
Qed.

(* ***** *)

Theorem about_exponentiating_with_a_sum :
  forall x i j : nat,
    power x (i + j) = power x i * power x j.
Proof.
  Compute (let f x i j := power x (i + j) = power x i * power x j in
           (f 2 3 2, f 4 2 3)).
  intros x i.
  induction i as [ | i' IHi'].
  - intro j.
    rewrite -> (Nat.add_0_l j).
    rewrite -> (fold_unfold_power_O x).
    rewrite -> (Nat.mul_1_l (power x j)).
    reflexivity.
  - intro j.
    rewrite -> (plus_Sn_m i' j).
    rewrite -> (fold_unfold_power_S x (i' + j)).
    rewrite -> (fold_unfold_power_S x i').
    rewrite -> (IHi' j).
    Check Nat.mul_assoc.
    exact (Nat.mul_assoc x (power x i') (power x j)).
Qed.

(* ***** *)

Theorem about_exponentiating_with_a_product :
  forall x y z : nat,
    power x (y * z) = power (power x y) z.
Proof.
Abort.

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

Fixpoint fib (n : nat) : nat :=
  match n with
    0 =>
    0
  | S n' =>
    match n' with
      0 =>
      1
    | S n'' =>
      fib n' + fib n''
    end
  end.

Lemma fold_unfold_fib_O :
  fib O =
  0.
Proof.
  fold_unfold_tactic fib.
Qed.

Lemma fold_unfold_fib_S :
  forall n' : nat,
    fib (S n') =
    match n' with
      0 =>
      1
    | S n'' =>
      fib n' + fib n''
    end.
Proof.
  fold_unfold_tactic fib.
Qed.

Corollary fold_unfold_fib_1 :
  fib 1 =
  1.
Proof.
  rewrite -> (fold_unfold_fib_S 0).
  reflexivity.
Qed.

Corollary fold_unfold_fib_SS :
  forall n'' : nat,
    fib (S (S n'')) =
    fib (S n'') + fib n''.
Proof.
  intro n''.
  rewrite -> (fold_unfold_fib_S (S n'')).
  reflexivity.
Qed.

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

Inductive binary_tree (V : Type) : Type :=
| Leaf : V -> binary_tree V
| Node : binary_tree V -> binary_tree V -> binary_tree V.

(* ***** *)

Definition specification_of_mirror (mirror : forall V : Type, binary_tree V -> binary_tree V) : Prop :=
  (forall (V : Type)
          (v : V),
      mirror V (Leaf V v) =
      Leaf V v)
  /\
  (forall (V : Type)
          (t1 t2 : binary_tree V),
      mirror V (Node V t1 t2) =
      Node V (mirror V t2) (mirror V t1)).

(* ***** *)

Fixpoint mirror (V : Type) (t : binary_tree V) : binary_tree V :=
  match t with
    Leaf _ v =>
    Leaf V v
  | Node _ t1 t2 =>
    Node V (mirror V t2) (mirror V t1)
  end.

Lemma fold_unfold_mirror_Leaf :
  forall (V : Type)
         (v : V),
    mirror V (Leaf V v) =
    Leaf V v.
Proof.
  fold_unfold_tactic mirror.
Qed.

Lemma fold_unfold_mirror_Node :
  forall (V : Type)
         (t1 t2 : binary_tree V),
    mirror V (Node V t1 t2) =
    Node V (mirror V t2) (mirror V t1).
Proof.
  fold_unfold_tactic mirror.
Qed.

(* ***** *)

Proposition there_is_at_least_one_mirror_function :
  specification_of_mirror mirror.
Proof.
  unfold specification_of_mirror.
  split.
  - exact fold_unfold_mirror_Leaf.
  - exact fold_unfold_mirror_Node.
Qed.

(* ***** *)

Theorem mirror_is_involutory :
  forall (V : Type)
         (t : binary_tree V),
    mirror V (mirror V t) = t.
Proof.
  intros V t.
  induction t as [v | t1 IHt1 t2 IHt2].
  - rewrite -> (fold_unfold_mirror_Leaf V v).
    exact (fold_unfold_mirror_Leaf V v).
  - rewrite -> (fold_unfold_mirror_Node V t1 t2).
    rewrite -> (fold_unfold_mirror_Node V (mirror V t2) (mirror V t1)).
    rewrite -> IHt1.
    rewrite -> IHt2.
    reflexivity.
Qed.

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

(* Exercise 23 *)

Require Import Bool.

Inductive binary_tree (V : Type) : Type :=
  Leaf : V -> binary_tree V
| Node : binary_tree V -> binary_tree V -> binary_tree V.

Definition test_mirrop (candidate : forall V : Type, (V -> V -> bool) -> binary_tree V -> binary_tree V -> bool) : bool :=
  true
    &&
    (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Leaf nat 1)) true).

(*
Fixpoint mirrorp (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : binary_tree V) : bool :=
  ...
*)

(*
Compute (test_mirrop mirrorp).
*)

(*
Lemma fold_unfold_mirrorp_Leaf :
  ...
*)

(*
Lemma fold_unfold_mirrorp_Node :
  ...
*)

(*
Proposition soundness_of_mirror_wrt_mirrorp :
  forall (V : Type)
         (eqb_V : V -> V -> bool),
    (forall v v' : V,
        v = v' ->
        eqb_V v v' = true) ->
    ...
*)

(*
Proposition completeness_of_mirror :
  forall (V : Type)
         (eqb_V : V -> V -> bool),
    (forall v v' : V,
        eqb_V v v' = true ->
        v = v') ->
    ...
*)

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

(* end of week-05_equational-reasoning-about-recursive-functions-using-fold-unfold-lemmas.v *)