形式化方法作业
写下第一题
一个好的开始
(** **** Exercise: 1 star (nandb) *)
(** Complete the definition of the following function, then make
sure that the [Example] assertions below each can be verified by
Coq. *)
(** This function should return [true] if either or both of
its inputs are [false]. *)
Definition nandb (b1:bool) (b2:bool) : bool :=
(* FILL IN HERE *)
match b1 with
| true => (negb b2)
| false => true
end.
(** Remove "[Admitted.]" and fill in each proof with
"[Proof. simpl. reflexivity. Qed.]" *)
Example test_nandb1: (nandb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb2: (nandb false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb3: (nandb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb4: (nandb true true) = false.
Proof. simpl. reflexivity. Qed.