(* week-01_functional-programming-in-Gallina.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 16 Feb 2025, with uniformly formatted unit-test functions *)
(* was: *)
(* Version of 30 Jan 2025, with a version of testing_the_conjecture_about_baz_x and of testing_the_conjecture_about_baz_y that is aligned with the informal description in the comments just before *)
(* was: *)
(* Version of 17 Jan 2025, writing "eqb" instead of "beq" *)
(* was: *)
(* Version of 17 Jan 2025 *)

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

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

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

Require Import Arith Bool. (* The two basic libraries about nat and bool. *)

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

Check 0.

Check O.

(* Note: "nat" is the type of natural numbers. *)

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

Check 1.

Check (S 0).

Check (S O).

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

Check 2.

Check (S (S 0)).

Check (S (S O)).

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

Check 3.

Compute 3.

(* Note: natural numbers are self-evaluating. *)

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

Compute (4 + 6).

Check (4 + 6).

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

Compute (plus 4 6).

Check (plus 4 6).

(* Note: infix + is syntactic sugar for plus. *)

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

Definition three := 3.

Check three.

Compute three.

Definition ten := 4 + 6.

Check ten.

Compute ten.

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

Check (1, false).

Check (fun (x : nat) => 2).

Check (fun (x : nat) => x).

Check (fun (x : nat) => S x).

Check (fun (n : nat) => fun (b : bool) => (n, b)).

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

(* The following definitions are all equivalent
   because they are parsed into the same abstract-syntax tree: *)

Definition succ_v0 : nat -> nat :=
  fun m : nat => S m.

Definition succ_v1 :=
  fun m => S m.

Definition succ_v2 (m : nat) :=
  S m.

Definition succ_v3 (m : nat) : nat :=
  S m.

Definition succ_v4 m :=
  S m.

(* Note: the definition of succ_v3 is the recommended one here. *)

(* Note: variables are defined once and for all in a file. *)

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

(* Ditto for the following definitions: *)

Definition zerop_v0 : nat -> bool :=
  fun n =>
    match n with
    | O =>
      true
    | S n' =>
      false
    end.

Compute (zerop_v0 0). (* = true : bool *)
Compute (zerop_v0 7). (* = false : bool *)

Definition zerop_v1 (n : nat) : bool :=
  match n with
  | O =>
    true
  | S n' =>
    false
  end.

Compute (zerop_v1 0). (* = true : bool *)
Compute (zerop_v1 7). (* = false : bool *)

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

(* The identity function: *)

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

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

(* What does foo do? *)

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

Compute (foo 0, foo 1, foo 2, foo 3, foo 4).

(* Testing suggests that foo multiplies its argument by 2:
   for all a and b of type nat,
   if applying foo to a yields b
   then b = 2 * a.
 *)

Definition testing_the_conjecture_about_foo (a : nat) : bool :=
  let b := foo a in
  Nat.eqb b (2 * a).

Compute ((testing_the_conjecture_about_foo 0)
         &&
         (testing_the_conjecture_about_foo 1)
         &&
         (testing_the_conjecture_about_foo 2)
         &&
         (testing_the_conjecture_about_foo 3)
         &&
         (testing_the_conjecture_about_foo 4)
         &&
         (testing_the_conjecture_about_foo 5)).

(* Soon we will prove this conjecture rather than test it. *)

(* ***** *)

(* What does bar do? *)

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

Compute (bar 0, bar 1, bar 2, bar 3, bar 4).

(* Testing suggests that bar multiplies its argument by 3:
   for all a and b of type nat,
   if applying bar to a yields b
   then b = 3 * a.
 *)

Definition testing_the_conjecture_about_bar (a : nat) : bool :=
  let b := bar a in
  Nat.eqb b (3 * a).

Compute ((testing_the_conjecture_about_bar 0)
         &&
         (testing_the_conjecture_about_bar 1)
         &&
         (testing_the_conjecture_about_bar 2)
         &&
         (testing_the_conjecture_about_bar 3)
         &&
         (testing_the_conjecture_about_bar 4)
         &&
         (testing_the_conjecture_about_bar 5)).

(* Soon we will prove this conjecture rather than test it. *)

(* ***** *)

(* What do baz_x and baz_y do? *)

