File CoMoEx.Forall
Ziel dieses Files ist es, den Allquantor näher kennenzulernen.
Section forallE_demo.
Variable T : Set.
Variable some_t : T.
Section forallE_demo_1.
Variable Q : Prop.
Hypothesis A1 : ∀ x : T, Q.
Aussage Q gilt also für alle x aus T.
Hier wird noch ein x aus T gefordert, da es in Coq wichtig ist, ob ein "Datentyp" (hier T) nicht-leer ist (inhabited).
exact some_t.
Hiermit geben wir ein gefordertes Element an.
Qed.
End forallE_demo_1.
Section forallE_demo_2.
Variable P : T → Prop.
Hypothesis A1 : ∀ x, P x.
Theorem forallE_demo_2 : P some_t.
End forallE_demo_1.
Section forallE_demo_2.
Variable P : T → Prop.
Hypothesis A1 : ∀ x, P x.
Theorem forallE_demo_2 : P some_t.
Unteschied zum ersten Beispiel: jetzt werden wir nicht mehr irgendein beliebiges x aus T brauchen, sondern ein bestimmtes spezielles Element.
Proof.
Admitted.
End forallE_demo_2.
End forallE_demo.
Section forallI_demo.
Variable T : Set.
Section forallI_demo_1.
Variable Q : Prop.
Hypothesis A1 : Q.
Theorem forallI_demo_1 : ∀ x : T, Q.
Proof.
intro t. exact A1.
Qed.
End forallI_demo_1.
Section forallI_demo_2.
Variable P : T → Prop.
Hypothesis A1 : ∀ x, P x.
Theorem forallI_demo_2 : ∀ x, P x.
Proof.
exact A1.
Admitted.
End forallE_demo_2.
End forallE_demo.
Section forallI_demo.
Variable T : Set.
Section forallI_demo_1.
Variable Q : Prop.
Hypothesis A1 : Q.
Theorem forallI_demo_1 : ∀ x : T, Q.
Proof.
intro t. exact A1.
Qed.
End forallI_demo_1.
Section forallI_demo_2.
Variable P : T → Prop.
Hypothesis A1 : ∀ x, P x.
Theorem forallI_demo_2 : ∀ x, P x.
Proof.
exact A1.
Natürlich kann man dieses Goal ziemlich trivial lösen. Dies ist jedoch nicht der Sinn dieser Aufgabe.
Restart.
Ziel ist es, hier sowohl Eliminierung als auch Einführung von Allquantoren explizit anzuwenden.
In dieser Section kommen nun ein paar kombinierte Beispiele, die grundsätzlich nach demselben Schema ablaufen. Konkret heißt das hier, dass wir den forall-Operator mit and, or, impl und iff kommutieren. Dadurch kann man nochmal die grundlegenden Funktionsweisen dieser bereits bekannten Operatoren kombinieren.
Section forall_comm_ops.
Variable T : Set.
Variables P Q : T → Prop.
Section forall_comm_and_1.
Hypothesis H1 : ∀ x, P x ∧ Q x.
Theorem forall_comm_and_1_1 : (∀ x, P x) ∧ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_and_1.
Section forall_comm_and_2.
Hypothesis H1 : ∀ x y, P x ∧ Q y.
Theorem forall_comm_and_2_1 : (∀ x, P x) ∧ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_and_2.
Section forall_comm_or_1.
Hypothesis H1 : ∀ x, P x ∨ Q x.
Theorem forall_comm_or_1_1 : (∀ x, P x) ∨ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_or_1.
Section forall_comm_or_2.
Hypothesis H1 : ∀ x y, P x ∨ Q y.
Theorem forall_comm_or_2_1 : (∀ x, P x) ∨ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_or_2.
Section forall_comm_impl_1.
Hypothesis H1 : ∀ x, P x → Q x.
Theorem forall_comm_impl_1_1 : (∀ x, P x) → ∀ x, Q x.
Proof.
Admitted.
End forall_comm_impl_1.
Section forall_comm_impl_2.
Hypothesis H1 : ∀ x y, P x → Q y.
Theorem forall_comm_impl_2_1 : (∀ x, P x) → ∀ x, Q x.
Proof.
Admitted.
End forall_comm_impl_2.
Section forall_comm_iff_1.
Hypothesis H1 : ∀ x, P x ↔ Q x.
Theorem forall_comm_iff_1_1 : (∀ x, P x) ↔ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_iff_1.
Section forall_comm_iff_2.
Hypothesis H1 : ∀ x y, P x ↔ Q y.
Theorem forall_comm_iff_2_1 : (∀ x, P x) ↔ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_iff_2.
End forall_comm_ops.
Section forall_ex_1.
Variable T : Set.
Variable P : T → T → Prop.
Hypothesis A1 : ∃ x, ∀ y, P x y.
Theorem forall_ex_1_1 : ∀ y, ∃ x, P x y.
Proof.
Admitted.
End forall_ex_1.
Section forall_ex_2.
Variable T : Set.
Variables P Q : T → Prop.
Variable R : T → T → Prop.
Hypothesis A1 : ∀ x, ∃ y, R x y ∧ P y.
Hypothesis A2 : ∀ x, P x → Q x.
Theorem forall_ex_2_1 : ∀ x, ∃ y, R x y ∧ Q y.
Proof.
Admitted.
End forall_ex_2.
Section forall_ex_3.
Variable T : Set.
Variables P Q : T → Prop.
Variable R : T → T → Prop.
Hypothesis A1 : ∀ x y z, (R x y ∧ R x z) → R y z.
Hypothesis A2 : ∀ x, R x x.
Hypothesis A3 : ∀ x, ∃ y, R x y ∧ P y.
Theorem forall_ex_3_1 : ∀ x, ∃ y, R y x ∧ P y.
Proof.
Admitted.
End forall_ex_3.
Section forall_ex_4.
Variable T : Set.
Variable P : T → Prop.
Variables R S : T → T → Prop.
Hypothesis A1 : ∀ x y, S x y → P y.
Hypothesis A2 : ∀ x y, R x y → ∃ z, S z y.
Theorem forall_ex_4_1 : ∀ x y, R x y → P y.
Proof.
Admitted.
End forall_ex_4.
Section forall_ex_5.
Variable T : Set.
Variable R : T → T → Prop.
Hypothesis A1 : ∀ x, ∃ y, R x y.
Hypothesis A2 : ∀ x y z, (R x y ∧ R y z) → R x z.
Hypothesis A3 : ∀ x y, R x y → R y x.
Theorem forall_ex_5_1 : ∀ x, R x x.
Proof.
Admitted.
End forall_ex_5.
Section forall_ex_6.
Variable T : Set.
Variable z : T.
Variable P : T → Prop.
Variable R : T → T → Prop.
Hypothesis A1 : ∀ x, ∃ y, R x y.
Hypothesis A2 : ∀ y, R z y → ¬ P y.
Theorem forall_ex_6_1 : ¬ ∀ y, R z y → P y.
Proof.
Admitted.
End forall_ex_6.
Section forall_ex_7.
Variable T : Set.
Variable P : T → T → Prop.
Theorem forall_ex_7_1 : ∀ x, ∃ y, P x y ∨ P y x → ∀ x, (∃ y, P x y) ∨ ∃ y, P y x.
Proof.
Admitted.
End forall_ex_7.
Variable T : Set.
Variables P Q : T → Prop.
Section forall_comm_and_1.
Hypothesis H1 : ∀ x, P x ∧ Q x.
Theorem forall_comm_and_1_1 : (∀ x, P x) ∧ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_and_1.
Section forall_comm_and_2.
Hypothesis H1 : ∀ x y, P x ∧ Q y.
Theorem forall_comm_and_2_1 : (∀ x, P x) ∧ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_and_2.
Section forall_comm_or_1.
Hypothesis H1 : ∀ x, P x ∨ Q x.
Theorem forall_comm_or_1_1 : (∀ x, P x) ∨ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_or_1.
Section forall_comm_or_2.
Hypothesis H1 : ∀ x y, P x ∨ Q y.
Theorem forall_comm_or_2_1 : (∀ x, P x) ∨ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_or_2.
Section forall_comm_impl_1.
Hypothesis H1 : ∀ x, P x → Q x.
Theorem forall_comm_impl_1_1 : (∀ x, P x) → ∀ x, Q x.
Proof.
Admitted.
End forall_comm_impl_1.
Section forall_comm_impl_2.
Hypothesis H1 : ∀ x y, P x → Q y.
Theorem forall_comm_impl_2_1 : (∀ x, P x) → ∀ x, Q x.
Proof.
Admitted.
End forall_comm_impl_2.
Section forall_comm_iff_1.
Hypothesis H1 : ∀ x, P x ↔ Q x.
Theorem forall_comm_iff_1_1 : (∀ x, P x) ↔ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_iff_1.
Section forall_comm_iff_2.
Hypothesis H1 : ∀ x y, P x ↔ Q y.
Theorem forall_comm_iff_2_1 : (∀ x, P x) ↔ ∀ x, Q x.
Proof.
Admitted.
End forall_comm_iff_2.
End forall_comm_ops.
Section forall_ex_1.
Variable T : Set.
Variable P : T → T → Prop.
Hypothesis A1 : ∃ x, ∀ y, P x y.
Theorem forall_ex_1_1 : ∀ y, ∃ x, P x y.
Proof.
Admitted.
End forall_ex_1.
Section forall_ex_2.
Variable T : Set.
Variables P Q : T → Prop.
Variable R : T → T → Prop.
Hypothesis A1 : ∀ x, ∃ y, R x y ∧ P y.
Hypothesis A2 : ∀ x, P x → Q x.
Theorem forall_ex_2_1 : ∀ x, ∃ y, R x y ∧ Q y.
Proof.
Admitted.
End forall_ex_2.
Section forall_ex_3.
Variable T : Set.
Variables P Q : T → Prop.
Variable R : T → T → Prop.
Hypothesis A1 : ∀ x y z, (R x y ∧ R x z) → R y z.
Hypothesis A2 : ∀ x, R x x.
Hypothesis A3 : ∀ x, ∃ y, R x y ∧ P y.
Theorem forall_ex_3_1 : ∀ x, ∃ y, R y x ∧ P y.
Proof.
Admitted.
End forall_ex_3.
Section forall_ex_4.
Variable T : Set.
Variable P : T → Prop.
Variables R S : T → T → Prop.
Hypothesis A1 : ∀ x y, S x y → P y.
Hypothesis A2 : ∀ x y, R x y → ∃ z, S z y.
Theorem forall_ex_4_1 : ∀ x y, R x y → P y.
Proof.
Admitted.
End forall_ex_4.
Section forall_ex_5.
Variable T : Set.
Variable R : T → T → Prop.
Hypothesis A1 : ∀ x, ∃ y, R x y.
Hypothesis A2 : ∀ x y z, (R x y ∧ R y z) → R x z.
Hypothesis A3 : ∀ x y, R x y → R y x.
Theorem forall_ex_5_1 : ∀ x, R x x.
Proof.
Admitted.
End forall_ex_5.
Section forall_ex_6.
Variable T : Set.
Variable z : T.
Variable P : T → Prop.
Variable R : T → T → Prop.
Hypothesis A1 : ∀ x, ∃ y, R x y.
Hypothesis A2 : ∀ y, R z y → ¬ P y.
Theorem forall_ex_6_1 : ¬ ∀ y, R z y → P y.
Proof.
Admitted.
End forall_ex_6.
Section forall_ex_7.
Variable T : Set.
Variable P : T → T → Prop.
Theorem forall_ex_7_1 : ∀ x, ∃ y, P x y ∨ P y x → ∀ x, (∃ y, P x y) ∨ ∃ y, P y x.
Proof.
Admitted.
End forall_ex_7.