Predikat Logika di Coq [tutup]

Question

Adakah yang bisa membantu dengan dua teorema ini sehubungan dengan logika predikat dan menggunakan coq. Saya kesulitan memahami sintaks coq.

1. ada x: D, (R x / \ S x) | - (ada y: D, R y) / \ (ada z: D, S z)
2. ada x: D, (R x \ / S x) | - (ada y: D, R y) \ / (ada z: D, S z)

Answer 1

Jika saya mengerti dengan baik, yang Anda cari adalah untuk membuktikan bahwa jika sebuah elemen memenuhi kedua Props , maka ada elemen tertentu yang memenuhi setiap 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).

Dan jika sebuah elemen memenuhi setidaknya satu dari Props , maka untuk salah satu dari Props , ada dan elemen yang memenuhi itu:

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).

Buktinya kemudian cukup sederhana, sebagai berikut:

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.