Fixpoint baz_aux (n : nat) (b : bool) : nat :=
  match n with
    O =>
    O
  | S n' =>
    if b
    then baz_aux n' (negb b)
    else S (baz_aux n' (negb b))
  end.

Definition baz_x (n : nat) : nat :=
  baz_aux n true.

Compute (baz_x 0, baz_x 1, baz_x 2, baz_x 3, baz_x 4, baz_x 5, baz_x 6, baz_x 7, baz_x 8, baz_x 9).

(* Testing suggests that baz_x divides its argument by 2:
   for all a and b of type nat,
   if applying baz_x to 2 * a yields b
   then b = a
   and
   if applying baz_x to 2 * a + 1 yields b
   then b = a. *)

Definition testing_the_conjecture_about_baz_x (a : nat) : bool :=
  (let b_even := baz_x (2 * a) in Nat.eqb b_even a)
  &&
  (let b_odd := baz_x (S (2 * a)) in Nat.eqb b_odd a).

Compute ((testing_the_conjecture_about_baz_x 0)
         &&
         (testing_the_conjecture_about_baz_x 1)
         &&
         (testing_the_conjecture_about_baz_x 2)
         &&
         (testing_the_conjecture_about_baz_x 3)
         &&
         (testing_the_conjecture_about_baz_x 4)
         &&
         (testing_the_conjecture_about_baz_x 5)).

(* Soon we will prove this conjecture rather than test it. *)

Definition baz_y (n : nat) : nat :=
  baz_aux n false.

Compute (baz_y 0, baz_y 1, baz_y 2, baz_y 3, baz_y 4, baz_y 5, baz_y 6, baz_y 7, baz_y 8, baz_y 9).

(* Testing suggests that baz_y divides its argument by 2:
   for all a and b of type nat,
   if applying baz_y to 2 * a yields b
   then b = a
   and
   if applying baz_y to 2 * a + 1 yields b
   then b = a + 1. *)

Definition testing_the_conjecture_about_baz_y (a : nat) : bool :=
  (let b := baz_y (2 * a) in Nat.eqb b a)
  &&
  (let b := baz_y (S (2 * a)) in Nat.eqb b (S a)).

Compute ((testing_the_conjecture_about_baz_x 0)
         &&
         (testing_the_conjecture_about_baz_y 1)
         &&
         (testing_the_conjecture_about_baz_y 2)
         &&
         (testing_the_conjecture_about_baz_y 3)
         &&
         (testing_the_conjecture_about_baz_y 4)
         &&
         (testing_the_conjecture_about_baz_y 5)).

(* Soon we will prove this conjecture rather than test it. *)

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

(* The addition function: *)

(* Unit tests: *)

Definition test_add (candidate: nat -> nat -> nat) : bool :=
  true
    &&
    (Nat.eqb (candidate 0 0) 0)
    &&
    (Nat.eqb (candidate 0 1) 1)
    &&
    (Nat.eqb (candidate 1 0) 1)
    &&
    (Nat.eqb (candidate 1 1) 2)
    &&
    (Nat.eqb (candidate 1 2) 3)
    &&
    (Nat.eqb (candidate 2 1) 3)
    &&
    (Nat.eqb (candidate 2 2) 4)
    &&
    (* commutativity: *)
    (Nat.eqb (candidate 2 10) (candidate 10 2))
    &&
    (* associativity: *)
    (Nat.eqb (candidate 2 (candidate 5 10))
             (candidate (candidate 2 5) 10))
(* etc. *)
.

(* Testing the unit-test function: *)

Compute (test_add plus).

(* Version 1: lambda-dropped *)

Definition add_v1 (n j : nat) : nat :=
  let fix visit i :=
    match i with
      O =>
      j
    | S i' =>
      S (visit i')
    end
  in visit n.

Compute (test_add add_v1).

(* Version 2: recursive, lambda lifted *)

Fixpoint add_v2 (i j : nat) : nat :=
  match i with
    O =>
    j
  | S i' =>
    S (add_v2 i' j)
  end.

Compute (test_add add_v2).

(* Version 3: tail recursive *)

Fixpoint add_v3 (i j : nat) : nat :=
  match i with
    O =>
    j
  | S i' =>
    add_v3 i' (S j)
  end.

Compute (test_add add_v3).

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

(* The multiplication function: *)

(*
   Given an integer j,
 
   * base case: multiplying 0 and j yields 0;
 
   * induction step: given a number i' such that multiplying it and j yields ih
     (which is the induction hypothesis),
     multiplying S i' and j should yield j + ih.
*)

(* ***** *)

(* Unit tests: *)

Definition test_mult (candidate: nat -> nat -> nat) : bool :=
  true
(* etc. *)
.

(* ***** *)

(* Testing the unit-test function: *)

(*
Compute (test_mult mult).
*)

(* ***** *)

(* Version 1: lambda-dropped *)

(*
Fixpoint mult_v1 (n j : nat) : nat :=
  ...

Compute (test_mult mult_v1).
*)

(* ***** *)

(* Version 2: lambda-lifted *)

(*
Fixpoint mult_v2 (i j : nat) : nat :=
  ...

Compute (test_mult mult_v2).
*)

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

(* The exponentiation function: *)

(*
   Given an integer x,
 
   * base case: exponentiating x with 0 yields 1;
 
   * induction step: given a number i' such that exponentiating x with i' it and j yields ih
     (which is the induction hypothesis),
     exponentiating x with S i' should yield x * ih.
*)

(* Unit tests: *)

Definition test_power (candidate: nat -> nat -> nat) : bool :=
  true
(* etc. *)
.

(* ***** *)

(* Version 1: lambda-dropped *)

(*
Definition power_v1 (x n : nat) : nat :=
  ...

Compute (test_power power_v1).
*)

(* ***** *)

(* Version 2: lambda-lifted *)

(*
Fixpoint power_v2 (x n : nat) : nat :=
  ...

Compute (test_power power_v2).
*)

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

(* The factorial function: *)

(*
   * base case: the factorial of 0 is 1;
 
   * induction step: given a number i' such that the factorial of i' is ih
     (which is the induction hypothesis),
     the factorial of S i' is (S i') * ih.
*)

(* Unit tests: *)

Definition test_fac (candidate: nat -> nat) : bool :=
  true
(* etc. *)
.

(* ***** *)

(* Version 1: recursive *)

(*
Fixpoint fac_v1 (n : nat) : nat :=
  ...

Compute (test_fac fac_v1).
*)

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

(* The fibonacci function: *)

(*
   * base case #1: the fibonacci number at index 0 is 0
 
   * base case #2: the fibonacci number at index 1 is 1
 
   * induction step: given a number i' such that
     the fibonacci number at index i' is fib_i' (which is the first induction hypothesis)
     and
     the fibonacci number at index S i' is fib_Si' (which is the first induction hypothesis),
     the fibonacci number at index S (S i') is fib_i' + fib_Si'
*)

(* ***** *)

(* Unit tests: *)

Definition test_fib (candidate: nat -> nat) : bool :=
  true
(* etc. *)
.

(* ***** *)

(* Version 1: recursive *)

(*
Fixpoint fib_v1 (n : nat) : nat :=
  ...

(* hint: make sure to read the interludes in the exercise chapter *)

Compute (test_fib fib_v1).
*)

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

(* The even predicate: *)

(* ***** *)

(* Unit tests: *)

Definition test_evenp (candidate: nat -> bool) : bool :=
  true
    &&
    (Bool.eqb (candidate 0) true)
    &&
    (Bool.eqb (candidate 1) false)
(* etc. *)
.

(* ***** *)

(* Version 1: recursive *)

(*
Fixpoint evenp_v1 (n : nat) : bool :=
  ...

Compute (test_evenp evenp_v1).
*)

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

(* The odd predicate: *)

(*
...
*)

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

(* Binary trees of natural numbers with payloads in the leaves: *)

Inductive binary_tree_nat : Type :=
  Leaf_nat : nat -> binary_tree_nat
| Node_nat : binary_tree_nat -> binary_tree_nat -> binary_tree_nat.

(* An equality predicate for binary trees of natural numbers
   with payloads in the leaves: *)

Fixpoint eqb_binary_tree_nat (t1 t2 : binary_tree_nat) : bool :=
  match t1 with
    Leaf_nat n1 =>
    match t2 with
      Leaf_nat n2 =>
      Nat.eqb n1 n2
    | Node_nat t21 t22 =>
      false
    end
  | Node_nat t11 t12 =>
    match t2 with
      Leaf_nat n2 =>
      false
    | Node_nat t21 t22 =>
      (eqb_binary_tree_nat t11 t21) && (eqb_binary_tree_nat t12 t22)
    end
  end.

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

(* How many leaves are there in a given binary tree? *)

(* Unit tests: *)

Definition test_number_of_leaves (candidate: binary_tree_nat -> nat) : bool :=
  true
    &&
    (Nat.eqb
       (candidate
          (Leaf_nat 1))
       1)
    &&
    (Nat.eqb
       (candidate
          (Node_nat
             (Leaf_nat 1)
             (Leaf_nat 2)))
       2)
(* etc. *)
.

(* ***** *)

(* Version 1: recursive *)

Fixpoint number_of_leaves_v1 (t : binary_tree_nat) : nat :=
  match t with
    Leaf_nat n =>
    1
  | Node_nat t1 t2 =>
    (number_of_leaves_v1 t1) + (number_of_leaves_v1 t2)
  end.

(* ***** *)

Compute (test_number_of_leaves number_of_leaves_v1).

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

(* How many nodes in a given binary tree? *)

(* Unit tests: *)

Definition test_number_of_nodes (candidate: binary_tree_nat -> nat) : bool :=
  true
(* etc. *)
.

(* ***** *)

(* Version 1: recursive *)

(*
Fixpoint number_of_nodes_v1 (t : binary_tree_nat) : nat :=
  ...

Compute (test_number_of_nodes number_of_nodes_v1).
*)

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

(* What is the smallest leaf in a given binary tree? *)

Compute (Nat.ltb 1 2).
Compute (Nat.leb 1 2).

Definition test_smallest_leaf (candidate: binary_tree_nat -> nat) : bool :=
  true
(* etc. *)
.

(*
Fixpoint smallest_leaf_v1 (t : binary_tree_nat) : nat :=
  ...

Compute (test_smallest_leaf smallest_leaf_v1).
*)

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

(* What is the sum of the payloads in the leaves of a given binary tree? *)

(* Unit tests: *)

Definition test_weight (candidate: binary_tree_nat -> nat) : bool :=
  true
(* etc. *)
.

(* ***** *)

(* Version 1: recursive *)

Fixpoint weight_v1 (t : binary_tree_nat) : nat :=
  match t with
    Leaf_nat n =>
    n
  | Node_nat t1 t2 =>
    weight_v1 t1 + weight_v1 t2
  end.

Compute (test_weight weight_v1).

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

(* What is the length of the longest path from the root of a given binary tree to its leaves? *)

(* ***** *)

Definition test_length_of_longest_path (candidate: binary_tree_nat -> nat) : bool :=
  true
(* etc. *)
.

(* ***** *)

(* Version 1: recursive *)

(*
Fixpoint length_of_longest_path_v1 (t : binary_tree_nat) : nat :=
  ...

Compute (test_length_of_longest_path length_of_longest_path_v1).
*)

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

(* What is the length of the shortest path from the root of a given binary tree to its leaves? *)

(* ***** *)

Definition test_length_of_shortest_path (candidate: binary_tree_nat -> nat) : bool :=
  true
(* etc. *)
.

(* ***** *)

(* Version 1: recursive *)

(*
Fixpoint length_of_shortest_path_v1 (t : binary_tree_nat) : nat :=
  ...

Compute (test_length_of_shortest_path length_of_shortest_path_v1).
*)

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

(* The mirror function: *)

(* Unit tests: *)

Definition test_mirror (candidate: binary_tree_nat -> binary_tree_nat) : bool :=
  true
    &&
    (eqb_binary_tree_nat
       (candidate
          (Leaf_nat 1))
       (Leaf_nat 1))
    &&
    (eqb_binary_tree_nat
       (candidate
          (Node_nat
             (Leaf_nat 1)
             (Leaf_nat 2)))
       (Node_nat
          (Leaf_nat 2)
          (Leaf_nat 1)))
(* etc. *)
.

(* ***** *)

(* Version 1: recursive *)

(*
Fixpoint mirror_v1 (t : binary_tree_nat) : binary_tree_nat :=
  ...

Compute (test_mirror mirror_v1).
*)

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

(* Calder mobiles: *)

(*
   base case:
   a leaf is well balanced

   induction step:
   given a first tree t1 that is well balanced
   and a second tree t2 that is well balanced,
   the tree
     Node t1 t2
   is well balanced if t1 and t2 have the same weight
*)

(* ***** *)

(* Unit tests: *)

(*
...
*)

(* ***** *)

(* Version 1: recursive *)

(*
...
*)

(* challenge: traverse the given tree only once, at most *)

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

(* end of week-01_functional-programming-in-Gallina.v *)