Predicate Logic in Coq [chiuso]

Question

Qualcuno può aiutare con questi due teoremi per quanto riguarda la logica dei predicati e l'utilizzo di coq. Ho problemi a capire la sintassi coq.

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

Answer 1

Se ho capito bene, quello che stai cercando è quello di dimostrare che se un elemento soddisfa entrambi i puntelli , poi c'è un elemento specifico che soddisfa ogni 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).

E che se un elemento soddisfa almeno uno degli oggetti di scena , allora per uno degli oggetti di scena , esiste un elemento che lo soddisfa:

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

Le dimostrazioni sarebbero quindi abbastanza semplici, come segue:

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.