没有合适的资源?快使用搜索试试~ 我知道了~
coq induction练习(1~2星)答案
需积分: 10 14 下载量 71 浏览量
2014-04-03
17:30:53
上传
评论
收藏 7KB TXT 举报
温馨提示
试读
10页
形式化方法coq induction练习(1~2星)答案
资源推荐
资源详情
资源评论
Require Export Basics.
Require String. Open Scope string_scope.
(** **** Exercise: 2 stars (andb_true_elim2) *)
Ltac move_to_top x :=
match reverse goal with
| H : _ |- _ => try move x after H
end.
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move_to_top x
| assert_eq x name; move_to_top x
| fail 1 "because we are working on a different case" ].
Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.
(** **** Exercise: 2 stars (andb_true_elim2) *)
Require String. Open Scope string_scope.
(** **** Exercise: 2 stars (andb_true_elim2) *)
Ltac move_to_top x :=
match reverse goal with
| H : _ |- _ => try move x after H
end.
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move_to_top x
| assert_eq x name; move_to_top x
| fail 1 "because we are working on a different case" ].
Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.
(** **** Exercise: 2 stars (andb_true_elim2) *)
(** Prove [andb_true_elim2], marking cases (and subcases) when
you use [destruct]. *)
Theorem andb_true_elim2 : forall b c : bool,
andb b c = true -> c = true.
Proof.
intros b c H.
destruct c.
Case "c = true".
reflexivity.
Case "c = false".
rewrite <- H.
rewrite andb_false.
reflexivity.
Qed.
(** [] *)
(* ###################################################################### *)
(** * Proof by Induction *)
(** **** Exercise: 2 stars (basic_induction) *)
(** Prove the following lemmas using induction. You might need
previously proven results. *)
Theorem mult_0_r : forall n:nat,
n * 0 = 0.
Proof.
intros. induction n.
simpl.
you use [destruct]. *)
Theorem andb_true_elim2 : forall b c : bool,
andb b c = true -> c = true.
Proof.
intros b c H.
destruct c.
Case "c = true".
reflexivity.
Case "c = false".
rewrite <- H.
rewrite andb_false.
reflexivity.
Qed.
(** [] *)
(* ###################################################################### *)
(** * Proof by Induction *)
(** **** Exercise: 2 stars (basic_induction) *)
(** Prove the following lemmas using induction. You might need
previously proven results. *)
Theorem mult_0_r : forall n:nat,
n * 0 = 0.
Proof.
intros. induction n.
simpl.
剩余9页未读,继续阅读
资源评论
stephanieleong912
- 粉丝: 11
- 资源: 2
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功