Merge branch 'more-examples' into 'main'

More examples

See merge request !32

src/Forall.v

@@ -163,3 +163,104 @@ Section forall_comm_ops.
   End forall_comm_iff_2.
 
 End forall_comm_ops.
+
+Section forall_ex_1.
+
+  Variable T : Set.
+  Variable P : T -> T -> Prop.
+
+  Hypothesis A1 : exists x, forall y, P x y.
+
+  Theorem forall_ex_1_1 : forall y, exists 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 : forall x, exists y, R x y /\ P y.
+  Hypothesis A2 : forall x, P x -> Q x.
+
+  Theorem forall_ex_2_1 : forall x, exists 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 : forall x y z, (R x y /\ R x z) -> R y z.
+  Hypothesis A2 : forall x, R x x.
+  Hypothesis A3 : forall x, exists y, R x y /\ P y.
+
+  Theorem forall_ex_3_1 : forall x, exists 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 : forall x y, S x y -> P y.
+  Hypothesis A2 : forall x y, R x y -> exists z, S z y.
+
+  Theorem forall_ex_4_1 : forall 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 : forall x, exists y, R x y.
+  Hypothesis A2 : forall x y z, (R x y /\ R y z) -> R x z.
+  Hypothesis A3 : forall x y, R x y -> R y x.
+
+  Theorem forall_ex_5_1 : forall 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 : forall x, exists y, R x y.
+  Hypothesis A2 : forall y, R z y -> ~ P y.
+
+  Theorem forall_ex_6_1 : ~ forall 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 : forall x, exists y, P x y \/ P y x -> forall x, (exists y, P x y) \/ exists y, P y x.
+  Proof.
+  Admitted.
+
+End forall_ex_7.

src/SomeExamples.v

@@ -103,3 +103,49 @@ Section se_3.
   Admitted.
 
 End se_3.
+
+Section se_4.
+
+  Variables p1 p2 p3 : Prop.
+
+  Hypothesis A1 : (p1 -> p2) /\ (p2 -> p3) /\ (p3 -> ~ p1).
+
+  Theorem se_4_1 : ~ p1.
+  Proof.
+  Admitted.
+
+End se_4.
+
+Section se_5.
+
+  Variables p1 p2 : Prop.
+
+  Hypothesis A1 : (~ p1 /\ p2) \/ (~p2 /\ p1).
+
+  Theorem se_5_1 : ~ (p1 /\ p2).
+  Proof.
+  Admitted.
+
+End se_5.
+
+Section se_6.
+
+  Variables p1 p2 : Prop.
+
+  Hypothesis A1 : (p1 -> (p1 -> p2)) -> ~ p1.
+
+  Theorem se_6_1 : ~ (p1 /\ p2).
+  Proof.
+  Admitted.
+
+End se_6.
+
+Section se_7.
+
+  Variables p1 p2 : Prop.
+
+  Theorem se_7_1 : ((p1 -> ~(p1 -> p2)) -> ~(p1 -> p1)) -> p2.
+  Proof.
+  Admitted.
+
+End se_7.