Predicate Logic ใน Coq [ปิด]

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

ถ้าฉันเข้าใจดีสิ่งที่คุณกำลังมองหาคือการพิสูจน์ว่าหากองค์ประกอบตรงตามอุปกรณ์ประกอบฉากทั้งสองแล้วมีองค์ประกอบเฉพาะที่ตรงตามข้อเสนอแต่ละข้อ :

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.