形式化方法—作业2—Coq的简单证明

一.背景

  课程主页: Formal Methods Foundation
  作业地址: Formal Methods Assignment2
  如果您的英文足够好,请直接点击上述链接查看相关信息
  由于课程结束上述链接失效, 请点击此处Wolai课程链接查看相关资料。

二.作业

 2.1 Coq基本说明

  Coq命题的基本结构如下:

  Theorem ident body: type.
  Proof.
     Tactics
  Qed.

  说明如下:

Theorem is a command in Coq, basically, it declares a new theorem which should be proved;
#Theorem指令代表提出一个新的待证明命题

ident is the name for the new theorem;
#ident是命题名称

body is the main body for the theorem;
#body是命题的内容

Proof starts the proving of the theorem. You need give the full poof after it;
#proof指令代表从此处开始证明

Qed command completes the proof;
#Qed指令代表证明完成,编译器提示No more subgoals.,代表证明结束

Tactics directs the process of proof, where we present deduction rules between the goal and premises. The tactics implement backward reasoning, 
when applied to a goal, a tactic replaces this goal with the sub-goals it generates. We say that a tactic reduces a goal to its sub-goal(s). 
For instance, to prove A /\ B, We have to prove A and B as sub-goals.
#Tactics代表证明过程中使用的策略,例如要证明 A /\ B,需要分别证明A和B,此时命题分别分裂成两个子命题,
分别证明A,B之后,原命题得证,这就是证明策略

 2.2 示例

  尝试证明 P -> P:
  代码如下:

Theorem example1: forall P:Prop,
    P -> P.
Proof.
    intros.
    apply H.
Qed.

  证明过程:
  1.产生命题: |- P -> P

  2.使用策略
  Γ, P |- Q
  --------------- (-> I)
  Γ |- P-> Q

  3.得出结论

  --------------- (Var)
  Γ, P |- P

  No more Subgoals代表证明完毕,可以使用Qed结束证明

 2.3 内容

  Exercise 1: Use intros and apply to prove the below theorem:

P -> (Q -> P)
Theorem exercise1: forall P Q:Prop,
    P -> (Q -> P).
Proof.
    intros.
    apply H.
Qed.

  Exercise 2: Use tactic apply .. in .., to prove:

(P->Q) -> (Q->H) -> (P->H)

  in的作用:如果有H1:P->Q,且H2:P is True,可以根据H2和H1联结推出Q is True ,语句为 apply H1 in H2

Theorem exercise2: forall P Q H: Prop,
    (P->Q) -> (Q->H) -> (P->H).
Proof.
    intros.
    apply H0,H1 in H2.
    apply H2.
Qed.

  Exercise 3:Use the inversion tactics to prove the following proposition:

P /\ (P -> Q) -> Q

  inversion的作用:如果有H1 :P/\Q,可以使用inversion关键词,将H1左右拆分,语句为 inversion H1

Theorem exercise3: forall P Q: Prop,
     P /\ (P -> Q) -> Q.
Proof.
    intros.
    inversion H.
    apply H1.
    apply H0 .
Qed.

  Exercise 4:With the new tactic split, try to prove:

(P /\ (Q /\ R)) -> ((P /\ Q) /\ R)

  split的作用:如果待证命题 :P/\Q,可以使用split关键词将目标分解为P,Q两个子命题,分别证明即可,语句为 split.
  策略如下:

   Γ |- P                Γ |- Q
  -------------------------------- (/\ I)
            Γ |- P /\ Q

  代码如下:

Theorem exercisee4: forall P Q R:Prop,
    (P /\ (Q /\ R)) -> ((P /\ Q) /\ R).
Proof.
    intros.
    inversion H.
    inversion H1.
    split.
    split.
    apply H0.
    apply H2.
    apply H3.
Qed.

  Exercise 5: Use tactic left and right to prove:

(P \/ (Q \/ R)) -> ((P \/ Q) \/ R)

  left的作用:如果存在H :P/\Q,可以使用left和right关键词将H为P,Q两个条件,如果P,Q中任意一个条件可以证明命题,则H也可以证明该命题
  策略如下:

 Γ |- P                          Γ |- Q
  ------------------- (\/ I1)    -------------------- (\/ I2)
       Γ |- P \/ Q                     Γ |- P \/ Q

  代码如下:

Theorem exercise5: forall P Q R:Prop,
  (P \/ (Q \/ R)) -> ((P \/ Q) \/ R).
Proof.
    intros.
    inversion H.
    left.
    left.
    apply H0.
    inversion H0.
    left.
    right.
    apply H1.
    right.
    apply H1.
Qed.

  Challenge: Try to prove the currying theorem:

(P /\ Q -> R) <-> (P -> Q -> R)
Theorem challenge1: forall P Q R:Prop,
  ((P -> R) /\ (Q -> R)) -> (P /\ Q -> R).
Proof.
    intros.
    inversion H.
    inversion H0.
    apply H1.
    apply H3.
Qed.

  Challenge: You may find that examples and exercises we've studied do not contain any not (aka. ~). Please read the Coq documents and try to prove below theorem:

(P -> Q) -> (~Q -> ~P)

  使用unfold "~"使得~p转变为p->false

Theorem challenge2: forall P Q:Prop,
  (P -> Q) -> (~Q -> ~P).
Proof.
    unfold "~".
    intros.
    apply H in H1.
    apply H0 in H1.
    apply H1.
Qed.

三.下载链接

  在线下载: 请点击这儿下载
  如果下载失败,点击此百度云链接:形式化方法作业二,提取码y825

end
  • 作者:Yuan(联系作者)
  • 发表时间:2021-11-30 13:21
  • 版权声明:自由转载-非商用-非衍生-保持署名(创意共享3.0许可证)
  • 转载声明:如果是转载博主转载的文章,请附上原文链接
  • 公众号转载:请联系作者
  • 评论