Аналіз I, Додаток A.4: Змінні та квантифікатори

Деякі приклади використання змінних та квантифікаторів у Lean

namespace VariableExample1variable (X:Type) (x y:X)

x = x : Prop

x = y : Prop

-- #check x+y = y+x   -- тут не будуть перевірятися типи

end VariableExample1

namespace VariableExample2variable (x:ℝ)

x + 3 : ℝ

x + 3 = 5 : Prop

example (h: x = 2) : x + 3 = 5 := byx:ℝh:x = 2⊢ x + 3 = 5 linarithAll goals completed! 🐙

example (h: x ≠ 2) : x + 3 ≠ 5 := byx:ℝh:x ≠ 2⊢ x + 3 ≠ 5
  contrapose! hx:ℝh:x + 3 = 5⊢ x = 2
  linarithAll goals completed! 🐙

example : ¬ ∀ (x:ℝ), x + 3 = 5 := byx:ℝ⊢ ¬∀ (x : ℝ), x + 3 = 5
  simpx:ℝ⊢ ∃ x, ¬x + 3 = 5
  use 0hx:ℝ⊢ ¬0 + 3 = 5
  simpAll goals completed! 🐙

example : ¬ ∀ (x:ℝ), x + 3 ≠ 5 := byx:ℝ⊢ ¬∀ (x : ℝ), x + 3 ≠ 5
  simpx:ℝ⊢ ∃ x, x + 3 = 5
  use 2hx:ℝ⊢ 2 + 3 = 5
  norm_numAll goals completed! 🐙

example : ∃ (x:ℝ), x + 3 = 5 := byx:ℝ⊢ ∃ x, x + 3 = 5
  use 2hx:ℝ⊢ 2 + 3 = 5
  norm_numAll goals completed! 🐙

example : ∀ (x:ℝ), (x+1)^2 = x^2 + 2*x + 1 := byx:ℝ⊢ ∀ (x : ℝ), (x + 1) ^ 2 = x ^ 2 + 2 * x + 1
  intro xx✝:ℝx:ℝ⊢ (x + 1) ^ 2 = x ^ 2 + 2 * x + 1
  ringAll goals completed! 🐙

end VariableExample2

Для цього прикладу тут використовується фіктивне твердження.

example : 0 = 0 := by⊢ 0 = 0
  set x := 342x:ℕ := 342⊢ 0 = 0
  have : x + 155 = 497 := by⊢ 0 = 0
    unfold xx:ℕ := 342⊢ 342 + 155 = 497
    norm_numAll goals completed! 🐙
  rflAll goals completed! 🐙

example : ¬ ∀ (x:ℝ), x + 155 = 497 := by⊢ ¬∀ (x : ℝ), x + 155 = 497
  simp⊢ ∃ x, ¬x + 155 = 497
  use 0h⊢ ¬0 + 155 = 497
  norm_numAll goals completed! 🐙

example : ¬ ∀ x > (0:ℝ), x^2 > x := by⊢ ¬∀ x > 0, x ^ 2 > x
  simp⊢ ∃ x, 0 < x ∧ x ^ 2 ≤ x
  use 0.5h⊢ 0 < 0.5 ∧ 0.5 ^ 2 ≤ 0.5
  norm_numAll goals completed! 🐙

/- Наведений нижче код не перевірятиме тип.

example : ∀ (x:ℝ), x + 3 = 5 := by
  use 2
  sorry

-/

example : ∀ x, (3 < x ∧ x < 2) → (6 < 2*x ∧ 2*x < 4) := by⊢ ∀ (x : ℕ), 3 < x ∧ x < 2 → 6 < 2 * x ∧ 2 * x < 4
  intro xx:ℕ⊢ 3 < x ∧ x < 2 → 6 < 2 * x ∧ 2 * x < 4
  intro hx:ℕh:3 < x ∧ x < 2⊢ 6 < 2 * x ∧ 2 * x < 4
  obtain ⟨ h1, h2 ⟩ := hintrox:ℕh1:3 < xh2:x < 2⊢ 6 < 2 * x ∧ 2 * x < 4
  -- попередні три рядки можна забуцкати в `intro x ⟨ h1, h2 ⟩`
  constructorintro.leftx:ℕh1:3 < xh2:x < 2⊢ 6 < 2 * xintro.rightx:ℕh1:3 < xh2:x < 2⊢ 2 * x < 4
  .intro.leftx:ℕh1:3 < xh2:x < 2⊢ 6 < 2 * x linarithAll goals completed! 🐙
  linarithAll goals completed! 🐙

example : ∃ (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! 🐙

example : ¬ ∃ x, (3 < x ∧ x < 2) ∧ (6 < 2*x ∧ 2*x < 4) := by⊢ ¬∃ x, (3 < x ∧ x < 2) ∧ 6 < 2 * x ∧ 2 * x < 4
  simp⊢ ∀ (x : ℕ), 3 < x → x < 2 → 6 < 2 * x → 4 ≤ 2 * x
  intro x h1 h2 h3x:ℕh1:3 < xh2:x < 2h3:6 < 2 * x⊢ 4 ≤ 2 * x
  linarithAll goals completed! 🐙