quantifiers_and_equality exercises

quantifiers_and_equality.lean

@@ -145,3 +145,54 @@ example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
       (fun hq =>
         fun x => Or.inr (hq x))
 
+variable (α : Type) (p q : α → Prop)
+variable (r : Prop)
+
+example : α → ((∀ x : α, r) ↔ r) :=
+  fun hα =>
+    have h1 := fun h => h hα
+    have h2 := fun hr => fun _ => hr
+    Iff.intro h1 h2
+open Classical in
+example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
+  have h1 : (∀ (x : α), p x ∨ r) → (∀ (x : α), p x) ∨ r :=
+    fun h =>
+      sorry
+  have h2 : (∀ (x : α), p x) ∨ r → ∀ (x : α), p x ∨ r :=
+    fun h =>
+      h.elim
+        (fun hl =>
+          fun hx =>
+            Or.inl (hl hx))
+        (fun hr =>
+          fun hx =>
+            Or.inr hr)
+  Iff.intro h1 h2
+
+example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
+  have h1 : (∀ (x : α), r → p x) → r → ∀ (x : α), p x :=
+    fun h =>
+      fun hr =>
+        fun x =>
+          (h x) hr
+  have h2 : (r → ∀ (x : α), p x) → ∀ (x : α), r → p x :=
+    fun h =>
+      fun x =>
+        fun hr =>
+          (h hr) x
+  Iff.intro h1 h2
+
+
+variable (men : Type) (barber : men)
+variable (shaves : men → men → Prop)
+
+open Classical in
+example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False :=
+  have hbarber : shaves barber barber ↔ ¬shaves barber barber :=
+    h barber
+  (em (shaves barber barber)).elim
+    (fun hbarberself =>
+      have hnbarbarself := hbarber.mp hbarberself
+      hnbarbarself hbarberself)
+    (fun hnbarbarself =>
+      hnbarbarself (hbarber.mpr hnbarbarself))