(* question-for-Yadunand.v *)
(* CS3234 oral exam *)
(* Sun 05 May 2024 *)

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

(* Your oral exam is about primitive recursion for Peano numbers. *)

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

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

Require Import Arith Bool List.

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

(* Reminder:
   Any function that is expressible as an instance of nat_fold_right is said to be "primitive iterative". *)

Fixpoint nat_fold_right (V : Type) (zero_case : V) (succ_case : V -> V) (n : nat) : V :=
  match n with
    O =>
    zero_case
  | S n' =>
    succ_case (nat_fold_right V zero_case succ_case n')
  end.

(* Definition:
   Any function that is expressible as an instance of nat_parafold_right is said to be "primitive recursive". *)

Fixpoint nat_parafold_right (V : Type) (zero_case : V) (succ_case : nat -> V -> V) (n : nat) : V := match n with
    O =>
    zero_case
  | S n' =>
    succ_case n' (nat_parafold_right V zero_case succ_case n')
  end.

Lemma fold_unfold_nat_parafold_right_O :
  forall (V : Type)
         (zero_case : V)
         (succ_case : nat -> V -> V),
    nat_parafold_right V zero_case succ_case 0 =
    zero_case.
Proof.
  fold_unfold_tactic nat_parafold_right.
Qed.

