形式化方法—作业4—Coq谓词逻辑证明

一.背景

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

二.作业

 2.1 策略的使用

  unfold策略:将~P展开为P->False

  assert策略:假设某个条件的真假,assert(f:False)即假设f为False,之后证明对应的子目标即可

  destruct策略:可以使用该策略将假设P/\Q破坏为两个假设P和Q,也可以使用此策略将假设P\/Q,分别证明在P和Q中成立即可

 2.2 谓词逻辑的引入

  在本节中,我们将学习如何使用Coq证明谓词逻辑定理。在Coq中,我们可以像声明命题变量一样声明集合变量:
  Variables A B: Set.
  在这里,我们将 A 和 B 声明为一个集合。接下来,我们在集合 A 上声明一些谓词变量 P 和 Q:
  Variables P Q: A -> Prop.
  您可以将 P 和 Q 视为从 A 获取元素并返回 Prop 的函数。如果我们有一个集合A中的元素,例如a:A,我们可以使用P(a)来表达元素a满足属性P,使用相同的方法,我们可以声明与几个元素相关的属性。例如,我们可以引入一个关系 R,通过以下方式将 A 和 B 联系起来:
  Variable R : A -> B -> Prop.
  这里R a b表示在函数R中a和b的关系。您可以将R视为具有两个参数的函数。

  本次实验主要用到的谓词逻辑包含存在∃和任意∀
  对于forall x: A, P x -> Q x意味着A中任意元素x如果满足属性P也将满足属性 Q
  示例如下:

  Theorem example4 :
        (forall x: A, P x -> Q x) -> (forall x: A, P x) -> forall x: A, Q x.
    Proof.
        intros H1 H2 a.
        apply H1.
        apply H2.
    Qed.

  说明如下:
  首先引入集合A中的一个变量a,作为前提条件

  我们可以应用H1将假设H1实例化为P a ->Q a,消除隐含的含义

  在最后一步中解决所有的forall。如果我们知道H : forall x: A, P,并且我们想要证明P(x),其中x被a替换,我们应当使用apply H2来证明P a

  对于exists x:A,P x来表示A有特定元素x具有属性P
  示例如下:

  Theorem example5 :
        (exists x: A, P x) -> (forall x: A, P x -> Q x) -> exists x: A, Q x.
    Proof.
        intros H1 H2.
        destruct H1 as [a p].
        exists a.
        apply H2.
        apply p.
    Qed.

  说明如下:
  为了证明存在exists x : A, Q x,我们可以假设满足的x的值是a,并将Q中的所有x替换为a 。在这个定理中,我们有假设H1:exists x:A,P x,它可以被分解为两个假设:a:A和P:a

  exists a将所有自由变量x替换为a>

  最后一步与上一个示例相同

 2.3 作业内容

  Exercise 1: 使用unfold策略,证明德摩根定律

~(P \/ Q) -> ~P /\ ~Q
Theorem exercise1 : forall P Q:Prop,
    ~(P \/ Q) -> ~P /\ ~Q.
Proof.
  unfold not.
  intros.
  split.
  intros.
  destruct H.
  left.
  apply H0.
  intros.
  destruct H.
  right.
  apply H0.
Qed.

  Exercise 2: 使用destruct策略证明以下命题

P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).
Theorem exercise2 : forall P Q R:Prop,
     P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).
Proof.
  intros.
  split.
  intros.
  inversion H.
  destruct H1 as [Hp|Hq].
  left.
  split.
  apply H0.
  apply Hp.
  right.
  split.
  apply H0.
  apply Hq.
  intros.
  inversion H.
  destruct H as [Hp|Hq].
  split.
  inversion H0.
  apply H.
  inversion H0.
  left.
  apply H1.
  inversion H0.
  split.
  apply H.
  inversion Hq.
  left.
  apply H1.
  inversion H0.
  split.
  apply H1.
  right.
  apply H2.
Qed.

  Exercise 3: 尝试证明以下包含任意的谓词逻辑表达式,注意需先声明集合变量,同一文件中只需申请一次

∀x.(~P(x) /\ Q(x)) -> ∀x.(P(x) -> Q(x))
Variables A: Set.
Variables P Q: A -> Prop.
Theorem exercise3:
  (forall x:A, ~(P x)/\(Q x))->(forall x: A,P x -> Q x).
Proof.
  intros H1 H2  a.
  apply H1.
Qed.

  Exercise 4: 尝试证明以下包含任意的谓词逻辑表达式

∀x.(P(x) -> Q(x)) -> ∀x.~Q(x) -> ∀x.~P(x)
(forall x: A, P x -> Q x) -> (forall x: A,~(Q x))-> forall x: A,~(P x).
Proof.
  unfold not.
  intros H1 H2 a.
  intros.
  apply H1 in H.
  apply H2 in H.
  apply H.
Qed.

  Exercise 5: 尝试证明以下包含任意的谓词逻辑表达式

∀x.(P(x) /\ Q(x)) <-> (∀x.P(x) /\ ∀x.Q(x))
Theorem exercise5:
    (forall x, (P x /\ Q x)) <-> ((forall x, P x) /\ (forall x, Q x)).
