From 6bdba703a69042961619c5a9b5b7cf1a4e5dc81e Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Wed, 24 Jan 2024 09:23:50 +0800 Subject: [PATCH] feat: 3234 WIP --- ...eek-01_functional-programming-in-Gallina.v | 518 +++++++++++++----- cs3234/labs/week-01_getting-started.v | 53 ++ 2 files changed, 420 insertions(+), 151 deletions(-) create mode 100644 cs3234/labs/week-01_getting-started.v diff --git a/cs3234/labs/week-01_functional-programming-in-Gallina.v b/cs3234/labs/week-01_functional-programming-in-Gallina.v index 8b31c06..2cd78fa 100644 --- a/cs3234/labs/week-01_functional-programming-in-Gallina.v +++ b/cs3234/labs/week-01_functional-programming-in-Gallina.v @@ -10,42 +10,42 @@ (* 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: -*) + *) (* ********** *) @@ -125,7 +125,7 @@ Compute (fun m : nat => S m). in OCaml and (lambda (m) (1+ m)) in Scheme. -*) + *) Compute ((fun m : nat => S m) 3). @@ -147,20 +147,26 @@ Compute ten. (* The following definitions are all equivalent: *) +(* This adds type definitions to the definition*) Definition succ_v0 : nat -> nat := fun m : nat => S m. +(* Without Type definitions *) Definition succ_v1 := fun m => S m. +(* defines the variable m as part of params *) Definition succ_v2 (m : nat) := S m. +(* defines the variable m as part of params and specifies return type *) Definition succ_v3 (m : nat) : nat := S m. +(* infers the input tpye and return type from function S *) Definition succ_v4 m := S m. +Check S. (* Note: the definition of succ_v3 is the recommended one here. *) @@ -219,9 +225,9 @@ Definition test_add (candidate: nat -> nat -> nat) : bool := && (* associativity: *) (Nat.eqb (candidate 2 (candidate 5 10)) - (candidate (candidate 2 5) 10)) - (* etc. *) - . + (candidate (candidate 2 5) 10)) +(* etc. *) +. (* Testing the unit-test function: *) @@ -277,50 +283,74 @@ Compute (test_add add_v3). * 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 := - ... - (* etc. *) - . -*) + (Nat.eqb (candidate 0 0) 0) + && + (Nat.eqb (candidate 0 1) 0) + && + (Nat.eqb (candidate 1 0) 0) + && + (Nat.eqb (candidate 2 1) 2) + && + (Nat.eqb (candidate 2 2) 4) + && + (Nat.eqb (candidate 4 3) (4+4+4)) + && + (let x := 5 in + let y := 6 in + (Nat.eqb (candidate x y) (candidate y x))) + && + (let x := 5 in + let y := 6 in + let z := 7 in + (Nat.eqb (candidate x (candidate y z)) (candidate z (candidate x y)))) + && + ( + (* Testing the inductive step *) + let j := 10 in + let i := 3 in + Nat.eqb (candidate (S i) j) (j + candidate i j)) +. (* ***** *) (* Testing the unit-test function: *) -(* + Compute (test_mult mult). -*) (* ***** *) (* Version 1: lambda-dropped *) -(* -Fixpoint mult_v1 (n j : nat) : nat := - ... + +Definition mult_v1 (n j : nat) : nat := + let fix visit i := + match i with + | 0 => 0 + | S i' => j + (visit i') + end + in visit n. Compute (test_mult mult_v1). -*) (* ***** *) (* Version 2: lambda-lifted *) - Fixpoint mult_v2 (i j : nat) : nat := match i with | 0 => 0 | (S i') => j + mult_v2 i' j end. -(* Compute (test_mult mult_v2). *) +Compute (test_mult mult_v2). Compute (mult_v2 2 6). (* ***** *) @@ -335,21 +365,22 @@ Definition mult_v3 (n j : nat) : nat := end in visit n 0. Compute (mult_v3 2 6). -(* Compute (test_mult mult_v3). *) +Compute (test_mult mult_v3). (* ***** *) (* Version 4: lambda-lifted and tail recursive with an accumulator *) -(* Fixpoint mult_v4_aux (i j a : nat) : nat := - ... + match i with + | 0 => a + | S i' => mult_v4_aux i' j (a+j) + end. Definition mult_v4 (n j : nat) : nat := - ... + mult_v4_aux n j 0. Compute (test_mult mult_v4). -*) (* ********** *) @@ -363,116 +394,154 @@ Compute (test_mult mult_v4). * 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 := - ... - (* etc. *) - . -*) +Definition test_power (candidate: nat -> nat -> nat) : bool := + (Nat.eqb (candidate 0 0) 1) + && + (Nat.eqb (candidate 0 1) 0) + && + (Nat.eqb (candidate 1 0) 1) + && + (Nat.eqb (candidate 1 1) 1) + && + (Nat.eqb (candidate 1 2) 1) + && + (Nat.eqb (candidate 2 1) 2) + && + (Nat.eqb (candidate 2 3) 8) + && + (Nat.eqb (candidate 3 4) 81) + && + (Nat.eqb (candidate 3 4) (3*3*3*3)). (* ***** *) (* Version 1: lambda-dropped *) -(* + Definition power_v1 (x n : nat) : nat := - ... + let fix visit i := + match i with + | 0 => 1 + | S i' => x * visit i' + end + in visit n. Compute (test_power power_v1). -*) (* ***** *) (* Version 2: lambda-lifted *) -(* + Fixpoint power_v2 (x n : nat) : nat := - ... + match n with + | 0 => 1 + | S n' => x * power_v2 x n' + end. Compute (test_power power_v2). -*) (* ***** *) (* Version 3: lambda-dropped and tail recursive with an accumulator *) -(* -Definition power_v3 (x n : nat) : nat := - ... -Compute (test_power power_v2). -*) +Definition power_v3 (x n : nat) : nat := + let fix visit i a := + match i with + | O => 1 + | S i' => visit i' a * x + end + in visit n 1. + +Compute (test_power power_v3). (* ***** *) (* Version 4: lambda-lifted and tail recursive with an accumulator *) -(* Fixpoint power_v4_aux (x i a : nat) : nat := - ... + match i with + | O => a + | S i' => power_v4_aux x i' x * a + end. Definition power_v4 (x n : nat) : nat := - ... + power_v4_aux x n 1. + +Compute power_v4 2 5. Compute (test_power power_v4). -*) (* ********** *) (* The factorial function: *) (* - * base case: the factorial of 0 is 1; + * 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 := - ... - (* etc. *) - . -*) + (Nat.eqb (candidate 0) 1) + && + (Nat.eqb (candidate 1) 1) + && + (Nat.eqb (candidate 2) 2) + && + (Nat.eqb (candidate 3) 6) + && + (Nat.eqb (candidate 4) 24) + && + (Nat.eqb (candidate 5) 120) + && + (Nat.eqb (candidate 6) 720) + && + (Nat.eqb (candidate 7) 5040) + && + (Nat.eqb (candidate 8) 40320). (* ***** *) (* Version 1: recursive *) -(* Fixpoint fac_v1 (n : nat) : nat := - ... + match n with + | 0 => 1 + | S n' => n * fac_v1 n' + end. Compute (test_fac fac_v1). -*) (* ***** *) (* Version 2: tail recursive with an accumulator *) -(* -Fixpoint fac_v2 (n a : nat) : nat := - ... - +Fixpoint fac_v2_aux (n a : nat) : nat := + match n with + | 0 => a + | S n' => fac_v2_aux n' a * n + end. Definition fac_v2 (n : nat) : nat := - ... + fac_v2_aux n 1. Compute (test_fac fac_v2). -*) (* ********** *) (* The fibonacci function: *) (* - * base case #1: the fibonacci number at index 0 is 0 + * base case #1: the fibonacci number at index 0 is 0 * base case #2: the fibonacci number at index 1 is 1 @@ -481,31 +550,49 @@ Compute (test_fac fac_v2). 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 := - ... - (* etc. *) - . -*) + (Nat.eqb (candidate 0) 0) + && + (Nat.eqb (candidate 1) 1) + && + (Nat.eqb (candidate 2) 1) + && + (Nat.eqb (candidate 3) 2) + && + (Nat.eqb (candidate 4) 3) + && + (Nat.eqb (candidate 5) 5) + && + (Nat.eqb (candidate 6) 8) + && + (Nat.eqb (candidate 7) 13) + && + (Nat.eqb (candidate 8) 21) +. (* ***** *) (* Version 1: recursive *) -(* Fixpoint fib_v1 (n : nat) : nat := - ... + match n with + | 0 => 0 + | S n' => match n' with + | 0 => 1 + | S n'' => fib_v1 n' + fib_v1 n'' + end + end. (* hint: make sure to read the interludes in the exercise chapter *) Compute (test_fib fib_v1). -*) (* ********** *) @@ -531,39 +618,65 @@ Definition bool_eqb (b1 b2 : bool) : bool := (* Unit tests: *) -(* + Definition test_evenp (candidate: nat -> bool) : bool := - ... - (* etc. *) - . -*) + (bool_eqb true (candidate 0)) + && + (bool_eqb false (candidate 1)) + && + (bool_eqb true (candidate 2)) + && + (bool_eqb false (candidate 3)) +. (* ***** *) (* Version 1: recursive *) -(* -Fixpoint even_v1 (n : nat) : bool := - ... +Fixpoint evenp_v1 (n : nat) : bool := + match n with + | 0 => true + | S n' => match n' with + | 0 => false + | S n'' => evenp_v1 n'' + end + end. -Compute (test_even even_v1). -*) +Compute (test_evenp evenp_v1). (* ***** *) (* Version 2: tail recursive with an accumulator *) +Fixpoint evenp_v2_aux (n : nat) (a : bool) : bool := + match n with + | 0 => a + | S n' => if a then evenp_v2_aux n' false else evenp_v2_aux n' true + end. + +Definition evenp_v2 (n : nat) : bool := + evenp_v2_aux n true. + +Compute (test_evenp evenp_v2). + (* ... -*) + *) (* ********** *) (* The odd predicate: *) +Definition oddp_v1 (n : nat) : bool := + if evenp_v2 n + then false + else true. + + + (* ... -*) + *) (* ********** *) @@ -597,13 +710,13 @@ Fixpoint beq_binary_tree_nat (t1 t2 : binary_tree_nat) : bool := Definition test_number_of_leaves (candidate: binary_tree_nat -> nat) : bool := (Nat.eqb (candidate (Leaf_nat 1)) - 1) + 1) && (Nat.eqb (candidate (Node_nat (Leaf_nat 1) - (Leaf_nat 2))) - 2) - (* etc. *) - . + (Leaf_nat 2))) + 2) +(* etc. *) +. (* ***** *) @@ -623,33 +736,43 @@ Compute (test_number_of_leaves number_of_leaves_v1). (* Version 2: recursive with an accumulator *) -(* -... -*) +Definition number_of_leaves_v2 (t: binary_tree_nat) : nat := + let fix visit (n : binary_tree_nat) (a : nat) : nat := + match n with + | Leaf_nat _ => S a + | Node_nat t1 t2 => visit t1 (visit t2 a) + end + in visit t 0. +Compute (test_number_of_leaves number_of_leaves_v2). (* ********** *) (* How many nodes in a given binary tree? *) (* Unit tests: *) -(* Definition test_number_of_nodes (candidate: binary_tree_nat -> nat) : bool := - ... - (* etc. *) - . -*) + (Nat.eqb (candidate (Leaf_nat 1)) + 1) + && + (Nat.eqb (candidate (Node_nat (Leaf_nat 1) + (Leaf_nat 2))) + 3) +. (* ***** *) (* Version 1: recursive *) -(* + Fixpoint number_of_nodes_v1 (t : binary_tree_nat) : nat := - ... + match t with + | Leaf_nat _ => 1 + | Node_nat l r => 1 + (number_of_nodes_v1 l) + (number_of_nodes_v1 r) + end. + Compute (test_number_of_nodes number_of_nodes_v1). -*) (* ********** *) @@ -658,17 +781,46 @@ Compute (test_number_of_nodes number_of_nodes_v1). Compute (Nat.ltb 1 2). Compute (Nat.leb 1 2). -(* +Check Nat.ltb. + Definition test_smallest_leaf (candidate: binary_tree_nat -> nat) : bool := - ... - (* etc. *) - . + (Nat.eqb (candidate (Leaf_nat 1)) + 1) + && + (Nat.eqb (candidate (Node_nat (Leaf_nat 1) + (Leaf_nat 2))) + 1) + && + (Nat.eqb (candidate (Node_nat (Node_nat (Leaf_nat 5) + (Leaf_nat 4)) + (Node_nat (Leaf_nat 3) + (Leaf_nat 2)))) + 2) +. + +(* + Given an Binary Tree t, + + * base case: If leaf node then the smallest value is value of leaf node; + + * 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. + *) Fixpoint smallest_leaf_v1 (t : binary_tree_nat) : nat := - ... + match t with + | Leaf_nat n => n + | Node_nat l r => + let l_v := (smallest_leaf_v1 l) in + let r_v := (smallest_leaf_v1 r) in + if Nat.ltb l_v r_v + then l_v + else r_v + end. + Compute (test_smallest_leaf smallest_leaf_v1). -*) (* ********** *) @@ -676,12 +828,21 @@ Compute (test_smallest_leaf smallest_leaf_v1). (* Unit tests: *) -(* + Definition test_weight (candidate: binary_tree_nat -> nat) : bool := - ... - (* etc. *) - . -*) + (Nat.eqb (candidate (Leaf_nat 1)) + 1) + && + (Nat.eqb (candidate (Node_nat (Leaf_nat 1) + (Leaf_nat 2))) + 3) + && + (Nat.eqb (candidate (Node_nat (Node_nat (Leaf_nat 5) + (Leaf_nat 4)) + (Node_nat (Leaf_nat 3) + (Leaf_nat 2)))) + 14) +. (* ***** *) @@ -691,21 +852,26 @@ 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 + | Node_nat l r => + weight_v1 l + weight_v1 r end. -(* + Compute (test_weight weight_v1). -*) (* ***** *) (* Version 2: recursive with an accumulator *) -(* -... -*) +Definition weight_v2 (t : binary_tree_nat) : nat := + let fix visit n a := + match n with + | Leaf_nat v => a + v + | Node_nat l r => visit l a + (visit r a) + end + in visit t 0. + +Compute (test_weight weight_v2). (* ********** *) @@ -713,23 +879,38 @@ Compute (test_weight weight_v1). (* ***** *) -(* + Definition test_length_of_longest_path (candidate: binary_tree_nat -> nat) : bool := - ... - (* etc. *) - . -*) + (Nat.eqb (candidate (Leaf_nat 1)) + 0) + && + (Nat.eqb (candidate (Node_nat (Leaf_nat 1) + (Leaf_nat 2))) + 1) + && + (Nat.eqb (candidate (Node_nat (Node_nat (Leaf_nat 5) + (Leaf_nat 4)) + (Leaf_nat 2))) + 2) +. (* ***** *) (* Version 1: recursive *) -(* + Fixpoint length_of_longest_path_v1 (t : binary_tree_nat) : nat := - ... + match t with + | Leaf_nat v => 0 + | Node_nat l r => + let l_v := length_of_longest_path_v1 l in + let r_v := length_of_longest_path_v1 r in + if Nat.ltb l_v r_v + then 1 + r_v + else 1 + l_v + end. Compute (test_length_of_longest_path length_of_longest_path_v1). -*) (* ********** *) @@ -737,23 +918,45 @@ Compute (test_length_of_longest_path length_of_longest_path_v1). (* ***** *) -(* + Definition test_length_of_shortest_path (candidate: binary_tree_nat -> nat) : bool := - ... - (* etc. *) + (Nat.eqb (candidate (Leaf_nat 1)) + 0) + && + (Nat.eqb (candidate (Node_nat (Leaf_nat 1) + (Leaf_nat 2))) + 1) + && + (Nat.eqb (candidate (Node_nat (Node_nat (Leaf_nat 5) + (Leaf_nat 4)) + (Leaf_nat 2))) + 1) + && + (Nat.eqb (candidate (Node_nat (Node_nat (Leaf_nat 5) + (Node_nat (Leaf_nat 1) (Leaf_nat 2))) + (Node_nat (Leaf_nat 5) + (Leaf_nat 4))) + ) 2) . -*) (* ***** *) (* Version 1: recursive *) -(* +(* Right now I'm DFS-ing through the tree, is it possible to BFS? *) + Fixpoint length_of_shortest_path_v1 (t : binary_tree_nat) : nat := - ... + match t with + | Leaf_nat v => 0 + | Node_nat l r => + let l_v := length_of_shortest_path_v1 l in + let r_v := length_of_shortest_path_v1 r in + if Nat.ltb l_v r_v + then 1 + l_v + else 1 + r_v + end. Compute (test_length_of_shortest_path length_of_shortest_path_v1). -*) (* ********** *) @@ -763,25 +966,27 @@ Compute (test_length_of_shortest_path length_of_shortest_path_v1). Definition test_mirror (candidate: binary_tree_nat -> binary_tree_nat) : bool := (beq_binary_tree_nat (candidate (Leaf_nat 1)) - (Leaf_nat 1)) + (Leaf_nat 1)) && (beq_binary_tree_nat (candidate (Node_nat (Leaf_nat 1) (Leaf_nat 2))) - (Node_nat (Leaf_nat 2) - (Leaf_nat 1))) - (* etc. *) - . + (Node_nat (Leaf_nat 2) + (Leaf_nat 1))) +(* etc. *) +. (* ***** *) (* Version 1: recursive *) -(* + Fixpoint mirror_v1 (t : binary_tree_nat) : binary_tree_nat := - ... + match t with + | Leaf_nat v => Leaf_nat v + | Node_nat l r => Node_nat (mirror_v1 r) (mirror_v1 l) + end. Compute (test_mirror mirror_v1). -*) (* ********** *) @@ -797,7 +1002,7 @@ Compute (test_mirror mirror_v1). the tree Node t1 t2 is well balanced if t1 and t2 have the same weight -*) + *) (* ***** *) @@ -805,15 +1010,26 @@ Compute (test_mirror mirror_v1). (* ... -*) + *) (* ***** *) (* Version 1: recursive *) +Fixpoint calder (t1 t2 : binary_tree_nat) : bool := + match t1 with + | Leaf_nat t1v => + match t2 with + | Leaf_nat t2v => t1v = t2v + | Node_nat t2l t2r => + | Node_nat t1l t1r => + match t2 with + | Leaf_nat t2v => + | Node_nat t2l t2r => + (* ... -*) + *) (* challenge: traverse the given tree only once, at most *) diff --git a/cs3234/labs/week-01_getting-started.v b/cs3234/labs/week-01_getting-started.v new file mode 100644 index 0000000..36d7c3b --- /dev/null +++ b/cs3234/labs/week-01_getting-started.v @@ -0,0 +1,53 @@ +(* week-01_getting-started.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 18 Jan 2024 *) + +(* ********** *) + +Require Import Arith. + +(* The Arith library offers addition, multiplication, and comparison predicates: *) + +Compute (1 + 2). +Compute (plus 1 2). +Check plus. + +Compute (2 * 3). +Compute (mult 2 3). +Check mult. + +Compute (2 =? 2). +Compute (2 =? 3). +Compute (Nat.eqb 2 3). +Check Nat.eqb. + +Compute (2