yadunut/nus
1
0
Fork 0
Code Issues Pull Requests Actions Projects Releases Wiki Activity

feat: 3234 WIP

Browse Source
This commit is contained in:
Yadunand Prem 2024-01-24 09:23:50 +08:00
parent 3544a28a2e
commit 6bdba703a6
No known key found for this signature in database
2 changed files with 420 additions and 151 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

518
cs3234/labs/week-01_functional-programming-in-Gallina.v
View File

@ -10,42 +10,42 @@
(* name: (* name:
e-mail address: e-mail address:
student number: student number:
*) *)
(* name: (* name:
e-mail address: e-mail address:
student number: student number:
*) *)
(* name: (* name:
e-mail address: e-mail address:
student number: student number:
*) *)
(* name: (* name:
e-mail address: e-mail address:
student number: student number:
*) *)
(* name: (* name:
e-mail address: e-mail address:
student number: student number:
*) *)
(* name: (* name:
e-mail address: e-mail address:
student number: student number:
*) *)
(* name: (* name:
e-mail address: e-mail address:
student number: student number:
*) *)
(* name: (* name:
e-mail address: e-mail address:
student number: student number:
*) *)
(* ********** *) (* ********** *)
@ -125,7 +125,7 @@ Compute (fun m : nat => S m).
in OCaml and in OCaml and
(lambda (m) (1+ m)) (lambda (m) (1+ m))
in Scheme. in Scheme.
*) *)
Compute ((fun m : nat => S m) 3). Compute ((fun m : nat => S m) 3).
@ -147,20 +147,26 @@ Compute ten.
(* The following definitions are all equivalent: *) (* The following definitions are all equivalent: *)
(* This adds type definitions to the definition*)
Definition succ_v0 : nat -> nat := Definition succ_v0 : nat -> nat :=
fun m : nat => S m. fun m : nat => S m.
(* Without Type definitions *)
Definition succ_v1 := Definition succ_v1 :=
fun m => S m. fun m => S m.
(* defines the variable m as part of params *)
Definition succ_v2 (m : nat) := Definition succ_v2 (m : nat) :=
S m. S m.
(* defines the variable m as part of params and specifies return type *)
Definition succ_v3 (m : nat) : nat := Definition succ_v3 (m : nat) : nat :=
S m. S m.
(* infers the input tpye and return type from function S *)
Definition succ_v4 m := Definition succ_v4 m :=
S m. S m.
Check S.
(* Note: the definition of succ_v3 is the recommended one here. *) (* Note: the definition of succ_v3 is the recommended one here. *)
@ -219,9 +225,9 @@ Definition test_add (candidate: nat -> nat -> nat) : bool :=
&& &&
(* associativity: *) (* associativity: *)
(Nat.eqb (candidate 2 (candidate 5 10)) (Nat.eqb (candidate 2 (candidate 5 10))
(candidate (candidate 2 5) 10)) (candidate (candidate 2 5) 10))
(* etc. *) (* etc. *)
. .
(* Testing the unit-test function: *) (* 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 * induction step: given a number i' such that multiplying it and j yields ih
(which is the induction hypothesis), (which is the induction hypothesis),
multiplying S i' and j should yield j + ih. multiplying S i' and j should yield j + ih.
*) *)
(* ***** *) (* ***** *)
(* Unit tests: *) (* Unit tests: *)
(*
Definition test_mult (candidate: nat -> nat -> nat) : bool := Definition test_mult (candidate: nat -> nat -> nat) : bool :=
... (Nat.eqb (candidate 0 0) 0)
(* etc. *) &&
. (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: *) (* Testing the unit-test function: *)
(*
Compute (test_mult mult). Compute (test_mult mult).
*)
(* ***** *) (* ***** *)
(* Version 1: lambda-dropped *) (* 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). Compute (test_mult mult_v1).
*)
(* ***** *) (* ***** *)
(* Version 2: lambda-lifted *) (* Version 2: lambda-lifted *)
Fixpoint mult_v2 (i j : nat) : nat := Fixpoint mult_v2 (i j : nat) : nat :=
match i with match i with
| 0 => 0 | 0 => 0
| (S i') => j + mult_v2 i' j | (S i') => j + mult_v2 i' j
end. end.
(* Compute (test_mult mult_v2). *) Compute (test_mult mult_v2).
Compute (mult_v2 2 6). Compute (mult_v2 2 6).
(* ***** *) (* ***** *)
@ -335,21 +365,22 @@ Definition mult_v3 (n j : nat) : nat :=
end end
in visit n 0. in visit n 0.
Compute (mult_v3 2 6). 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 *) (* Version 4: lambda-lifted and tail recursive with an accumulator *)
(*
Fixpoint mult_v4_aux (i j a : nat) : nat := 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 := Definition mult_v4 (n j : nat) : nat :=
... mult_v4_aux n j 0.
Compute (test_mult mult_v4). 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 * induction step: given a number i' such that exponentiating x with i' it and j yields ih
(which is the induction hypothesis), (which is the induction hypothesis),
exponentiating x with S i' should yield x * ih. exponentiating x with S i' should yield x * ih.
*) *)
(* Unit tests: *) (* 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 *) (* Version 1: lambda-dropped *)
(*
Definition power_v1 (x n : nat) : nat := 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). Compute (test_power power_v1).
*)
(* ***** *) (* ***** *)
(* Version 2: lambda-lifted *) (* Version 2: lambda-lifted *)
(*
Fixpoint power_v2 (x n : nat) : nat := 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). Compute (test_power power_v2).
*)
(* ***** *) (* ***** *)
(* Version 3: lambda-dropped and tail recursive with an accumulator *) (* 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 *) (* Version 4: lambda-lifted and tail recursive with an accumulator *)
(*
Fixpoint power_v4_aux (x i a : nat) : nat := 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 := Definition power_v4 (x n : nat) : nat :=
... power_v4_aux x n 1.
Compute power_v4 2 5.
Compute (test_power power_v4). Compute (test_power power_v4).
*)
(* ********** *) (* ********** *)
(* The factorial function: *) (* 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 * induction step: given a number i' such that the factorial of i' is ih
(which is the induction hypothesis), (which is the induction hypothesis),
the factorial of S i' is (S i') * ih. the factorial of S i' is (S i') * ih.
*) *)
(* Unit tests: *) (* Unit tests: *)
(*
Definition test_fac (candidate: nat -> nat) : bool := Definition test_fac (candidate: nat -> nat) : bool :=
... (Nat.eqb (candidate 0) 1)
(* etc. *) &&
. (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 *) (* Version 1: recursive *)
(*
Fixpoint fac_v1 (n : nat) : nat := Fixpoint fac_v1 (n : nat) : nat :=
... match n with
| 0 => 1
| S n' => n * fac_v1 n'
end.
Compute (test_fac fac_v1). Compute (test_fac fac_v1).
*)
(* ***** *) (* ***** *)
(* Version 2: tail recursive with an accumulator *) (* Version 2: tail recursive with an accumulator *)
(* Fixpoint fac_v2_aux (n a : nat) : nat :=
Fixpoint fac_v2 (n a : nat) : nat := match n with
... | 0 => a
| S n' => fac_v2_aux n' a * n
end.
Definition fac_v2 (n : nat) : nat := Definition fac_v2 (n : nat) : nat :=
... fac_v2_aux n 1.
Compute (test_fac fac_v2). Compute (test_fac fac_v2).
*)
(* ********** *) (* ********** *)
(* The fibonacci function: *) (* 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 * base case #2: the fibonacci number at index 1 is 1
@ -481,31 +550,49 @@ Compute (test_fac fac_v2).
and and
the fibonacci number at index S i' is fib_Si' (which is the first induction hypothesis), 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' the fibonacci number at index S (S i') is fib_i' + fib_Si'
*) *)
(* ***** *) (* ***** *)
(* Unit tests: *) (* Unit tests: *)
(*
Definition test_fib (candidate: nat -> nat) : bool := Definition test_fib (candidate: nat -> nat) : bool :=
... (Nat.eqb (candidate 0) 0)
(* etc. *) &&
. (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 *) (* Version 1: recursive *)
(*
Fixpoint fib_v1 (n : nat) : nat := 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 *) (* hint: make sure to read the interludes in the exercise chapter *)
Compute (test_fib fib_v1). Compute (test_fib fib_v1).
*)
(* ********** *) (* ********** *)
@ -531,39 +618,65 @@ Definition bool_eqb (b1 b2 : bool) : bool :=
(* Unit tests: *) (* Unit tests: *)
(*
Definition test_evenp (candidate: nat -> bool) : bool := Definition test_evenp (candidate: nat -> bool) : bool :=
... (bool_eqb true (candidate 0))
(* etc. *) &&
. (bool_eqb false (candidate 1))
*) &&
(bool_eqb true (candidate 2))
&&
(bool_eqb false (candidate 3))
.
(* ***** *) (* ***** *)
(* Version 1: recursive *) (* Version 1: recursive *)
(* Fixpoint evenp_v1 (n : nat) : bool :=
Fixpoint even_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 *) (* 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: *) (* 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 := Definition test_number_of_leaves (candidate: binary_tree_nat -> nat) : bool :=
(Nat.eqb (candidate (Leaf_nat 1)) (Nat.eqb (candidate (Leaf_nat 1))
1) 1)
&& &&
(Nat.eqb (candidate (Node_nat (Leaf_nat 1) (Nat.eqb (candidate (Node_nat (Leaf_nat 1)
(Leaf_nat 2))) (Leaf_nat 2)))
2) 2)
(* etc. *) (* etc. *)
. .
(* ***** *) (* ***** *)
@ -623,33 +736,43 @@ Compute (test_number_of_leaves number_of_leaves_v1).
(* Version 2: recursive with an accumulator *) (* 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? *) (* How many nodes in a given binary tree? *)
(* Unit tests: *) (* Unit tests: *)
(*
Definition test_number_of_nodes (candidate: binary_tree_nat -> nat) : bool := Definition test_number_of_nodes (candidate: binary_tree_nat -> nat) : bool :=
... (Nat.eqb (candidate (Leaf_nat 1))
(* etc. *) 1)
. &&
*) (Nat.eqb (candidate (Node_nat (Leaf_nat 1)
(Leaf_nat 2)))
3)
.
(* ***** *) (* ***** *)
(* Version 1: recursive *) (* Version 1: recursive *)
(*
Fixpoint number_of_nodes_v1 (t : binary_tree_nat) : nat := 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). 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.ltb 1 2).
Compute (Nat.leb 1 2). Compute (Nat.leb 1 2).
(* Check Nat.ltb.
Definition test_smallest_leaf (candidate: binary_tree_nat -> nat) : bool := Definition test_smallest_leaf (candidate: binary_tree_nat -> nat) : bool :=
... (Nat.eqb (candidate (Leaf_nat 1))
(* etc. *) 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 := 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). Compute (test_smallest_leaf smallest_leaf_v1).
*)
(* ********** *) (* ********** *)
@ -676,12 +828,21 @@ Compute (test_smallest_leaf smallest_leaf_v1).
(* Unit tests: *) (* Unit tests: *)
(*
Definition test_weight (candidate: binary_tree_nat -> nat) : bool := Definition test_weight (candidate: binary_tree_nat -> nat) : bool :=
... (Nat.eqb (candidate (Leaf_nat 1))
(* etc. *) 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 match t with
| Leaf_nat n => | Leaf_nat n =>
n n
| Node_nat t1 t2 => | Node_nat l r =>
weight_v1 t1 + weight_v1 t2 weight_v1 l + weight_v1 r
end. end.
(*
Compute (test_weight weight_v1). Compute (test_weight weight_v1).
*)
(* ***** *) (* ***** *)
(* Version 2: recursive with an accumulator *) (* 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 := Definition test_length_of_longest_path (candidate: binary_tree_nat -> nat) : bool :=
... (Nat.eqb (candidate (Leaf_nat 1))
(* etc. *) 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 *) (* Version 1: recursive *)
(*
Fixpoint length_of_longest_path_v1 (t : binary_tree_nat) : nat := 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). 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 := Definition test_length_of_shortest_path (candidate: binary_tree_nat -> nat) : bool :=
... (Nat.eqb (candidate (Leaf_nat 1))
(* etc. *) 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 *) (* 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 := 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). 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 := Definition test_mirror (candidate: binary_tree_nat -> binary_tree_nat) : bool :=
(beq_binary_tree_nat (candidate (Leaf_nat 1)) (beq_binary_tree_nat (candidate (Leaf_nat 1))
(Leaf_nat 1)) (Leaf_nat 1))
&& &&
(beq_binary_tree_nat (candidate (Node_nat (Leaf_nat 1) (beq_binary_tree_nat (candidate (Node_nat (Leaf_nat 1)
(Leaf_nat 2))) (Leaf_nat 2)))
(Node_nat (Leaf_nat 2) (Node_nat (Leaf_nat 2)
(Leaf_nat 1))) (Leaf_nat 1)))
(* etc. *) (* etc. *)
. .
(* ***** *) (* ***** *)
(* Version 1: recursive *) (* Version 1: recursive *)
(*
Fixpoint mirror_v1 (t : binary_tree_nat) : binary_tree_nat := 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). Compute (test_mirror mirror_v1).
*)
(* ********** *) (* ********** *)
@ -797,7 +1002,7 @@ Compute (test_mirror mirror_v1).
the tree the tree
Node t1 t2 Node t1 t2
is well balanced if t1 and t2 have the same weight is well balanced if t1 and t2 have the same weight
*) *)
(* ***** *) (* ***** *)
@ -805,15 +1010,26 @@ Compute (test_mirror mirror_v1).
(* (*
... ...
*) *)
(* ***** *) (* ***** *)
(* Version 1: recursive *) (* 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 *) (* challenge: traverse the given tree only once, at most *)

53
cs3234/labs/week-01_getting-started.v Normal file
View File

@ -0,0 +1,53 @@
(* week-01_getting-started.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* 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 <? 3).
Check Nat.ltb.
Compute (2 <=? 2).
Check Nat.leb.
(* ********** *)
Require Import Bool.
(* The Bool library offers true, false, comparison, negation, conjunction, and disjunction: *)
Compute true.
Compute false.
Check Bool.eqb.
Check negb.
Compute (negb true).
Check (true && true).
Check (true && false).
Check (false || true).
Check (false || false).
(* ********** *)
(* end of week-01_getting-started.v *)