(* mini-project-about-summations-that-start-above-zero.v *)
(* Time-stamp: <2025-07-11 14:46:50 olivier> *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 11 Jul 2025 *)

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

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

Require Import Arith Bool.

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

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

Lemma fold_unfold_Sigma0_O :
  forall (f : nat -> nat),
    Sigma0 0 f =
    f 0.
Proof.
  fold_unfold_tactic Sigma0.
Qed.

Lemma fold_unfold_Sigma0_S :
  forall (n' : nat)
         (f : nat -> nat),
    Sigma0 (S n') f =
    Sigma0 n' f + f (S n').
Proof.
  fold_unfold_tactic Sigma0.
Qed.

Definition sketchy_characterization_of_a_summation_function_that_starts_at_zero (Sigma0 : nat -> (nat -> nat) -> nat) :=
  forall f : nat -> nat,
    Sigma0 0 f = f 0
    /\
    Sigma0 1 f = f 0 + f 1
    /\
    Sigma0 2 f = f 0 + f 1 + f 2
    /\
    Sigma0 3 f = f 0 + f 1 + f 2 + f 3.

Proposition sketchy_characterization_of_Sigma0 :
  sketchy_characterization_of_a_summation_function_that_starts_at_zero Sigma0.
Proof.
  unfold sketchy_characterization_of_a_summation_function_that_starts_at_zero.
  intro f.
  unfold Sigma0.
  split; [ | split; [ | split]]; reflexivity.
Qed.

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

Definition specification_of_a_summation_function (Sigma : nat -> nat -> (nat -> nat) -> nat) :=
  (forall (x : nat)
          (f : nat -> nat),
      Sigma x x f = f x)
  /\
  (forall (x y : nat)
          (f : nat -> nat),
      x <= y ->
      Sigma x (S y) f = Sigma x y f + f (S y)).

(* ***** *)

Property sketchy_characterization_of_a_summation_function :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    forall (x : nat)
           (f : nat -> nat),
      Sigma x          x    f = f x
      /\
      Sigma x       (S x)   f = f x + f (S x)
      /\
      Sigma x    (S (S x))  f = f x + f (S x) + f (S (S x))
      /\
      Sigma x (S (S (S x))) f = f x + f (S x) + f (S (S x)) + f (S (S (S x))).
Proof.
  intros Sigma [S_Sigma_O S_Sigma_S] x f.
  assert (C0 : Sigma x x f = f x).
  { rewrite -> S_Sigma_O.
    reflexivity. }
  assert (C1 : Sigma x (S x) f = f x + f (S x)).
  { rewrite -> (S_Sigma_S x x f (Nat.le_refl x)).
    rewrite -> C0.
    reflexivity. }
  assert (C2 : Sigma x (S (S x)) f = f x + f (S x) + f (S (S x))).
  { rewrite -> (S_Sigma_S x (S x) f (Nat.le_succ_diag_r x)).
    rewrite -> C1.
    reflexivity. }
  assert (C3 : Sigma x (S (S (S x))) f = f x + f (S x) + f (S (S x)) + f (S (S (S x)))).
  { Check (Nat.le_trans x (S x) (S (S x)) (Nat.le_succ_diag_r x) (Nat.le_succ_diag_r (S x))).
    rewrite -> (S_Sigma_S x (S (S x)) f (Nat.le_trans x (S x) (S (S x)) (Nat.le_succ_diag_r x) (Nat.le_succ_diag_r (S x)))).
    rewrite -> C2.
    reflexivity. }
  split; [exact C0 | split; [exact C1 | split; [exact C2 | exact C3]]].
Qed.

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

(* Task 1: Simulating summations that may start above zero as instances of summations that start at zero *)

(* ***** *)

(* Task 1a *)

Theorem simulation_of_Sigma_as_an_instance_of_Sigma0 :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    forall x y : nat,
      x <= y ->
      forall f : nat -> nat,
        Sigma x y f = Sigma0 (y - x) (fun i => f (i + x)).
Proof.
Abort.

(* ***** *)

(* Task 1b *)

Property about_Sigma0_with_two_equivalent_functions :
  forall (x : nat)
         (f g : nat -> nat),
    (forall i : nat,
        f i = g i) ->
    Sigma0 x f = Sigma0 x g.
Proof.
Admitted. (* proved in week-10_formalizing-summations.v *)

Property about_Sigma_with_two_equivalent_functions :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    forall x y : nat,
      x <= y ->
      forall f g : nat -> nat,
        (forall i : nat,
            f i = g i) ->
        Sigma x y f = Sigma x y g.
Proof.
Abort.

(* ***** *)

(* Task 1c *)

Theorem self_simulation_of_Sigma_as_an_instance_of_Sigma0 :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    forall (y : nat)
           (f : nat -> nat),
      Sigma 0 y f = Sigma0 y f.
Proof.
Abort.

(* ***** *)

(* Task 1d *)

Theorem simulation_of_Sigma_as_an_up_instance_of_Sigma :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    forall x y : nat,
      x <= y ->
      forall (f : nat -> nat)
             (z : nat),
        Sigma x y f = Sigma (x + z) (y + z) (fun i => f (i - z)).
Proof.
Abort.

(* ***** *)

(* Task 1e *)

Theorem simulation_of_Sigma_as_a_down_instance_of_Sigma :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    forall x y : nat,
      x <= y ->
      forall (f : nat -> nat)
             (z : nat),
        z <= x ->
        Sigma x y f = Sigma (x - z) (y - z) (fun i => f (i + z)).
Proof.
Abort.

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

(* Task 2: Tailoring an induction principle *)

Lemma nat_ind_shifted :
  forall (m : nat)
         (P : nat -> Prop),
    P m ->
    (forall n' : nat,
        m <= n' -> P n' -> P (S n')) ->
    forall n : nat,
      m <= n -> P n.
Proof.
Admitted.

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

(* Task 3: Revisiting the simulation using the tailored induction principle *)

Theorem simulation_of_Sigma_as_an_instance_of_Sigma0_using_nat_ind_shifted :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    forall x y : nat,
      x <= y ->
      forall f : nat -> nat,
        Sigma x y f = Sigma0 (y - x) (fun i => f (i + x)).
Proof.
  intros Sigma [S_Sigma_O S_Sigma_S] x y le_x_y f.
  Check (nat_ind_shifted
           x
           (fun y : nat => Sigma x y f = Sigma0 (y - x) (fun i : nat => f (i + x)))).
Abort.

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

(* Task 4: Summing binomial coefficients *)

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

Lemma fold_unfold_binomial_coefficient_O :
  forall k : nat,
    binomial_coefficient 0 k =
    match k with
      O =>
      1
    | S k' =>
      0
    end.
Proof.
  fold_unfold_tactic binomial_coefficient.
Qed.

Lemma fold_unfold_binomial_coefficient_S :
  forall n' k : nat,
    binomial_coefficient (S n') k =
    match k with
      O =>
      1
    | S k' =>
      binomial_coefficient n' k' + binomial_coefficient n' (S k')
    end.
Proof.
  fold_unfold_tactic binomial_coefficient.
Qed.

(* ***** *)

Property about_binomial_coefficients_n_more_than_n :
  forall n k : nat,
    n < k <-> binomial_coefficient n k = 0.
Proof.
Admitted. (* Exercise 13 in week-08_binomial-coefficients.v *)

Property about_binomial_coefficients_n_n :
  forall n : nat,
    binomial_coefficient n n = 1.
Proof.
Admitted. (* Exercise 14 in week-08_binomial-coefficients.v *)

Property about_binomial_coefficients_n_0 :
  forall n : nat,
    binomial_coefficient n 0 = 1.
Proof.
Admitted. (* Exercise 15 in week-08_binomial-coefficients.v *)

Property about_binomial_coefficients_n_1 :
  forall n : nat,
    binomial_coefficient n 1 = n.
Proof.
Admitted. (* Exercise 16 in week-08_binomial-coefficients.v *)

(* ***** *)

Property warmup :
  forall n : nat,
    Sigma0 n (fun i => binomial_coefficient i 0) = S n.
Proof.
  Compute (let f n := Sigma0 n (fun i => binomial_coefficient i 0) =? S n in
           f 0 && f 1 && f 2 && f 3).
Abort.

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

(* Task 5: The hockey-stick identity *)

Lemma sketchy_characterization_of_the_hockey_stick_identity_first_shot :
  binomial_coefficient 3 3 =
  binomial_coefficient 4 4
  /\
  binomial_coefficient 2 2 + binomial_coefficient 3 2 =
  binomial_coefficient 4 3
  /\
  binomial_coefficient 1 1 + binomial_coefficient 2 1 + binomial_coefficient 3 1 =
  binomial_coefficient 4 2
  /\
  binomial_coefficient 0 0 + binomial_coefficient 1 0 + binomial_coefficient 2 0 + binomial_coefficient 3 0 =
  binomial_coefficient 4 1.
Proof.
  compute.
  split; [ | split; [ | split]]; reflexivity.
Qed.  

Lemma sketchy_characterization_of_the_hockey_stick_identity_second_shot :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    Sigma 3 3 (fun i => binomial_coefficient i 3) = binomial_coefficient 4 4
    /\
    Sigma 2 3 (fun i => binomial_coefficient i 2) = binomial_coefficient 4 3
    /\
    Sigma 1 3 (fun i => binomial_coefficient i 1) = binomial_coefficient 4 2
    /\
    Sigma 0 3 (fun i => binomial_coefficient i 0) = binomial_coefficient 4 1.
Proof.
  intros Sigma [S_Sigma_O S_Sigma_S].
  assert (le_0_3 :
            0 <= 3).
  { Search (_ <= S _).
    Check (Nat.le_le_succ_r 0 2 Nat.le_0_2).
    exact (Nat.le_le_succ_r 0 2 Nat.le_0_2). }
  split; [ | split; [ | split]].
  - rewrite -> S_Sigma_O.
    compute.
    reflexivity.
  - rewrite -> (S_Sigma_S 2 2 (fun i : nat => binomial_coefficient i 2) (Nat.le_refl 2)).
    rewrite -> S_Sigma_O.
    compute.
    reflexivity.
  - rewrite -> (S_Sigma_S 1 2 (fun i : nat => binomial_coefficient i 1) (Nat.le_succ_diag_r 1)).
    rewrite -> (S_Sigma_S 1 1 (fun i : nat => binomial_coefficient i 1) (Nat.le_refl 1)).
    rewrite -> S_Sigma_O.
    compute.
    reflexivity.
  - rewrite -> (S_Sigma_S 0 2 (fun i : nat => binomial_coefficient i 0) Nat.le_0_2).
    rewrite -> (S_Sigma_S 0 1 (fun i : nat => binomial_coefficient i 0) Nat.le_0_1).
    rewrite -> (S_Sigma_S 0 0 (fun i : nat => binomial_coefficient i 0) (Nat.le_refl 0)).
    rewrite -> S_Sigma_O.
    compute.
    reflexivity.
Qed.

Lemma hockey_stick_identity_shifted :
  forall n k : nat,
    k <= n ->
    Sigma0 (n - k) (fun i => binomial_coefficient (i + k) k) = binomial_coefficient (S n) (S k).
Proof.
  Compute (let f n k := Sigma0 (n - k) (fun i => binomial_coefficient (i + k) k) =? binomial_coefficient (S n) (S k) in
           f 0 0 && f 1 0 && f 1 1 && f 2 0 && f 1 0 && f 0 0).
Abort.

Theorem hockey_stick_identity :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    forall n k : nat,
      k <= n ->
      Sigma k n (fun i => binomial_coefficient i k) = binomial_coefficient (S n) (S k).
Proof.
Abort.

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

(* Task 6: Summing one up *)

Lemma summing_one_up_shifted :
  forall a b : nat,
    S a <= b ->
    forall f : nat -> nat,
      f a + Sigma0 (b - S a) (fun i => f (i + S a)) = Sigma0 (b - a) (fun i => f (i + a)).
Proof.
Abort.

Theorem summing_one_up :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    forall a b : nat,
      S a <= b ->
      forall f : nat -> nat,
        f a + Sigma (S a) b f = Sigma a b f.
Proof.
Abort.

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

(* Task 7: Summing up and up *)

Theorem summing_up_and_up :
  forall Sigma : nat -> nat -> (nat -> nat) -> nat,
    specification_of_a_summation_function Sigma ->
    forall x y : nat,
      x <= y ->
      forall z : nat,
        S y <= z ->
        forall f : nat -> nat,
          Sigma x y f + Sigma (S y) z f = Sigma x z f.
Proof.
Abort.

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

(* Task 8: A summation function that starts at one *)

Definition sketchy_characterization_of_a_summation_function_that_starts_at_one (Sigma1 : nat -> (nat -> nat) -> nat) :=
  forall f : nat -> nat,
    (Sigma1 1 f = f 1)
    /\
    (Sigma1 2 f = f 1 + f 2)
    /\
    (Sigma1 3 f = f 1 + f 2 + f 3).

Fixpoint Sigma1 (n : nat) (f : nat -> nat) : nat :=
  0. (* <-- FIX ME PLEASE*)

Proposition sketchy_characterization_of_Sigma1 :
  sketchy_characterization_of_a_summation_function_that_starts_at_one Sigma1.
Proof.
Abort.

(* ***** *)

Definition Sigma1_alt (n : nat) (f : nat -> nat) : nat :=
  0. (* <-- FIX ME PLEASE*)

(* ***** *)

Theorem Sigma1_and_Sigma1_alt_are_functionally_equal :
  forall (n : nat)
         (f : nat -> nat),
    Sigma1 n f = Sigma1_alt n f.
Proof.
Abort.

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

(* Task 9: Properties of the summation function that starts at one *)

(* ***** *)

Property about_Sigma1_with_two_equivalent_functions :
  forall (x : nat)
         (f g : nat -> nat),
    (forall i : nat,
        f i = g i) ->
    Sigma1 x f = Sigma1 x g.
Proof.
Admitted.

(* ***** *)

Property about_Sigma1_with_an_additive_function :
  forall (x : nat)
         (f g : nat -> nat),
    Sigma1 x (fun i => f i + g i) = Sigma1 x f + Sigma1 x g.
Proof.
Admitted.

(* ***** *)

Property about_Sigma1_with_a_constant_function :
  forall x c : nat,
    Sigma1 x (fun _ => c) = x * c.
Proof.
Admitted.

(* ***** *)

Property about_swapping_Sigma1 :
  forall (x y : nat)
         (f : nat -> nat -> nat),
    Sigma1 x (fun i => Sigma1 y (fun j => f i j)) = Sigma1 y (fun j => Sigma1 x (fun i => f i j)).
Proof.
Admitted.

(* ***** *)

Property about_Sigma1_with_the_identity_function :
  forall x : nat,
    2 * Sigma1 x (fun i => i) = x * S x.
Proof.
Admitted.

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

(* Task 10: Putting Sigma1 to work *)

(* ***** *)

Property to_sum_up_with_Sigma1 :
  forall x y : nat,
    2 * Sigma1 x (fun i => Sigma1 y (fun j => i + j)) = x * y * (x + y + 2).
Proof.
Abort.

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

(* end of mini-project-about-summations-that-may-start-above-zero.v *)