Coq中的谓词逻辑 [英] Predicate Logic in Coq

问题描述

任何人都可以在谓词逻辑和使用coq方面对这两个定理提供帮助.我无法理解coq语法.

Can anyone help with these two theorems in regards to predicate logic and using coq. I have trouble understanding coq syntax.

1. 存在x:D，(R x/\ S x)|-(存在y:D，R y)/\(存在z:D，S z)
2. 存在x:D，(R x \/S x)|-(存在y:D，R y)\/(存在z:D，S z)

推荐答案

如果我很好理解，那么您要寻找的是证明如果一个元素同时满足两个道具，那么有一个满足每个 Prop 的特定元素:

If I understood well, what you're looking for is to prove that if an element satisfies both Props, then there is a specific element that satisfies each 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).

并且，如果一个元素至少满足道具之一，那么对于道具之一，就存在一个满足它的元素:

And that if an element satisfies at least one of the Props, then for one of the Props, there exists and element that satisfies it :

Lemma or : forall (D:Type)(R S:D -> Prop), 
(exists x:D, (R x \/ S x)) -> (exists y:D, R y) \/ (exists z:D, S z).

证明将非常简单，如下所示:

The proofs would then be quite simple, as following :

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).
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), 
(exists x:D, (R x \/ S x)) -> (exists y:D, R y) \/ (exists z:D, S z).
Proof.
  intros. destruct H. 
  destruct H; [left | right]; exists x; apply H.
Qed.

这篇关于Coq中的谓词逻辑的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！