Coq의 술어 논리 [closed]

Question

술어 논리와 coq 사용과 관련 하여이 두 가지 정리를 도울 수 있습니까? coq 구문을 이해하는 데 문제가 있습니다.

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)

Answer 1

내가 잘 이해했다면, 당신이 찾고있는 것은 요소가 두 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), 
(exists x:D, (R x \/ S x)) -> (exists y:D, R y) \/ (exists z:D, S z).

증명은 다음과 같이 매우 간단합니다.

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.