Proof.
    split.
    intros.
    split.
    apply H.
    apply H.
    intros H a.
    inversion H.
    split.
    apply H0.
    apply H1.
Qed.

  Exercise 6: 尝试证明以下包含存在的谓词逻辑表达式

∃x.(~P(x) \/ Q(x)) -> ∃x.(~(P(x) /\ ~Q(x)))
# ~优先级最高,即命题为∃x.(~(P(x) \/ Q(x))) -> ∃x.(~(P(x) /\ ~Q(x)))
Theorem exercise6:
  (exists x:A, ~((P x)\/(Q x)))->(exists x: A,(~(P x) /\~(Q x))).
Proof.
  unfold not.
  intros H.
  destruct H as [a p].
  exists a.
  split.
  intros.
  apply p.
  left.
  apply H.
  intros.
  apply p.
  right.
  apply H.
Qed.

  Exercise 7:尝试证明以下包含存在的谓词逻辑表达式

∃x.(~P(x) /\ ~Q(x)) -> ∃x.~(P(x) /\ Q(x))
Theorem exercise7:
  (exists x:A, ~(P x)/\(Q x))->(exists x: A,~(P x /\Q x)).
Proof.
  unfold not.
  intros H1.
  destruct H1 as [a p].
  exists a.
  inversion p.
  intros.
  inversion H1.
  apply H in H2.
  apply H2.
Qed.

  Exercise 8:尝试证明以下包含存在的谓词逻辑表达式

∃x.(~P(x) /\ ~Q(x)) -> ∃x.~(P(x) /\ Q(x))
Theorem exercise8:
  (exists x:A, ((P x)\/(Q x)))<->(exists x: A,P x )\/ (exists x: A,Q x).
Proof.
  split.
  intros.
  destruct H as [a p]. 
  inversion p.
  left.                               
  exists a.
  apply H.
  right.
  exists a.
  apply H.

  intros.
  inversion H.
  destruct H0 as [a p]. 
  exists a.
  left.
  apply p.
  destruct H0 as [a p]. 
  exists a.
  right.
  apply p.
Qed.

  Exercise 9:尝试证明以下包含任意和存在的谓词逻辑表达式

∃x.~P(x) -> ~(∀x.P(x))
Theorem exercise9:
  (exists x:A, ~(P x))->~(forall x: A,P x ).
Proof.
  unfold not.
  intros H0 H1.
  destruct H0 as [a p]. 
  apply p.
  apply H1.
Qed.

  Exercise 10:尝试证明以下包含任意和存在的谓词逻辑表达式

∀x.(P(x) -> ~Q(x)) -> ~(∃x.(P(x) /\ Q(x)))
Theorem exercise10:
  (forall x:A, (P x->~(Q x)))->~(exists x: A,(P x/\Q x)).
Proof.
  unfold not.
  intros H0 H1 .
  destruct H1 as [a p]. 
  inversion p.
  apply H0 in H.
  apply H.
  apply H1.
Qed.

  Exercise 11:尝试证明以下包含任意和存在的谓词逻辑表达式

∀x.(P(x) -> Q(x)) /\ ∃x.P(x) -> ∃x.Q(x)
Theorem exercise11:
  (forall x:A, (P x->Q x))/\(exists x: A, P x)->(exists x: A,Q x).
Proof.
  intros H0.
  inversion H0.
  destruct H1 as [a p]. 
  exists a.
  apply H in p.
  apply p.
Qed.

  Exercise 12:尝试证明以下包含任意和存在的谓词逻辑表达式

∃x.(P(x) /\ Q(x)) /\ ∀x.(P(x) -> R(x)) -> ∃x.(R(x) /\ Q(x))
Theorem exercise12:
  (exists x: A, P x/\Q x)/\(forall x:A, (P x->R x))->(exists x: A,R x/\Q x).
Proof.
  intros H0.
  inversion H0.
  destruct H as [a p]. 
  inversion p.
  exists a.
  apply H1 in H.
  split.
  apply H.
  apply H2.
Qed.

  challenge1:尝试证明以下包含存在的谓词逻辑表达式

∃x.∃y.P(x, y) -> ∃y.∃x.P(x, y)
Variables A B: Set.
Variables P: A -> B -> Prop.
Theorem challenge1:
    (exists x, exists y, P x y) -> (exists y, exists x, P x y).
Proof.
    intros.
    destruct H as [a p1].
    destruct p1 as [b p2].
    exists b, a.
    apply p2.
Qed.

  challenge2:尝试证明以下包含任意的谓词逻辑表达式

P(b) /\ (∀x.∀y.(P(x) /\ P(y) -> x = y)) -> (∀x.(P(x) <-> x = b))
#此处P(b)理解为任意b,满足P(b)
Theorem challenge2:
    (forall b:A,P(b))/\(forall x:A,forall y:A,(P x/\P y->x=y))->(forall x:A,(P x <->forall b:A, x=b)).
Proof.
   intros.
   split.
   inversion H.
   intros.
   apply H1.
   split.
   apply H2.
   apply H0.
   intros.
   inversion H.
   apply H1.    
Qed.

三.下载链接

  在线下载: 请点击这儿下载
  如果下载失败,点击此百度云链接:形式化方法作业四,提取码y825
  如果您有任何疑问,请通过邮箱联系我

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