(* week-04_equational-reasoning.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 09 Feb 2024 *)

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

(* 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_v1 (i j : nat) : nat :=
  match i with
    O =>
    j
  | S i' =>
    S (add_v1 i' j)
  end.

Lemma fold_unfold_add_v1_O :
  forall j : nat,
    add_v1 O j =
    j.
Proof.
  fold_unfold_tactic add_v1.
Qed.

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

Theorem add_v1_satisfies_the_recursive_specification_of_addition :
  recursive_specification_of_addition add_v1.
Proof.
  unfold recursive_specification_of_addition.
  split.
  
  - exact fold_unfold_add_v1_O.

  - exact fold_unfold_add_v1_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 :=
  (candidate 2 0 =? 1) &&
  (candidate 10 2 =? 10 * 10) &&
  (candidate 3 2 =? 3 * 3).

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

Compute (test_power power_v0).

Lemma fold_unfold_power_v0_O :
  forall x : nat,
    power_v0 x O =
    1.
Proof.
  fold_unfold_tactic power_v0.
Qed.

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

(* ***** *)

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

Lemma fold_unfold_power_v1_aux_O :
  forall x a : nat,
    power_v1_aux x 0 a =
    a.
Proof.
  fold_unfold_tactic power_v1_aux.
Qed.

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

Definition power_v1 (x n : nat) : nat :=
  power_v1_aux x n 1.

Compute (test_power power_v1).

Lemma power_v0_and_power_v1_are_equivalent_aux :
  forall x n a : nat,
    (power_v0 x n) * a = power_v1_aux x n a.
Proof.
  intros x n.
  induction n as [| n' IHx'].
  - intro a.
    rewrite -> (fold_unfold_power_v0_O x).
    rewrite -> (fold_unfold_power_v1_aux_O x a).
    exact (Nat.mul_1_l a).
  - intro a.
    rewrite -> (fold_unfold_power_v0_S x n').
    rewrite -> (fold_unfold_power_v1_aux_S x n' a).
    rewrite <- (IHx' (x * a)).
    rewrite -> (Nat.mul_comm x (power_v0 x n')).
    symmetry.
    exact (Nat.mul_assoc (power_v0 x n') x a).

Qed.

Theorem power_v0_and_power_v1_are_equivalent:
  forall x n : nat,
    power_v0 x n = power_v1 x n.
Proof.
  intros x n.
  unfold power_v1.
  Check (power_v0_and_power_v1_are_equivalent_aux).
  rewrite <- (Nat.mul_1_r (power_v0 x n)).
  exact (power_v0_and_power_v1_are_equivalent_aux x n 1).
Qed.


(* ***** *)

(* Eureka lemma: *)

(* Lemma about_power_v0_and_power_v1_aux : *)
(*   forall x n a : nat, *)
(*     power_v0 x n * a = power_v1_aux x n a. *)
(* (* *)
(*     power_v0 x n is       x * x * ... * x n times *)

(*     power_v1_aux x n a is x * x * ... * x * a *)
(*  *) *)
(* Proof. *)
(*   intros x n. *)
(*   induction n as [ | n' IHn']. *)
(*   - intro a. *)
(*     rewrite -> (fold_unfold_power_v0_O x). *)
(*     rewrite -> (fold_unfold_power_v1_aux_O x a). *)
(*     exact (Nat.mul_1_l a). *)
(*   - intro a. *)
(*     rewrite -> (fold_unfold_power_v0_S x n'). *)
(*     rewrite -> (fold_unfold_power_v1_aux_S x n' a). *)
(*     Check (IHn' (x * a)). *)
(*     rewrite <- (IHn' (x * a)). *)
(*     rewrite -> (Nat.mul_comm x (power_v0 x n')). *)
(*     Check (Nat.mul_assoc). *)
(*     symmetry. *)
(*     exact (Nat.mul_assoc (power_v0 x n') x a). *)
(* Qed.     *)

(* Lemma that proves unnecessary: *)

(* Lemma power_v0_and_power_v1_are_equivalent_aux : *)
(*   forall x n : nat, *)
(*     power_v0 x n = power_v1_aux x n 1. *)
(* Proof. *)
(*   intros x n. *)
(*   induction n as [ | n' IHn']. *)
(*   - rewrite -> (fold_unfold_power_v0_O x). *)
(*     rewrite -> (fold_unfold_power_v1_aux_O x 1). *)
(*     reflexivity. *)
(*   - rewrite -> (fold_unfold_power_v0_S x n'). *)
(*     rewrite -> (fold_unfold_power_v1_aux_S x n' 1). *)
(*     rewrite -> (Nat.mul_1_r x). *)
(*     Check (about_power_v0_and_power_v1_aux x n' x). *)
(*     rewrite <- (about_power_v0_and_power_v1_aux x n' x). *)
(*     Check (Nat.mul_comm x (power_v0 x n')). *)
(*     exact (Nat.mul_comm x (power_v0 x n')). *)
(* Qed. *)
(*
    case n' as [ | n''].
    + rewrite -> (fold_unfold_power_v0_O x).
      rewrite -> (fold_unfold_power_v1_aux_O x x).
      exact (Nat.mul_1_r x).
    + rewrite -> (fold_unfold_power_v0_S x n'').
      rewrite -> (fold_unfold_power_v1_aux_S x n'' x).
*)

(* Theorem power_v0_and_power_v1_are_equivalent : *)
(*   forall x n : nat, *)
(*     power_v0 x n = power_v1 x n. *)
(* Proof. *)
(*   intros x n. *)
(*   unfold power_v1. *)
(*   Check (about_power_v0_and_power_v1_aux x n 1). *)
(*   rewrite <- (Nat.mul_1_r (power_v0 x n)). *)
(*   exact (about_power_v0_and_power_v1_aux x n 1). *)
(* Qed. *)

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

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

Lemma fold_unfold_fib_v1_O :
  fib_v1 O =
  0.
Proof.
  fold_unfold_tactic fib_v1.
Qed.

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

Corollary fold_unfold_fib_v1_1 :
  fib_v1 1 =
  1.
Proof.
  rewrite -> (fold_unfold_fib_v1_S 0).
  reflexivity.
Qed.

Corollary fold_unfold_fib_v1_SS :
  forall n'' : nat,
    fib_v1 (S (S n'')) =
    fib_v1 (S n'') + fib_v1 n''.
Proof.
  intro n''.
  rewrite -> (fold_unfold_fib_v1_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 18 *)

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 :=
  (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Leaf nat 1)) true)
  &&
  (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Leaf nat 2)) false)
  &&
  (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Node nat (Leaf nat 2) (Leaf nat 3))) false)
  &&
  (Bool.eqb (candidate nat Nat.eqb (Node nat (Leaf nat 1) (Leaf nat 2)) (Leaf nat 1)) false)

.

Fixpoint mirrorp (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : binary_tree V) : bool :=
  match t1 with
  | Leaf _ v1 =>
    match t2 with
    | Leaf _ v2 => eqb_V v1 v2
    | Node _ _ _ => false
    end
  | Node _ t11 t12 =>
    match t2 with
    | Leaf _ _ => false
    | Node _ t21 t22 => (mirrorp V eqb_V t11 t22) && (mirrorp V eqb_V t12 t21)
    end
  end.

Compute (test_mirrop mirrorp).

(* Taken from github.com/valiant-tCPA-learners/cs3234_week_04 *)
Definition improved_test_mirrop (candidate : forall V : Type,
      (V -> V -> bool) -> binary_tree V -> binary_tree V -> bool) : bool :=
  (* Mirror over leaf nodes *)
  (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Leaf nat 1)) true)
  &&
    (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Leaf nat 2)) false)
  &&
  (* Ensure that trees with non-equivalent structures are not considered mirrors*)
  (Bool.eqb
     (candidate nat Nat.eqb
        (Leaf nat 1)
        (Node nat (Leaf nat 2) (Leaf nat 3)))
     false)
  &&
  (Bool.eqb
     (candidate nat Nat.eqb
        (Node nat (Leaf nat 1) (Leaf nat 2))
        (Leaf nat 1))
     false)
  &&
  (* Mirror over balanced trees of height 1 *)
  (Bool.eqb
     (candidate nat Nat.eqb
        (Node nat (Leaf nat 1) (Leaf nat 2))
        (Node nat (Leaf nat 2) (Leaf nat 1)))
     true)
  &&
  (Bool.eqb
     (candidate nat Nat.eqb
        (Node nat (Leaf nat 1) (Leaf nat 2))
        (Node nat (Leaf nat 1) (Leaf nat 2)))
     false)
  &&
  (* Mirror over balanced trees of height 2 *)
  (Bool.eqb
     (candidate nat Nat.eqb
        (Node nat
           (Node nat (Leaf nat 1) (Leaf nat 2))
           (Node nat (Leaf nat 3) (Leaf nat 4)))
        (Node nat
           (Node nat (Leaf nat 4) (Leaf nat 3))
           (Node nat (Leaf nat 2) (Leaf nat 1))))
     true)
  &&
  (Bool.eqb
     (candidate nat Nat.eqb
        (Node nat
           (Node nat (Leaf nat 1) (Leaf nat 2))
           (Node nat (Leaf nat 3) (Leaf nat 4)))
        (Node nat
           (Node nat (Leaf nat 3) (Leaf nat 4))
           (Node nat (Leaf nat 1) (Leaf nat 2))))
     false).

Compute (improved_test_mirrop mirrorp).


Lemma fold_unfold_mirrorp_Leaf :
  forall (V : Type) (eqb_V: V -> V -> bool) (v1: V) (t2 : binary_tree V),
    mirrorp V eqb_V (Leaf V v1) t2 =
    match t2 with
    | Leaf _ v2 => eqb_V v1 v2
    | Node _ _ _ => false
    end.
Proof.
  fold_unfold_tactic mirrorp.
Qed.

Lemma fold_unfold_mirrorp_Node :
  forall (V : Type) (eqb_V: V -> V -> bool) (t11 t12 t2 : binary_tree V),
    mirrorp V eqb_V (Node V t11 t12) t2 =
    match t2 with
    | Leaf _ _ => false
    | Node _ t21 t22 => (mirrorp V eqb_V t11 t22) && (mirrorp V eqb_V t12 t21)
    end.
Proof.
  fold_unfold_tactic mirrorp.
Qed.



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) ->
    forall t1 t2 : binary_tree V,
      mirror V t1 = t2 -> mirrorp V eqb_V t1 t2 = true.
  Proof.
    intros V eqb_V H_eqb_V t1.
    induction t1 as [v1 | t11 IHt11 t12 IHt12].
    - intros t2 H_mirror.
      rewrite -> (fold_unfold_mirrorp_Leaf V eqb_V v1 t2).
      unfold mirror in H_mirror.
      case t2 as [v2 | t21 t22].
      + injection H_mirror as H_v1_eq_v2.
        apply (H_eqb_V v1 v2).
        exact H_v1_eq_v2.
      + discriminate H_mirror.
    - intros t2 H_mirror.
      rewrite -> (fold_unfold_mirrorp_Node V eqb_V t11 t12 t2).
      case t2 as [v2 | t21 t22].
      + rewrite -> (fold_unfold_mirror_Node V t11 t12) in H_mirror.
        discriminate H_mirror.
      + rewrite -> (fold_unfold_mirror_Node V t11 t12) in H_mirror.
        injection H_mirror as H_mirror_12 H_mirror_11.
        Search (_ && _ = true).
        rewrite -> (andb_true_iff (mirrorp V eqb_V t11 t22) (mirrorp V eqb_V t12 t21)).
        split.
        * apply (IHt11 t22).
          exact H_mirror_11.
        * apply (IHt12 t21).
          exact H_mirror_12.

          (* * rewrite -> (IHt11 t22). *)
          (*   ** reflexivity. *)
          (* * rewrite -> (IHt12 t21). *)
          (*   ** reflexivity. *)
          (*   ** exact H_mirror_12.  *)
  Qed.



(*
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-04_equational-reasoning.v *)
