Analysis I, Appendix A.5: Nested quantifiers

Some examples of nested quantifiers in Lean

example : ∀ x > (0:ℝ), ∃ y > 0, y^2 = x := by⊢ ∀ x > 0, ∃ y > 0, y ^ 2 = x intro x hxx:ℝhx:x > 0⊢ ∃ y > 0, y ^ 2 = x use √xhx:ℝhx:x > 0⊢ √x > 0 ∧ √x ^ 2 = x constructorh.leftx:ℝhx:x > 0⊢ √x > 0h.rightx:ℝhx:x > 0⊢ √x ^ 2 = x .h.leftx:ℝhx:x > 0⊢ √x > 0 positivityAll goals completed! 🐙 convert Real.sq_sqrt _h.right.convert_2x:ℝhx:x > 0⊢ 0 ≤ x positivityAll goals completed! 🐙namespace SwanExamplevariable (Swans:Type)variable (isBlack : Swans → Prop)example : (¬ ∀ s:Swans, isBlack s) = (∃ s:Swans, ¬ isBlack s) := bySwans:TypeisBlack:Swans → Prop⊢ (¬∀ (s : Swans), isBlack s) = ∃ s, ¬isBlack s simpAll goals completed! 🐙example : (¬ ∃ s:Swans, isBlack s) = (∀ s:Swans, ¬ isBlack s) := bySwans:TypeisBlack:Swans → Prop⊢ (¬∃ s, isBlack s) = ∀ (s : Swans), ¬isBlack s simpAll goals completed! 🐙end SwanExampleexample : (¬ ∀ x, (0 < x ∧ x < Real.pi/2) → Real.cos x ≥ 0) = (∃ x, (0 < x ∧ x < Real.pi/2) ∧ Real.cos x < 0) := by⊢ (¬∀ (x : ℝ), 0 < x ∧ x < Real.pi / 2 → Real.cos x ≥ 0) = ∃ x, (0 < x ∧ x < Real.pi / 2) ∧ Real.cos x < 0 simp⊢ (∃ x, 0 < x ∧ x < Real.pi / 2 ∧ Real.cos x < 0) ↔ ∃ x, (0 < x ∧ x < Real.pi / 2) ∧ Real.cos x < 0 simp_rw [and_assoc]All goals completed! 🐙example : (¬ ∃ x:ℝ, x^2 + x + 1 = 0) = (∀ x:ℝ, x^2 + x + 1 ≠ 0) := by⊢ (¬∃ x, x ^ 2 + x + 1 = 0) = ∀ (x : ℝ), x ^ 2 + x + 1 ≠ 0 simpAll goals completed! 🐙theorem square_expand : ∀ (x:ℝ), (x + 1)^2 = x^2 + 2 * x + 1 := by⊢ ∀ (x : ℝ), (x + 1) ^ 2 = x ^ 2 + 2 * x + 1 intro xx:ℝ⊢ (x + 1) ^ 2 = x ^ 2 + 2 * x + 1 ringAll goals completed! 🐙example : (Real.pi+1)^2 = Real.pi^2 + 2 * Real.pi + 1 := by⊢ (Real.pi + 1) ^ 2 = Real.pi ^ 2 + 2 * Real.pi + 1 apply square_expandAll goals completed! 🐙 -- one can also use `exact square_expand _`example : ∀ (y:ℝ), (Real.cos y + 1)^2 = Real.cos y^2 + 2 * Real.cos y + 1 := by⊢ ∀ (y : ℝ), (Real.cos y + 1) ^ 2 = Real.cos y ^ 2 + 2 * Real.cos y + 1 intro yy:ℝ⊢ (Real.cos y + 1) ^ 2 = Real.cos y ^ 2 + 2 * Real.cos y + 1 apply square_expandAll goals completed! 🐙theorem solve_quadratic : ∃ (x:ℝ), x^2 + 2 * x - 8 = 0 := by⊢ ∃ x, x ^ 2 + 2 * x - 8 = 0 use 2h⊢ 2 ^ 2 + 2 * 2 - 8 = 0 norm_numAll goals completed! 🐙/- The following proof will not typecheck. example : Real.pi^2 + 2 * Real.pi - 8 = 0 := by apply solve_quadratic -/ namespace Remark_A_5_1variable (Man : Type)variable (Mortal : Man → Prop)example (premise : ∀ m : Man, Mortal m) (Socrates : Man) : Mortal Socrates := byMan:TypeMortal:Man → Proppremise:∀ (m : Man), Mortal mSocrates:Man⊢ Mortal Socrates apply premiseAll goals completed! 🐙 -- `exact premise Socrates` would also workend Remark_A_5_1example : (∀ a:ℝ, ∀ b:ℝ, (a+b)^2 = a^2 + 2*a*b + b^2) = (∀ b:ℝ, ∀ a:ℝ, (a+b)^2 = a^2 + 2*a*b + b^2) := by⊢ (∀ (a b : ℝ), (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2) = ∀ (b a : ℝ), (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 rw [forall_comm]All goals completed! 🐙example : (∃ a:ℝ, ∃ b:ℝ, a^2 + b^2 = 0) = (∃ b:ℝ, ∃ a:ℝ, a^2 + b^2 = 0) := by⊢ (∃ a b, a ^ 2 + b ^ 2 = 0) = ∃ b a, a ^ 2 + b ^ 2 = 0 rw [exists_comm]All goals completed! 🐙example : ∀ n:ℤ, ∃ m:ℤ, m > n := by⊢ ∀ (n : ℤ), ∃ m, m > n intro nn:ℤ⊢ ∃ m, m > n use n + 1hn:ℤ⊢ n + 1 > n linarithAll goals completed! 🐙example : ¬ ∃ m:ℤ, ∀ n:ℤ, m > n := by⊢ ¬∃ m, ∀ (n : ℤ), m > n by_contra hh:∃ m, ∀ (n : ℤ), m > n⊢ False choose m hm using hm:ℤhm:∀ (n : ℤ), m > n⊢ False -- `obtain ⟨m, hm⟩ := h` would also work here specialize hm (m+1)m:ℤhm:m > m + 1⊢ False linarithAll goals completed! 🐙 def declaration uses 'sorry'Exercise_A_5_1b : Decidable (∃ x > (0:ℝ), ∀ y > (0:ℝ), y^2 = x ) := by⊢ Decidable (∃ x > 0, ∀ y > 0, y ^ 2 = x) -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. sorryAll goals completed! 🐙def declaration uses 'sorry'Exercise_A_5_1c : Decidable (∃ x > (0:ℝ), ∃ y > (0:ℝ), y^2 = x ) := by⊢ Decidable (∃ x > 0, ∃ y > 0, y ^ 2 = x) -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. sorryAll goals completed! 🐙def declaration uses 'sorry'Exercise_A_5_1d : Decidable (∀ y > (0:ℝ), ∃ x > (0:ℝ), y^2 = x ) := by⊢ Decidable (∀ y > 0, ∃ x > 0, y ^ 2 = x) -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. sorryAll goals completed! 🐙def declaration uses 'sorry'Exercise_A_5_1e : Decidable (∃ y > (0:ℝ), ∀ x > (0:ℝ), y^2 = x ) := by⊢ Decidable (∃ y > 0, ∀ x > 0, y ^ 2 = x) -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. sorryAll goals completed! 🐙