(* week-08_the-abstraction-and-instantiation-of-Eureka-lemmas-about-resetting-the-accumulator.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 13 Mar 2025 *)

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

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

Require Import Arith Bool List.

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

Definition make_Eureka_lemma (A : Type) (id_A : A) (combine_A : A -> A -> A) (c : A -> A) (a : A) : Prop :=
  c a = combine_A (c id_A) a.

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

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

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

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.

Check (make_Eureka_lemma nat).
Check (make_Eureka_lemma nat 1).
Check (make_Eureka_lemma nat 1).
Check (make_Eureka_lemma nat 1 Nat.mul).
Check (forall x n a : nat, make_Eureka_lemma nat 1 Nat.mul (power_acc x n) a).

Lemma about_power_acc :
  forall x n a : nat,
    power_acc x n a = power_acc x n 1 * a.
Proof.
  intros x n.
  induction n as [ | n' IHn']; intro a.
  - rewrite ->2 fold_unfold_power_acc_O.
    exact (eq_sym (Nat.mul_1_l a)).
  - rewrite ->2 fold_unfold_power_acc_S.
    rewrite -> Nat.mul_1_r.
    rewrite -> (IHn' (x * a)).
    rewrite -> (IHn' x).
    Check Nat.mul_assoc.
    apply Nat.mul_assoc.
Qed.

Lemma about_power_acc_generically :
  forall x n a : nat,
    make_Eureka_lemma nat 1 Nat.mul (power_acc x n) a.
Proof.
  unfold make_Eureka_lemma.
  exact about_power_acc.
Qed.

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

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

Definition add_alt (n m : nat) : nat :=
  add_acc n m.

Lemma fold_unfold_add_acc_O :
  forall a : nat,
    add_acc 0 a =
    a.
Proof.
  fold_unfold_tactic add_acc.
Qed.

Lemma fold_unfold_add_acc_S :
  forall n' a : nat,
    add_acc (S n') a =
    add_acc n' (S a).
Proof.
  fold_unfold_tactic add_acc.
Qed.

Lemma about_add_acc :
  forall n a : nat,
    add_acc n a = add_acc n 0 + a.
Proof.
  intro n.
  induction n as [ | n' IHn']; intro a.
  - rewrite ->2 fold_unfold_add_acc_O.
    exact (eq_sym (Nat.add_0_l a)).
  - rewrite ->2 fold_unfold_add_acc_S.
    rewrite -> (IHn' (S a)).
    rewrite -> (IHn' 1).
    rewrite <- Nat.add_assoc.
    rewrite -> (Nat.add_1_l a).
    reflexivity.
Qed.

Lemma about_add_acc_generically :
  forall n a : nat,
    make_Eureka_lemma nat 0 Nat.add (add_acc n) a.
Proof.
  unfold make_Eureka_lemma.
  exact about_add_acc.
Qed.

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

(* Exercise 01 *)

Fixpoint length_acc (V : Type) (vs : list V) (a : nat) : nat :=
  match vs with
    nil =>
    a
  | v :: vs' =>
    length_acc V vs' (S a)
  end.

Definition length_alt (V : Type) (vs : list V) : nat :=
  length_acc V vs 0.

(*
Lemma about_length_acc :
*)

(*
Lemma about_length_acc_generically :
*)

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

(* Exercise 02 *)

Fixpoint list_append (V : Type) (v1s v2s : list V) : list V :=
  match v1s with
    nil =>
    v2s
  | v1 :: v1s' =>
    v1 :: list_append V v1s' v2s
  end.

Fixpoint reverse_acc (V : Type) (vs a : list V) : list V :=
  match vs with
    nil =>
    a
  | v :: vs' =>
    reverse_acc V vs' (v :: a)
  end.

Definition reverse_alt (V : Type) (vs : list V) : list V :=
  reverse_acc V vs nil.

(*
Lemma about_reverse_acc :
*)

(*
Lemma about_reverse_acc_generically :
*)

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

(* Exercise 03 *)

Fixpoint list_fold_left (V W : Type) (nil_case : W) (cons_case : V -> W -> W) (vs : list V) : W :=
  match vs with
    nil =>
      nil_case
  | v :: vs' =>
      list_fold_left V W (cons_case v nil_case) cons_case vs'
  end.

(*
Lemma about_list_fold_left :
*)

(*
Lemma about_list_fold_left_generically :
*)

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

(* Exercise 04 *)

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

Definition fac_alt (n : nat) : nat :=
  fac_acc n 1.

Lemma fold_unfold_fac_acc_O :
  forall a : nat,
    fac_acc 0 a =
    a.
Proof.
  fold_unfold_tactic fac_acc.
Qed.

Lemma fold_unfold_fac_acc_S :
  forall n' a : nat,
    fac_acc (S n') a =
    fac_acc n' (S n' * a).
Proof.
  fold_unfold_tactic fac_acc.
Qed.

(*
Lemma about_fac_acc :
*)

(*
Lemma about_fac_acc_generically :
*)

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

(* Exercise 05 *)

Inductive binary_tree : Type :=
| Leaf : nat -> binary_tree
| Node : binary_tree -> binary_tree -> binary_tree.

(* ***** *)

Fixpoint weight (t : binary_tree) : nat :=
  match t with
  | Leaf n =>
    n
  | Node t1 t2 =>
    weight t1 + weight t2
  end.

Lemma fold_unfold_weight_Leaf :
  forall n : nat,
    weight (Leaf n) = n.
Proof.
  fold_unfold_tactic weight.
Qed.

Lemma fold_unfold_weight_Node :
  forall t1 t2 : binary_tree,
    weight (Node t1 t2) = weight t1 + weight t2.
Proof.
  fold_unfold_tactic weight.
Qed.

(* ***** *)

Fixpoint weight_acc (t : binary_tree) (a : nat) : nat :=
  match t with
  | Leaf n =>
    n + a
  | Node t1 t2 =>
    weight_acc t1 (weight_acc t2 a)
  end.

Definition weight_alt (t : binary_tree) : nat :=
  weight_acc t 0.

Lemma fold_unfold_weight_acc_Leaf :
  forall n a : nat,
    weight_acc (Leaf n) a = n + a.
Proof.
  fold_unfold_tactic weight_acc.
Qed.

Lemma fold_unfold_weight_acc_Node :
  forall (t1 t2 : binary_tree)
         (a : nat),
    weight_acc (Node t1 t2) a = weight_acc t1 (weight_acc t2 a).
Proof.
  fold_unfold_tactic weight_acc.
Qed.

(*
Lemma about_weight_acc :
*)

(*
Lemma about_weight_acc_generically :
*)

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

(* end of week-08_the-abstraction-and-instantiation-of-Eureka-lemmas-about-resetting-the-accumulator.v *)