my first coq

形式化方法作业

写下第一题

一个好的开始

(** **** 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.