如何解决Coq中的谓词逻辑
任何人都可以就谓词逻辑和使用coq提出这两个定理的帮助。我无法理解coq语法。
- 存在x:D,(R x / \ S x)|-(存在y:D,R y)/ \(存在z:D,S z)
- 存在x:D,(R x \ / S x)|-(存在y:D,R y)\ /(存在z:D,S z)
解决方法
如果我很好理解,您正在寻找的是证明如果一个元素同时满足两个 Props 的要求,那么就有一个特定的元素可以满足每个 Prop 的要求:
Lemma and : forall (D:Type)(R S:D -> Prop),(exists x:D,(R x /\ S x)) -> (exists y:D,R y) /\ (exists z:D,S z).
并且如果一个元素至少满足道具之一,那么对于道具之一,就存在一个满足它的元素:
Lemma or : forall (D:Type)(R S:D -> Prop),(R x \/ S x)) -> (exists y:D,R y) \/ (exists z:D,S z).
然后,证明将非常简单,如下所示:
Lemma and : forall (D:Type)(R S:D -> Prop),S z).
Proof.
intros. destruct H. destruct H as [H1 H2].
split; exists x; [apply H1 | apply H2].
Qed.
Lemma or : forall (D:Type)(R S:D -> Prop),S z).
Proof.
intros. destruct H.
destruct H; [left | right]; exists x; apply H.
Qed.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。