(* week-08_binomial-coefficients.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 15 Jun 2025, with Exercise 19 *)
(* was: *)
(* Version of 04 Apr 2025 *)
(* was: *)
(* Version of 31 Mar 2025 *)

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

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

Require Import Arith Bool.

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

(* N.B.: The redundant initial occurrence of true is to ensure a uniform layout,
   in a mechanism-not-solution sort of way. *)

(* ***** *)

Definition specification_of_binomial_coefficient (binomial_coefficient : nat -> nat -> nat) :=
  (forall n : nat,
      binomial_coefficient n 0 = 1)
  /\
  (forall k' : nat,
      binomial_coefficient 0 (S k') = 0)
  /\
  (forall n' k' : nat,
      binomial_coefficient (S n') (S k') = binomial_coefficient n' k' + binomial_coefficient n' (S k')).

(* ***** *)

(* testing inside Pascal's triangle: *)

Definition test_binomial_coefficient (candidate : nat -> nat -> nat) : bool :=
  true
    &&
    (Nat.eqb (candidate 0 0) 1)
    &&
    (true
       &&
       (Nat.eqb (candidate 1 0) 1)
       &&
       (Nat.eqb (candidate 1 1) 1))
    &&
    (true
       &&
       (Nat.eqb (candidate 2 0) 1)
       &&
       (Nat.eqb (candidate 2 1) 2)
       &&
       (Nat.eqb (candidate 2 2) 1))
    &&
    (true
       &&
       (Nat.eqb (candidate 3 0) 1)
       &&
       (Nat.eqb (candidate 3 1) 3)
       &&
       (Nat.eqb (candidate 3 2) 3)
       &&
       (Nat.eqb (candidate 3 3) 1))
    &&
    (true
       &&
       (Nat.eqb (candidate 4 0) 1)
       &&
       (Nat.eqb (candidate 4 1) 4)
       &&
       (Nat.eqb (candidate 4 2) 6)
       &&
       (Nat.eqb (candidate 4 3) 4)
       &&
       (Nat.eqb (candidate 4 4) 1))
    &&
    (true
       &&
       (Nat.eqb (candidate 5 0) 1)
       &&
       (Nat.eqb (candidate 5 1) 5)
       &&
       (Nat.eqb (candidate 5 2) 10)
       &&
       (Nat.eqb (candidate 5 3) 10)
       &&
       (Nat.eqb (candidate 5 4) 5)
       &&
       (Nat.eqb (candidate 5 5) 1)).

(* ***** *)

(* testing outside Pascal's triangle: *)

Definition test_binomial_coefficient' (candidate : nat -> nat -> nat) : bool :=
  true
    &&
    (Nat.eqb (candidate 0 1) 0)
    &&
    (Nat.eqb (candidate 1 2) 0)
    &&
    (Nat.eqb (candidate 2 3) 0)
    &&
    (Nat.eqb (candidate 3 4) 0).

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

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 testing_binomial_coefficient :
  test_binomial_coefficient binomial_coefficient = true
  /\
  test_binomial_coefficient' binomial_coefficient = true.
Proof.
  compute.
  split; reflexivity.
Qed.

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.

(* ***** *)

(* Exercise 12 *)

Proposition binomial_coefficient_satisfies_the_specification_of_binomial_coefficient :
  specification_of_binomial_coefficient binomial_coefficient.
Proof.
  unfold specification_of_binomial_coefficient.
  split.
  { intros [ | n'].
    - rewrite -> fold_unfold_binomial_coefficient_O.
      reflexivity.
    - rewrite -> fold_unfold_binomial_coefficient_S.
      reflexivity. }
  split.
  { intro k'.
    rewrite -> fold_unfold_binomial_coefficient_O.
    reflexivity. }
  intros n' k'.
  rewrite -> fold_unfold_binomial_coefficient_S.
  reflexivity.
Qed.

(* ***** *)

(* Exercise 13 *)

(* Binomial coefficients outside Pascal's triangle: *)

Property about_binomial_coefficients_n_more_than_n :
  forall n k : nat,
    n < k <-> binomial_coefficient n k = 0.
Proof.
Abort.

(* ***** *)

(* Exercise 14 *)

(* Binomial coefficients on the right edge of Pascal's triangle: *)

Property about_binomial_coefficients_n_n :
  forall n : nat,
    binomial_coefficient n n = 1.
Proof.
Abort.

(* ***** *)

(* Exercise 15 *)

(* Binomial coefficients on the left edge of Pascal's triangle: *)

Property about_binomial_coefficients_n_0 :
  forall n : nat,
    binomial_coefficient n 0 = 1.
Proof.
Abort.

(* ***** *)

(* Exercise 16 *)

(* Binomial coefficients in the second left layer of Pascal's triangle: *)

Property about_binomial_coefficients_n_1 :
  forall n : nat,
    binomial_coefficient n 1 = n.
Proof.
Abort.

(* ***** *)

(* Exercise 17 *)

(* Binomial coefficients in the second right layer of Pascal's triangle: *)

Property about_binomial_coefficients_Sk_k :
  forall k : nat,
    binomial_coefficient (S k) k = S k.
Proof.
Abort.

(* ***** *)

(* Exercise 18 *)

(* Each line in Pascal's triangle is a palindrome: *)

Property about_binomial_of_sums :
  forall a b : nat,
    binomial_coefficient (a + b) a = binomial_coefficient (a + b) b.
Proof.
  Compute (let f a b :=
             binomial_coefficient (a + b) a =? binomial_coefficient (a + b) b
           in (f 0 0 && f 0 1 && f 0 2 && f 0 3 && f 0 4 &&
               f 1 0 && f 1 1 && f 1 2 && f 1 3 && f 1 4 &&
               f 2 0 && f 2 1 && f 2 2 && f 2 3 && f 2 4 &&
               f 3 0 && f 3 1 && f 3 2 && f 3 3 && f 3 4)).
Abort.

(* ***** *)

(* Exercise 19 *)

Property another_square :
  forall n : nat,
    n * n = n + 2 * binomial_coefficient n 2.
Proof.
  Compute (let f n := n * n =? n + 2 * binomial_coefficient n 2 in
           f 0 && f 1 && f 2 && f 3 && f 4 && f 5).
Abort.

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

(* end of week-08_binomial-coefficients.v *)