(* week-10_formalizing-summations.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 20 Apr 2025 *)
(* was: *)
(* Version of 28 Mar 2025 *)

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

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

Require Import Arith.

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

(* To start with, here are a specification of Sigma0
   and a recursive implementation that satisfies this specification. *)

(* ***** *)

Definition specification_of_Sigma0 (Sigma0 : nat -> (nat -> nat) -> nat) :=
  forall f : nat -> nat,
    Sigma0 0 f = f 0
    /\
    forall n' : nat,
      Sigma0 (S n') f = Sigma0 n' f + f (S n').

(* ***** *)

Fixpoint Sigma0 (n : nat) (f : nat -> nat) : nat :=
  match n with
  | O =>
    f 0
  | S n' =>
    Sigma0 n' f + f 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.

(* ***** *)

Theorem Sigma0_satisfies_the_specification_of_Sigma0 :
  specification_of_Sigma0 Sigma0.
Proof.
  unfold specification_of_Sigma0.
  intro f.
  split.
  - exact (fold_unfold_Sigma0_O f).
  - intro n'.
    exact (fold_unfold_Sigma0_S n' f).
Qed.

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

(* Then here is a series of properties of Sigma0. *)

(* ***** *)

Property about_factoring_a_multiplicative_constant_on_the_right_in_Sigma0 :
  forall (x c : nat)
         (f : nat -> nat),
    Sigma0 x (fun i => f i * c) = Sigma0 x f * c.
Proof.
Abort.

(* ***** *)

Property about_factoring_a_multiplicative_constant_on_the_left_in_Sigma0 :
  forall (x c : nat)
         (f : nat -> nat),
    Sigma0 x (fun i => c * f i) = c * Sigma0 x f.
Proof.
Abort.

(* ***** *)

Property about_swapping_Sigma0 :
  forall (x y : nat)
         (f : nat -> nat -> nat),
    Sigma0 x (fun i => Sigma0 y (fun j => f i j)) = Sigma0 y (fun j => Sigma0 x (fun i => f i j)).
Proof.
Abort.

(* ***** *)

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

(* ***** *)

Property about_Sigma0_with_two_equivalent_functions_up_to_the_bound :
  forall (x : nat)
         (f g : nat -> nat),
    (forall i : nat,
        i <= x ->
        f i = g i) ->
    Sigma0 x f = Sigma0 x g.
Proof.
Abort.

(* ***** *)

Property about_Sigma0_with_an_additive_function :
  forall (x : nat)
         (f g : nat -> nat),
    Sigma0 x (fun i => f i + g i) = Sigma0 x f + Sigma0 x g.
Proof.
Abort.

(* ***** *)

Property about_Sigma0_with_a_constant_function :
  forall x y : nat,
    Sigma0 x (fun _ => y) = y * (S x).
Proof.
Abort.

(* ***** *)

Property about_Sigma0_with_two_small_a_function :
  forall (x : nat)
         (f : nat -> nat),
    (forall i : nat,
        i <= x ->
        f i = 0) ->
    Sigma0 x f = 0.
Proof.
Abort.

(* ***** *)

Property about_Sigma0_up_to_a_positive_sum :
  forall (x y : nat)
         (f : nat -> nat),
    Sigma0 (x + S y) f = Sigma0 x f + Sigma0 y (fun i => f (x + S i)).
Proof.
Abort.

(* ***** *)

Property about_Sigma0_specifically_left :
  forall (x y : nat)
         (f : nat -> nat),
    Sigma0 (x * S y + y) f = Sigma0 x (fun i => Sigma0 y (fun j => f (i * S y + j))).
Proof.
Abort.

(* ***** *)

Property about_Sigma0_up_to_a_positive_product_left :
  forall (x y : nat)
         (f : nat -> nat),
    Sigma0 (S x * S y) f = Sigma0 (x * S y + y) f + f (S x * S y).
Proof.
Abort.

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

(* Applications: *)

(* ***** *)

(* Prove the following theorem and its corollary without using simpl: *)

Theorem twice_a_triangular_number :
  forall n : nat,
    2 * Sigma0 n (fun x : nat => x) = n * S n.
Proof.
Abort.

Corollary the_product_of_two_consecutive_Peano_numbers_is_even :
  forall n : nat,
    exists q : nat,
      n * S n = 2 * q.
Proof.
Abort.

(* ***** *)

(* Prove the following theorem
   as a corollary of the properties of summation that you have proved so far.
   Write two proofs:
   - one where you apply properties without arguments, and
   - one where you apply properties with all their arguments. *)

Theorem an_affine_summation :
  forall a b n : nat,
    Sigma0 n (fun x : nat => a * x + b) = a * Sigma0 n (fun x : nat => x) + b * S n.
Proof.
  intros a b n.
  (* ... *)

  Restart.

  intros a b n.
  (* ... *)
Abort.

(* ***** *)

(* Prove the following theorem
   (1) as a corollary of the properties that you have proved so far, and then
   (2) by induction. *)

Theorem about_the_sum_of_the_first_odd_numbers :
  forall n : nat,
    Sigma0 n (fun i => S (2 * i)) = S n * S n.
Proof.
  intro n.
  (* ... *)

  Restart.

  intro n.
  (* ... *)
Abort.

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

(* Here are a specification of Sigma1
   and a recursive implementation that satisfies this specification. *)

(* ***** *)

Definition specification_of_Sigma1 (Sigma1 : nat -> (nat -> nat) -> nat) :=
  forall f : nat -> nat,
    Sigma1 0 f = 0
    /\
    forall n' : nat,
      Sigma1 (S n') f = Sigma1 n' f + f (S n').

Theorem there_is_at_most_one_Sigma1_function :
  forall x : nat -> (nat -> nat) -> nat,
    specification_of_Sigma1 x ->
    forall y : nat -> (nat -> nat) -> nat,
      specification_of_Sigma1 y ->
      forall (n : nat)
             (f : nat -> nat),
        x n f = y n f.
Proof.
Abort.

(* ***** *)

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

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

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

Theorem Sigma1_satisfies_the_specification_of_Sigma1 :
  specification_of_Sigma1 Sigma1.
Proof.
  unfold specification_of_Sigma1.
  intro f.
  split.
  - exact (fold_unfold_Sigma1_O f).
  - intro n'.
    exact (fold_unfold_Sigma1_S n' f).
Qed.

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

Property about_Sigma1 :
  forall f : nat -> nat,
    f 0 = 0 ->
    forall n : nat,
      Sigma1 n f = Sigma0 n f.
Proof.
Abort.

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

(* Implement Sigma1 by cases:
   - in the O case, the result should be 0; and
   - in the S case, the result should be a call to Sigma0. *)

Definition Sigma1' (n : nat) (f : nat -> nat) : nat :=
  match n with
    O =>
    0
  | S n' =>
    0 (* <-- FIXMEPLEASE *)
  end.

Theorem Sigma1'_satisfies_the_specification_of_Sigma1 :
  specification_of_Sigma1 Sigma1'.
Proof.
Abort.

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

Property about_Sigma1' :
  forall f : nat -> nat,
    f 0 = 0 ->
    forall n : nat,
      Sigma1' n f = Sigma0 n f.
Proof.
Abort.

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

(* end of week-10_formalizing-summations.v *)