| 1 |
Inductive bool : Type :=
|
| 2 |
| true : bool
|
| 3 |
| false : bool.
|
| 4 |
|
| 5 |
(* exercise nandb *)
|
| 6 |
|
| 7 |
Definition nandb (b1 : bool) (b2 : bool) : bool :=
|
| 8 |
match b1 with
|
| 9 |
| true => match b2 with
|
| 10 |
| true => false
|
| 11 |
| false => true
|
| 12 |
end
|
| 13 |
| false => true
|
| 14 |
end.
|
| 15 |
|
| 16 |
Example test_nandb1: (nandb true false) = true.
|
| 17 |
Proof. simpl. reflexivity. Qed.
|
| 18 |
Example test_nandb2: (nandb false false) = true.
|
| 19 |
Proof. simpl. reflexivity. Qed.
|
| 20 |
Example test_nandb3: (nandb false true) = true.
|
| 21 |
Proof. simpl. reflexivity. Qed.
|
| 22 |
Example test_nandb4: (nandb true true) = false.
|
| 23 |
Proof. simpl. reflexivity. Qed.
|
| 24 |
|
| 25 |
(* exercise andb3 *)
|
| 26 |
|
| 27 |
Definition andb3 (b1: bool) (b2: bool) (b3: bool) : bool :=
|
| 28 |
match (b1, b2, b3) with
|
| 29 |
| (true, true, true) => true
|
| 30 |
| _ => false
|
| 31 |
end.
|
| 32 |
|
| 33 |
Example test_andb31: (andb3 true true true) = true.
|
| 34 |
Proof. simpl. reflexivity. Qed.
|
| 35 |
Example test_andb32: (andb3 false true true) = false.
|
| 36 |
Proof. simpl. reflexivity. Qed.
|
| 37 |
Example test_andb33: (andb3 true false true) = false.
|
| 38 |
Proof. simpl. reflexivity. Qed.
|
| 39 |
Example test_andb34: (andb3 true true false) = false.
|
| 40 |
Proof. simpl. reflexivity. Qed.
|
| 41 |
|
| 42 |
(* exercise factorial *)
|
| 43 |
|
| 44 |
Fixpoint factorial (n: nat) : nat :=
|
| 45 |
match n with
|
| 46 |
| 0 => 1
|
| 47 |
| S n => S n * factorial n
|
| 48 |
end.
|
| 49 |
|
| 50 |
Example test_factorial1: (factorial 3) = 6.
|
| 51 |
Proof. simpl. reflexivity. Qed.
|
| 52 |
|
| 53 |
Example test_factorial2: (factorial 5) = (mult 10 12).
|
| 54 |
Proof. simpl. reflexivity. Qed.
|
| 55 |
|
| 56 |
(* exercise blt_nat *)
|
| 57 |
|
| 58 |
Definition blt_nat (n m : nat) : bool. Admitted.⏎
|