Lemma fold_unfold_nat_parafold_right_S :
  forall (V : Type)
         (zero_case : V)
         (succ_case : nat -> V -> V)
         (n' : nat),
    nat_parafold_right V zero_case succ_case (S n') =
    succ_case n' (nat_parafold_right V zero_case succ_case n').
Proof.
  fold_unfold_tactic nat_parafold_right.
Qed.

(* ***** *)

Fixpoint nat_parafold_left (V : Type) (zero_case : V) (succ_case : nat -> V -> V) (n : nat) : V :=
  match n with
    O =>
    zero_case
  | S n' =>
    nat_parafold_left V (succ_case n' zero_case) succ_case n'    
  end.

Lemma fold_unfold_nat_parafold_left_O :
  forall (V : Type)
         (zero_case : V)
         (succ_case : nat -> V -> V),
    nat_parafold_left V zero_case succ_case 0 =
    zero_case.
Proof.
  fold_unfold_tactic nat_parafold_left.
Qed.

Lemma fold_unfold_nat_parafold_left_S :
  forall (V : Type)
         (zero_case : V)
         (succ_case : nat -> V -> V)
         (n' : nat),
    nat_parafold_left V zero_case succ_case (S n') =
    nat_parafold_left V (succ_case n' zero_case) succ_case n'.
Proof.
  fold_unfold_tactic nat_parafold_left.
Qed.

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

Definition test_fac (candidate: nat -> nat) : bool :=
  (Nat.eqb (candidate 0) 1)
  &&
  (Nat.eqb (candidate 5) 120).

(* ***** *)

(* Recursive implementation of the factorial function: *)

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

Compute (test_fac r_fac).

(* 1.a Implement r_fac as an instance of nat_parafold_right: *)

Definition r_fac_right (n : nat) : nat :=
  nat_parafold_right nat 1 (fun n' ih => (S n') * ih) n.

(* 1.b Test your implementation. *)
Compute (test_fac r_fac).

(* 1.c Prove that r_fac and r_fac_right are equivalent. *)

Lemma fold_unfold_r_fac_O :
  r_fac 0 = 1.
Proof.
  fold_unfold_tactic r_fac.
Qed.
Lemma fold_unfold_r_fac_S :
  forall (n' : nat),
    r_fac (S n') = S n' * r_fac n'.
Proof.
  fold_unfold_tactic r_fac.
Qed.

Lemma about_r_fac_and_r_fac_right :
  forall (n : nat),
    r_fac n = nat_parafold_right nat 1 (fun n' ih : nat => S n' * ih) n.
Proof.
  intro n.
  induction n as [ | n' IHn' ].
  - rewrite -> fold_unfold_r_fac_O.
    rewrite -> fold_unfold_nat_parafold_right_O.
    reflexivity.
  - rewrite -> fold_unfold_r_fac_S.
    rewrite -> fold_unfold_nat_parafold_right_S.
    rewrite <- IHn'.
    reflexivity.
Qed.

Theorem r_fac_and_r_fac_right_are_equivalent :
  forall (n : nat),
    r_fac n = r_fac_right n.
Proof.
  intro n.
  unfold r_fac_right.
  exact (about_r_fac_and_r_fac_right n).
Qed.

(* ***** *)

(* Tail-recursive implementation of the factorial function: *)

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

Lemma fold_unfold_tr_fac_acc_O :
  forall (a : nat),
  tr_fac_acc 0 a = a.
Proof.
  fold_unfold_tactic r_fac.
Qed.

Lemma fold_unfold_tr_fac_acc_S :
  forall (n' a : nat),
    tr_fac_acc (S n') a = tr_fac_acc n' (S n' * a).
Proof.
  fold_unfold_tactic r_fac.
Qed.

Definition tr_fac (n : nat) : nat :=
  tr_fac_acc n 1.

Compute (test_fac tr_fac).

(* 2.a Implement tr_fac as an instance of nat_parafold_left: *)

Definition tr_fac_left (n : nat) : nat :=
  nat_parafold_left nat 1 (fun n' a => S n' * a) n.

(* 2.b Test your implementation. *)

Compute (test_fac tr_fac_left).

(* 2.c Prove that tr_fac and tr_fac_left are equivalent. *)
(* Lemma about_tr_fac_acc : *)
(*   forall (n a : nat), *)
(*     tr_fac_acc n a = (tr_fac_acc n 1) * a. *)
(* Proof. *)
(*   intros n. *)
(*   induction n as [ | n' IHn' ]. *)
(*   - intro a. *)
(*     rewrite -> fold_unfold_tr_fac_acc_O. *)
(*     rewrite -> fold_unfold_tr_fac_acc_O. *)
(*     rewrite -> Nat.mul_1_l. *)
(*     reflexivity. *)
(*   - intro a. *)
(*     rewrite -> fold_unfold_tr_fac_acc_S. *)
(*     rewrite -> (IHn' (S (S n') * a)). *)
(*     rewrite ->  *)


Lemma about_tr_fac_and_tr_fac_left :
  forall (n : nat),
    tr_fac_acc n 1 = nat_parafold_left nat 1 (fun n' a : nat => S n' * a) n.
  Proof.
    intro n.
    induction n as [ | n' IHn' ].
    - rewrite -> fold_unfold_tr_fac_acc_O.
      rewrite -> fold_unfold_nat_parafold_left_O.
      reflexivity.
    - rewrite -> fold_unfold_tr_fac_acc_S.
      rewrite -> fold_unfold_nat_parafold_left_S.
      rewrite -> Nat.mul_1_r.
    Abort.

Lemma about_tr_fac_and_tr_fac_left :
  forall (n a: nat),
    tr_fac_acc n a = nat_parafold_left nat a (fun n' a : nat => S n' * a) n.
Proof.
  intro n.
  induction n as [ | n' IHn' ].
  - intro a.
    rewrite -> fold_unfold_tr_fac_acc_O.
    rewrite -> fold_unfold_nat_parafold_left_O.
    reflexivity.
  - intro a.
    rewrite -> fold_unfold_tr_fac_acc_S.
    rewrite -> fold_unfold_nat_parafold_left_S.
    exact (IHn' (S n' * a)).
Qed.

Theorem tr_fac_and_tr_fac_left_are_equivalent :
  forall (n : nat),
    tr_fac n = tr_fac_left n.
Proof.
  intro n.
  unfold tr_fac.
  unfold tr_fac_left.
  exact (about_tr_fac_and_tr_fac_left n 1).
Qed.


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

Definition test_Sigma (candidate: nat -> (nat -> nat) -> nat) : bool :=
  (Nat.eqb (candidate 0 (fun n => S (2 * n))) 1)
  &&
  (Nat.eqb (candidate 1 (fun n => S (2 * n))) 4)
  &&
  (Nat.eqb (candidate 2 (fun n => S (2 * n))) 9)
  &&
  (Nat.eqb (candidate 3 (fun n => S (2 * n))) 16).

(* ***** *)

(* Recursive implementation of the summation function: *)

Fixpoint r_Sigma (n : nat) (f : nat -> nat) : nat :=
  match n with
    O =>
    f 0
  | S n' =>
    (r_Sigma n' f) + f (S n')
  end.

Compute (test_Sigma r_Sigma).

(* 3.a Implement r_Sigma as an instance of nat_parafold_right: *)

Definition r_Sigma_right (n : nat) (f : nat -> nat) : nat :=
  nat_parafold_right
    nat
    (f 0)
    (fun n' ih => (ih + f (S n')))
    n.

(* 3.b Test your implementation. *)

Compute (test_Sigma r_Sigma_right).

(* 3.c Prove that r_Sigma and r_Sigma_right are equivalent. *)

Lemma fold_unfold_r_Sigma_O :
  forall (f : nat -> nat),
    r_Sigma O f = f 0.
Proof.
  fold_unfold_tactic r_Sigma.
Qed.
Lemma fold_unfold_r_Sigma_S :
  forall (n' : nat)
    (f : nat -> nat),
    r_Sigma (S n') f = (r_Sigma n' f) + f (S n').
Proof.
  fold_unfold_tactic r_Sigma.
Qed.

Lemma about_r_Sigma_and_r_Sigma_right :
  forall (n : nat)
    (f : nat -> nat),
    r_Sigma n f = nat_parafold_right nat (f 0) (fun n' ih : nat => ih + f (S n')) n.
Proof.
  intros n f.
  induction n as [ | n' IHn' ].
  - rewrite -> fold_unfold_r_Sigma_O.
    rewrite -> fold_unfold_nat_parafold_right_O.
    reflexivity.
  - rewrite -> fold_unfold_r_Sigma_S.
    rewrite -> fold_unfold_nat_parafold_right_S.
    rewrite <- IHn'.
    reflexivity.
Qed.

Theorem r_Sigma_and_r_Sigma_right_are_equivalent :
  forall (n : nat)
    (f : nat -> nat),
    r_Sigma n f = r_Sigma_right n f.
Proof.
  intros n f.
  unfold r_Sigma_right.
  exact (about_r_Sigma_and_r_Sigma_right n f).
Qed.

(* ***** *)

(* Tail-recursive implementation of the summation function: *)

Fixpoint tr_Sigma_acc (n : nat) (f : nat -> nat) (a : nat) : nat :=
  match n with
    O =>
    a
  | S n' =>
    tr_Sigma_acc n' f (a + f (S n'))
  end.

Lemma fold_unfold_tr_Sigma_acc_O :
  forall (f : nat -> nat)
    (a : nat),
    tr_Sigma_acc 0 f a = a.
Proof.
  fold_unfold_tactic tr_Sigma_acc.
Qed.
Lemma fold_unfold_tr_Sigma_acc_S :
  forall (n' : nat)
    (f : nat -> nat)
    (a : nat),
    tr_Sigma_acc (S n') f a = tr_Sigma_acc n' f (a + f (S n')).
Proof.
  fold_unfold_tactic tr_Sigma_acc.
Qed.

Definition tr_Sigma (n : nat) (f : nat -> nat) : nat :=
  tr_Sigma_acc n f (f 0).

Compute (test_Sigma tr_Sigma).

(* 4.a Implement tr_Sigma as an instance of nat_parafold_left: *)

Definition tr_Sigma_left (n : nat) (f : nat -> nat) : nat :=
  nat_parafold_left nat (f 0) (fun n' a => a + f (S n')) n.


(* 4.b Test your implementation. *)

Compute (test_Sigma tr_Sigma_left).

(* 4.c Prove that tr_Sigma and tr_Sigma_left are equivalent. *)

Lemma about_tr_Sigma_and_tr_Sigma_left :
  forall (n : nat)
    (f : nat -> nat),
    tr_Sigma_acc n f (f 0) = nat_parafold_left nat (f 0) (fun n' a : nat => a + f (S n')) n.
Proof.
Abort.

Lemma about_tr_Sigma_and_tr_Sigma_left :
  forall (n: nat)
    (f : nat -> nat)
    (a : nat),
    tr_Sigma_acc n f a = nat_parafold_left nat a (fun n' a : nat => a + f (S n')) n.
Proof.
  intros n f.
  induction n as [ | n' IHn' ].
  - intros a.
    rewrite -> (fold_unfold_tr_Sigma_acc_O f a).
    rewrite -> fold_unfold_nat_parafold_left_O.
    reflexivity.
  - intros a.
    rewrite -> (fold_unfold_tr_Sigma_acc_S n' f a).
    rewrite -> fold_unfold_nat_parafold_left_S.
    exact (IHn' (a + f (S n'))).
Qed.

Theorem tr_Sigma_and_tr_Sigma_left_are_equivalent :
  forall (n : nat)
    (f : nat -> nat),
    tr_Sigma n f = tr_Sigma_left n f.
Proof.
  intros n f.
  unfold tr_Sigma,tr_Sigma_left.
  exact (about_tr_Sigma_and_tr_Sigma_left n f (f 0)).
Qed.
(* ********** *)

(* 5. Taking inspiration from the theorem about folding left and right over lists in the midterm project,
      state and admit a similar theorem about parafolding left and right over Peano numbers. *)

(* Theorem folding_left_and_right_over_lists : *)
(*   forall (V W : Type) *)
(*          (cons_case : V -> W -> W), *)
(*     is_left_permutative V W cons_case -> *)
(*     forall (nil_case : W) *)
(*            (vs : list V), *)
(*       list_fold_left  V W nil_case cons_case vs = *)
(*       list_fold_right V W nil_case cons_case vs. *)
(* Proof. *)
(*   intros V W cons_case. *)
(*   unfold is_left_permutative. *)
(*   intros H_left_permutative nil_case vs. *)
(*   induction vs as [ | v' vs' IHvs']. *)
(*   - rewrite -> (fold_unfold_list_fold_left_nil  V W nil_case cons_case). *)
(*     rewrite -> (fold_unfold_list_fold_right_nil V W nil_case cons_case). *)
(*     reflexivity. *)
(*   - rewrite -> (fold_unfold_list_fold_left_cons  V W nil_case cons_case v' vs'). *)
(*     rewrite -> (fold_unfold_list_fold_right_cons V W nil_case cons_case v' vs'). *)
(*     rewrite <- IHvs'. *)
(*     rewrite -> (about_list_fold_left_with_left_permutative_cons_case *)
(*                  V W cons_case H_left_permutative nil_case v' vs'). *)
(*     reflexivity. *)
(* Qed. *)
(* Definition is_left_permutative (V W : Type) (op2 : V -> W -> W) := *)
(*   forall (v1 v2 : V) *)
(*          (w : W), *)
(*     op2 v1 (op2 v2 w) = op2 v2 (op2 v1 w). *)
(* ********** *)

Definition is_left_permutative (V : Type) (op2 : nat -> V -> V) :=
  forall (n1 n2 : nat)
    (v : V),
    op2 n1 (op2 n2 v) = op2 n2 (op2 n1 v).

Lemma about_parafolding_l_over_peano_numbers :
  forall (V: Type)
    (succ_case : nat -> V -> V),
    is_left_permutative V succ_case ->
    forall (n : nat)
      (zero_case : V),
  nat_parafold_left V (succ_case n zero_case) succ_case n =
  succ_case n (nat_parafold_left V zero_case succ_case n).
Proof.
  intros V succ_case H_is_left_permutative n.
  unfold is_left_permutative in H_is_left_permutative.
  induction n as [| n' IHn'].
  - intro zero_case.
    rewrite -> 2 fold_unfold_nat_parafold_left_O.
    reflexivity.
  - intro zero_case.
    rewrite -> fold_unfold_nat_parafold_left_S.
    rewrite ->H_is_left_permutative.
    Abort. (* The lemma I stated here is a bit wrong. *)

Lemma about_parafolding_left_over_peano_numbers :
  forall (V: Type)
    (succ_case : nat -> V -> V),
    is_left_permutative V succ_case ->
    forall (n m : nat)
      (zero_case : V),
  nat_parafold_left V (succ_case m zero_case) succ_case n =
  succ_case m (nat_parafold_left V zero_case succ_case n).
Proof.
  intros V succ_case H_is_left_permutative n m.
  unfold is_left_permutative in H_is_left_permutative.
  induction n as [| n' IHn'].
  - intros zero_case.
    rewrite -> 2 fold_unfold_nat_parafold_left_O.
    reflexivity.
  - intros zero_case.
    rewrite -> fold_unfold_nat_parafold_left_S.
    rewrite -> H_is_left_permutative.
    rewrite -> (IHn' (succ_case n' zero_case)).
    rewrite -> fold_unfold_nat_parafold_left_S.
    reflexivity.
Qed.

Lemma about_parafolding_right_over_peano_numbers :
  forall (V : Type)
    (succ_case : nat -> V -> V),
    is_left_permutative V succ_case ->
    forall (n m : nat)
      (zero_case : V),
      nat_parafold_right V (succ_case m zero_case) succ_case n =
        succ_case m (nat_parafold_right V zero_case succ_case n).
Proof.
  intros V succ_case H_left_permutative n m zero_case.
  unfold is_left_permutative in H_left_permutative.
  induction n as [ | n' IHn' ].
  - rewrite -> 2 fold_unfold_nat_parafold_right_O.
    reflexivity.
  - rewrite -> 2 fold_unfold_nat_parafold_right_S.
    rewrite -> H_left_permutative.
    rewrite -> IHn'.
    reflexivity.
Qed.
Theorem parafolding_left_and_right_over_peano_numbers :
  forall (V : Type)
    (succ_case : nat -> V -> V),
    is_left_permutative V succ_case ->
    forall (n : nat)
      (zero_case : V),
      nat_parafold_left V zero_case succ_case n = nat_parafold_right V zero_case succ_case n.
Proof.
  intros V succ_case H_left_permutative n zero_case.
  (* Generalizing the accumulator(?) *)
  induction n as [ | n' IHn' ].
  - rewrite -> fold_unfold_nat_parafold_left_O.
    rewrite -> fold_unfold_nat_parafold_right_O.
    reflexivity.
  - rewrite -> fold_unfold_nat_parafold_left_S.
    rewrite -> fold_unfold_nat_parafold_right_S.
    rewrite <- IHn'.
    Check (about_parafolding_left_over_peano_numbers V succ_case H_left_permutative n' n' zero_case).
    exact (about_parafolding_left_over_peano_numbers V succ_case H_left_permutative n' n' zero_case).
    Restart.
    intros V succ_case H_left_permutative n.
    (* Generalizing the accumulator(?) *)
    induction n as [ | n' IHn' ].
  - intro zero_case.
    rewrite -> fold_unfold_nat_parafold_left_O.
    rewrite -> fold_unfold_nat_parafold_right_O.
    reflexivity.
  - intro zero_case.
    rewrite -> fold_unfold_nat_parafold_right_S.
    rewrite -> fold_unfold_nat_parafold_left_S.
    rewrite -> (IHn' (succ_case n' zero_case)).
    exact (about_parafolding_right_over_peano_numbers
             V
             succ_case
             H_left_permutative
             n'
             n'
             zero_case
          ).
Qed.

(* 6. As a corollary of your similar theorem,
      prove that tr_fac_left and r_fac_right are equivalent
      and that tr_Sigma_left and r_Sigma_right are equivalent. *)

Lemma succ_case_of_fac_is_left_permutative :
  is_left_permutative nat (fun n' a : nat => S n' * a).
Proof.
  unfold is_left_permutative.
  intros n1 n2 v.
  rewrite -> Nat.mul_shuffle3.
  reflexivity.
Qed.

Corollary tr_fac_left_and_r_fac_right_are_equivalent :
  forall (n : nat),
    tr_fac_left n = r_fac_right n.
Proof.
  intros n.
  unfold tr_fac_left.
  unfold r_fac_right.
  exact (parafolding_left_and_right_over_peano_numbers
           nat
           (fun n' a : nat => S n' * a)
           succ_case_of_fac_is_left_permutative
           n
           1
        ).
Qed.

Lemma succ_case_of_Sigma_is_left_permutative :
  forall (f : nat -> nat),
    is_left_permutative nat (fun n' a : nat => a + f (S n')).
Proof.
  intro f.
  unfold is_left_permutative.
  intros n1 n2 v.
  Search (_ + _ + _).
  rewrite -> Nat.add_shuffle0.
  reflexivity.
Qed.

Corollary tr_Sigma_left_and_r_Sigma_right_are_equivalent :
  forall (n : nat)
    (f : nat -> nat),

    tr_Sigma_left n f = r_Sigma_right n f.
Proof.
  intros n f.
  unfold tr_Sigma_left.
  unfold r_Sigma_right.
  exact (parafolding_left_and_right_over_peano_numbers
           nat
           (fun n' a : nat => a + f (S n'))
           (succ_case_of_Sigma_is_left_permutative f)
           n
           (f 0)
        ).
Qed.
(* ********** *)

(* 7. Prove your similar theorem. *)

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

(* end of question-for-Yadunand.v *)