Dự đoán Logic trong Coq [đã đóng]

Question

Bất cứ ai có thể giúp đỡ với hai định lý liên quan đến logic vị từ và sử dụng coq. Tôi gặp khó khăn khi hiểu cú pháp coq.

1. tồn tại x: D, (R x / \ S x) | - (tồn tại y: D, R y) / \ (tồn tại z: D, S z)
2. tồn tại x: D, (R x \ / S x) | - (tồn tại y: D, R y) \ / (tồn tại z: D, S z)

Answer 1

Nếu tôi hiểu rõ, điều bạn đang tìm là chứng minh rằng nếu một phần tử thỏa mãn cả hai Props , thì sẽ có một phần tử cụ thể thỏa mãn mỗi 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).

Và rằng nếu một phần tử thỏa mãn ít nhất một trong các Đạo cụ , thì đối với một trong các Đạo cụ , tồn tại và phần tử thỏa mãn nó:

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

Các bằng chứng sau đó sẽ khá đơn giản, như sau:

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.