My solutions to Tao's Analysis I, formalized in Lean
danabra.mov
1import Mathlib.Tactic
2
3/-!
4# Analysis I, Appendix A.5: Nested quantifiers
5
6Some examples of nested quantifiers in Lean
7
8-/
9
10
11example : ∀ x > (0:ℝ), ∃ y > 0, y^2 = x := by
12 intro x hx
13 use √x
14 constructor
15 . positivity
16 convert Real.sq_sqrt _
17 positivity
18
19namespace SwanExample
20
21variable (Swans:Type)
22variable (isBlack : Swans → Prop)
23
24example : (¬ ∀ s:Swans, isBlack s) = (∃ s:Swans, ¬ isBlack s) := by
25 simp
26
27example : (¬ ∃ s:Swans, isBlack s) = (∀ s:Swans, ¬ isBlack s) := by
28 simp
29
30end SwanExample
31
32example : (¬ ∀ x, (0 < x ∧ x < Real.pi/2) → Real.cos x ≥ 0) = (∃ x, (0 < x ∧ x < Real.pi/2) ∧ Real.cos x < 0) := by
33 simp
34 simp_rw [and_assoc]
35
36example : (¬ ∃ x:ℝ, x^2 + x + 1 = 0) = (∀ x:ℝ, x^2 + x + 1 ≠ 0) := by
37 simp
38
39theorem square_expand : ∀ (x:ℝ), (x + 1)^2 = x^2 + 2 * x + 1 := by
40 intro x
41 ring
42
43example : (Real.pi+1)^2 = Real.pi^2 + 2 * Real.pi + 1 := by
44 apply square_expand -- one can also use `exact square_expand _`
45
46example : ∀ (y:ℝ), (Real.cos y + 1)^2 = Real.cos y^2 + 2 * Real.cos y + 1 := by
47 intro y
48 apply square_expand
49
50theorem solve_quadratic : ∃ (x:ℝ), x^2 + 2 * x - 8 = 0 := by
51 use 2
52 norm_num
53
54/- The following proof will not typecheck.
55
56example : Real.pi^2 + 2 * Real.pi - 8 = 0 := by
57 apply solve_quadratic
58
59-/
60
61namespace Remark_A_5_1
62
63variable (Man : Type)
64variable (Mortal : Man → Prop)
65
66example
67 (premise : ∀ m : Man, Mortal m)
68 (Socrates : Man) :
69 Mortal Socrates := by
70 apply premise -- `exact premise Socrates` would also work
71
72end Remark_A_5_1
73
74example :
75 (∀ a:ℝ, ∀ b:ℝ, (a+b)^2 = a^2 + 2*a*b + b^2)
76 = (∀ b:ℝ, ∀ a:ℝ, (a+b)^2 = a^2 + 2*a*b + b^2)
77 := by
78 rw [forall_comm]
79
80example :
81 (∃ a:ℝ, ∃ b:ℝ, a^2 + b^2 = 0)
82 = (∃ b:ℝ, ∃ a:ℝ, a^2 + b^2 = 0)
83 := by
84 rw [exists_comm]
85
86example : ∀ n:ℤ, ∃ m:ℤ, m > n := by
87 intro n
88 use n + 1
89 linarith
90
91example : ¬ ∃ m:ℤ, ∀ n:ℤ, m > n := by
92 by_contra h
93 obtain ⟨m, hm⟩ := h
94 specialize hm (m+1)
95 linarith
96
97/-- Exercise A.5.1 -/
98def Exercise_A_5_1a : Decidable (∀ x > (0:ℝ), ∀ y > (0:ℝ), y^2 = x ) := by
99 -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
100 sorry
101
102def Exercise_A_5_1b : Decidable (∃ x > (0:ℝ), ∀ y > (0:ℝ), y^2 = x ) := by
103 -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
104 sorry
105
106def Exercise_A_5_1c : Decidable (∃ x > (0:ℝ), ∃ y > (0:ℝ), y^2 = x ) := by
107 -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
108 sorry
109
110def Exercise_A_5_1d : Decidable (∀ y > (0:ℝ), ∃ x > (0:ℝ), y^2 = x ) := by
111 -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
112 sorry
113
114def Exercise_A_5_1e : Decidable (∃ y > (0:ℝ), ∀ x > (0:ℝ), y^2 = x ) := by
115 -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
116 sorry