CoMoEx FOL.Exists
Ziel dieses Files ist es, den Existenzquantor in Coq näher zu betrachten.
Section existsI_demo.
Variable T : Set.
Section existsI_demo_1.
Variable Q : Prop.
Variable some_t : T.
Hypothesis A1 : Q.
Einfachstes Beispiel: Wir wollen zeigen, dass ein x existiert, sodass Q gilt. Q ist ein konstantes Prädikatensymbol, hängt also nicht von x ab. Zudem wissen wir schon, dass Q grundsätzlich gilt. Dieses Beispiel reduziert sich also darauf, zu zeigen, dass überhaupt irgendein x aus T existiert, dass also T nicht-leer ist. Dies ist über some_t sichergestellt. (Wir nehmen das hier also einfach an, da der Fokus auf dem Existenzquantor, nicht aber auf Inhabitation liegt.
Theorem existsI_demo_1 : ∃ x : T, Q.
Proof.
∃ some_t.
exact A1.
Qed.
End existsI_demo_1.
Section existsI_demo_2.
Variable P : T → Prop.
Variable some_t : T.
Hypothesis A1 : P some_t.
Proof.
∃ some_t.
exact A1.
Qed.
End existsI_demo_1.
Section existsI_demo_2.
Variable P : T → Prop.
Variable some_t : T.
Hypothesis A1 : P some_t.
Ähnliches Beispiel.
Theorem existsI_demo_2 : ∃ x, P x.
Proof.
Admitted.
End existsI_demo_2.
Section existsI_demo_3.
Variable P : T → Prop.
Variable x : T.
Hypothesis A1 : P x.
Proof.
Admitted.
End existsI_demo_2.
Section existsI_demo_3.
Variable P : T → Prop.
Variable x : T.
Hypothesis A1 : P x.
Ähnliches Beispiel. Welchen Zweck könnte es haben, dass ich Bsp. 2 UND 3 anführe?
Theorem existsI_demo_3 : ∃ x, P x.
Proof.
Admitted.
End existsI_demo_3.
End existsI_demo.
Section existsE_demo.
Variable T : Set.
Variable Q : Prop.
Section existsE_demo_1.
Hypothesis A1 : ∃ x : T, Q.
Theorem existsE_demo_1 : Q.
Proof.
destruct A1 as [x A2].
Proof.
Admitted.
End existsI_demo_3.
End existsI_demo.
Section existsE_demo.
Variable T : Set.
Variable Q : Prop.
Section existsE_demo_1.
Hypothesis A1 : ∃ x : T, Q.
Theorem existsE_demo_1 : Q.
Proof.
destruct A1 as [x A2].
A1 sagt "Es gibt ein x, sodass Q gilt." Also nehme ich dieses x einfach mal als gegeben an, zudem die zugehörige Aussage. Damit arbeite ich weiter.
exact A2.
Qed.
End existsE_demo_1.
Section existsE_demo_2.
Variable P : T → Prop.
Hypothesis A1 : ∃ x, Q → P x.
Hypothesis A2 : Q.
Qed.
End existsE_demo_1.
Section existsE_demo_2.
Variable P : T → Prop.
Hypothesis A1 : ∃ x, Q → P x.
Hypothesis A2 : Q.
Hier muss man wohl nicht nur eliminieren, sondern auch einführen...
In dieser Section kommen nun ein paar kombinierte Beispiele, die grundsätzlich nach demselben Schema ablaufen. Konkret heißt das hier, dass wir den exists-Operator mit and und or kommutieren. Dadurch kann man nochmal die grundlegenden Funktionsweisen dieser bereits bekannten Operatoren kombinieren.
Section exists_comm_ops.
Variable T : Set.
Variables P Q : T → Prop.
Section exists_comm_and_1.
Hypothesis H1 : ∃ x, P x ∧ Q x.
Theorem exists_comm_and_1_1 : (∃ x, P x) ∧ ∃ x, Q x.
Proof.
Admitted.
End exists_comm_and_1.
Section exists_comm_and_2.
Hypothesis H1 : ∃ x y, P x ∧ Q y.
Theorem exists_comm_and_2_1 : (∃ x, P x) ∧ ∃ x, Q x.
Proof.
Admitted.
End exists_comm_and_2.
Section exists_comm_or_1.
Hypothesis H1 : ∃ x, P x ∨ Q x.
Theorem exists_comm_or_1_1 : (∃ x, P x) ∨ ∃ x, Q x.
Proof.
Admitted.
End exists_comm_or_1.
Section exists_comm_or_2.
Hypothesis H1 : ∃ x y, P x ∨ Q y.
Theorem exists_comm_or_2_1 : (∃ x, P x) ∨ ∃ x, Q x.
Proof.
Admitted.
End exists_comm_or_2.
End exists_comm_ops.
Variable T : Set.
Variables P Q : T → Prop.
Section exists_comm_and_1.
Hypothesis H1 : ∃ x, P x ∧ Q x.
Theorem exists_comm_and_1_1 : (∃ x, P x) ∧ ∃ x, Q x.
Proof.
Admitted.
End exists_comm_and_1.
Section exists_comm_and_2.
Hypothesis H1 : ∃ x y, P x ∧ Q y.
Theorem exists_comm_and_2_1 : (∃ x, P x) ∧ ∃ x, Q x.
Proof.
Admitted.
End exists_comm_and_2.
Section exists_comm_or_1.
Hypothesis H1 : ∃ x, P x ∨ Q x.
Theorem exists_comm_or_1_1 : (∃ x, P x) ∨ ∃ x, Q x.
Proof.
Admitted.
End exists_comm_or_1.
Section exists_comm_or_2.
Hypothesis H1 : ∃ x y, P x ∨ Q y.
Theorem exists_comm_or_2_1 : (∃ x, P x) ∨ ∃ x, Q x.
Proof.
Admitted.
End exists_comm_or_2.
End exists_comm_ops.