没有合适的资源?快使用搜索试试~ 我知道了~
coq basic练习(1~2星)答案
需积分: 10 14 下载量 168 浏览量
2014-04-03
17:29:51
上传
评论
收藏 6KB TXT 举报
温馨提示
试读
10页
形式化方法作业之coq basic练习(1~2星)答案
资源推荐
资源详情
资源评论
(** **** Exercise: 1 star (nandb) *)
(** Complete the definition of the following function, then make
sure that the [Example] assertions below can each 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 :=
match b1 with
| true => negb(b2)
| false => true
end.
(** Remove "[Admitted.]" and fill in each proof with
"[Proof. reflexivity. Qed.]" *)
Example test_nandb1: (nandb true false) = true.
Proof. reflexivity. Qed.
Example test_nandb2: (nandb false false) = true.
Proof. reflexivity. Qed.
Example test_nandb3: (nandb false true) = true.
Proof. reflexivity. Qed.
Example test_nandb4: (nandb true true) = false.
Proof. reflexivity. Qed.
(** [] *)
(** **** Exercise: 1 star (andb3) *)
(** Do the same for the [andb3] function below. This function should
return [true] when all of its inputs are [true], and [false]
(** Complete the definition of the following function, then make
sure that the [Example] assertions below can each 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 :=
match b1 with
| true => negb(b2)
| false => true
end.
(** Remove "[Admitted.]" and fill in each proof with
"[Proof. reflexivity. Qed.]" *)
Example test_nandb1: (nandb true false) = true.
Proof. reflexivity. Qed.
Example test_nandb2: (nandb false false) = true.
Proof. reflexivity. Qed.
Example test_nandb3: (nandb false true) = true.
Proof. reflexivity. Qed.
Example test_nandb4: (nandb true true) = false.
Proof. reflexivity. Qed.
(** [] *)
(** **** Exercise: 1 star (andb3) *)
(** Do the same for the [andb3] function below. This function should
return [true] when all of its inputs are [true], and [false]
otherwise. *)
Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
match b1 with
| true => (andb b2 b3)
| false => false
end.
Example test_andb31: (andb3 true true true) = true.
Proof. reflexivity. Qed.
Example test_andb32: (andb3 false true true) = false.
Proof. reflexivity. Qed.
Example test_andb33: (andb3 true false true) = false.
Proof. reflexivity. Qed.
Example test_andb34: (andb3 true true false) = false.
Proof. reflexivity. Qed.
(** [] *)
(* ###################################################################### *)
(** ** Numbers *)
(** **** Exercise: 1 star (factorial) *)
(** Recall the standard factorial function:
<<
factorial(0) = 1
factorial(n) = n * factorial(n-1) (if n>0)
>>
Translate this into Coq. *)
Fixpoint factorial (n:nat) : nat :=
Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
match b1 with
| true => (andb b2 b3)
| false => false
end.
Example test_andb31: (andb3 true true true) = true.
Proof. reflexivity. Qed.
Example test_andb32: (andb3 false true true) = false.
Proof. reflexivity. Qed.
Example test_andb33: (andb3 true false true) = false.
Proof. reflexivity. Qed.
Example test_andb34: (andb3 true true false) = false.
Proof. reflexivity. Qed.
(** [] *)
(* ###################################################################### *)
(** ** Numbers *)
(** **** Exercise: 1 star (factorial) *)
(** Recall the standard factorial function:
<<
factorial(0) = 1
factorial(n) = n * factorial(n-1) (if n>0)
>>
Translate this into Coq. *)
Fixpoint factorial (n:nat) : nat :=
剩余9页未读,继续阅读
资源评论
stephanieleong912
- 粉丝: 11
- 资源: 2
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功