Аналіз I, Додаток A.1

Вступ до математичних тверджень. Демонструє деякі базові тактики та синтаксис Lean.

-- Приклад A.1.1. Те, що в підручнику називається «твердженнями», є об'єктами типу `Prop` в Lean. Крім того, в Lean ми схильні присвоювати "мусорні" значення виразам, які зазвичай вважаються невизначеними, тому обговорення невизначених термінів у підручнику слід відповідно скоригувати.

2 + 2 = 4 : Prop#check 2+2=4

2 + 2 = 4 : Prop

2 + 2 = 5 : Prop#check 2+2=5

2 + 2 = 5 : Prop

Кожне добре сформульоване твердження або істинне, або хибне...

example (P:Prop) : (P=true) ∨ (P=false) := byP:Prop⊢ P = (true = true) ∨ P = (false = true) simpP:Prop⊢ P ∨ ¬P; tautoAll goals completed! 🐙

.. але не одночасно.

example (P:Prop) : ¬ ((P=true) ∧ (P=false)) := byP:Prop⊢ ¬(P = (true = true) ∧ P = (false = true)) simpAll goals completed! 🐙

-- Примітка: `P=true` та `P=false` спрощуються до `P` та `¬P` відповідно.

Щоб довести істинність твердження, достатньо показати, що воно не є хибним,

example {P:Prop} (h: P ≠ false) : P = true := byP:Proph:P ≠ (false = true)⊢ P = (true = true) simpP:Proph:P ≠ (false = true)⊢ P; tautoAll goals completed! 🐙

тоді як для того, щоб довести, що твердження хибне, достатньо довести, що воно не є істинним.

example {P:Prop} (h: P ≠ true) : P = false := byP:Proph:P ≠ (true = true)⊢ P = (false = true) simpP:Proph:P ≠ (true = true)⊢ ¬P; tautoAll goals completed! 🐙

Це твердження істінне, але навряд чи буде дуже корисним.

example : 2 = 2 := rfl

Це твердження також істінне, але не дуже ефективне.

example : 4 ≤ 4 := by⊢ 4 ≤ 4 norm_numAll goals completed! 🐙

/- This is an expression, not a statement. -/
2 + 3 * 5 : ℕ#check 2 + 3*5

2 + 3 * 5 : ℕ

/- Це твердження, а не вираз. -/
2 + 3 * 5 = 17 : Prop#check 2 + 3*5 = 17

2 + 3 * 5 = 17 : Prop

Prime (30 + 5) : Prop#check Prime (30+5)

Prime (30 + 5) : Prop

30 + 5 ≤ 42 - 7 : Prop#check 30+5 ≤ 42-7

30 + 5 ≤ 42 - 7 : Prop

Кон'юнкція

example {X Y: Prop} (hX: X) (hY: Y) : X ∧ Y := byX:PropY:ProphX:XhY:Y⊢ X ∧ Y
  constructorleftX:PropY:ProphX:XhY:Y⊢ XrightX:PropY:ProphX:XhY:Y⊢ Y
  .leftX:PropY:ProphX:XhY:Y⊢ X exact hXAll goals completed! 🐙
  exact hYAll goals completed! 🐙

example {X Y: Prop} (hXY: X ∧ Y) : X := byX:PropY:ProphXY:X ∧ Y⊢ X
  exact hXY.1All goals completed! 🐙

example {X Y: Prop} (hXY: X ∧ Y) : Y := byX:PropY:ProphXY:X ∧ Y⊢ Y
  exact hXY.2All goals completed! 🐙

example {X Y: Prop} (hX: ¬ X) : ¬ (X ∧ Y) := byX:PropY:ProphX:¬X⊢ ¬(X ∧ Y)
  contrapose! hXX:PropY:ProphX:X ∧ Y⊢ X
  exact hX.1All goals completed! 🐙

example {X Y: Prop} (hY: ¬ Y) : ¬ (X ∧ Y) := byX:PropY:ProphY:¬Y⊢ ¬(X ∧ Y)
  contrapose! hYX:PropY:ProphY:X ∧ Y⊢ Y
  exact hY.2All goals completed! 🐙

example : (2+2=4) ∧ (3+3=6) := by⊢ 2 + 2 = 4 ∧ 3 + 3 = 6
  constructorleft⊢ 2 + 2 = 4right⊢ 3 + 3 = 6
  .left⊢ 2 + 2 = 4 norm_numAll goals completed! 🐙
  norm_numAll goals completed! 🐙

Диз'юнкція

example {X Y: Prop} (hX: X) : X ∨ Y := byX:PropY:ProphX:X⊢ X ∨ Y
  lefthX:PropY:ProphX:X⊢ X
  exact hXAll goals completed! 🐙

example {X Y: Prop} (hY: Y) : X ∨ Y := byX:PropY:ProphY:Y⊢ X ∨ Y
  righthX:PropY:ProphY:Y⊢ Y
  exact hYAll goals completed! 🐙

example {X Y: Prop} (hX: ¬ X) (hY: ¬ Y) : ¬ (X ∨ Y) := byX:PropY:ProphX:¬XhY:¬Y⊢ ¬(X ∨ Y)
  simpX:PropY:ProphX:¬XhY:¬Y⊢ ¬X ∧ ¬Y
  constructorleftX:PropY:ProphX:¬XhY:¬Y⊢ ¬XrightX:PropY:ProphX:¬XhY:¬Y⊢ ¬Y
  .leftX:PropY:ProphX:¬XhY:¬Y⊢ ¬X exact hXAll goals completed! 🐙
  exact hYAll goals completed! 🐙

example : (2+2=4) ∨ (3+3=5) := by⊢ 2 + 2 = 4 ∨ 3 + 3 = 5
  lefth⊢ 2 + 2 = 4
  norm_numAll goals completed! 🐙

example : ¬ ((2+2=5) ∨ (3+3=5)) := by⊢ ¬(2 + 2 = 5 ∨ 3 + 3 = 5)
  simpAll goals completed! 🐙

example : (2+2=4) ∨ (3+3=6) := by⊢ 2 + 2 = 4 ∨ 3 + 3 = 6
  lefth⊢ 2 + 2 = 4
  norm_numAll goals completed! 🐙

example : (2+2=4) ∧ (3+3=6) := by⊢ 2 + 2 = 4 ∧ 3 + 3 = 6
  constructorleft⊢ 2 + 2 = 4right⊢ 3 + 3 = 6
  .left⊢ 2 + 2 = 4 norm_numAll goals completed! 🐙
  norm_numAll goals completed! 🐙

example : (2+2=4) ∨ (2353 + 5931 = 7284) := by⊢ 2 + 2 = 4 ∨ 2353 + 5931 = 7284
  lefth⊢ 2 + 2 = 4
  norm_numAll goals completed! 🐙

Xor' (a b : Prop) : Prop#check Xor'

Xor' (a b : Prop) : Prop

Заперечення

example {X:Prop} : (¬ X = true) ↔ (X = false) := byX:Prop⊢ ¬X = (true = true) ↔ X = (false = true) simpAll goals completed! 🐙

example {X:Prop} : (¬ X = false) ↔ (X = true) := byX:Prop⊢ ¬X = (false = true) ↔ X = (true = true) simpAll goals completed! 🐙

example : ¬ (2+2=5) := by⊢ ¬2 + 2 = 5 simpAll goals completed! 🐙example : 2+2 ≠ 5 := by⊢ 2 + 2 ≠ 5 simpAll goals completed! 🐙

example (Jane_black_hair Jane_blue_eyes:Prop) :
  (¬ (Jane_black_hair ∧ Jane_blue_eyes)) ↔ (¬ Jane_black_hair ∨  ¬ Jane_blue_eyes) := byJane_black_hair:PropJane_blue_eyes:Prop⊢ ¬(Jane_black_hair ∧ Jane_blue_eyes) ↔ ¬Jane_black_hair ∨ ¬Jane_blue_eyes
  simpJane_black_hair:PropJane_blue_eyes:Prop⊢ Jane_black_hair → ¬Jane_blue_eyes ↔ ¬Jane_black_hair ∨ ¬Jane_blue_eyes; tautoAll goals completed! 🐙

example (x:ℤ) : ¬ (Even x ∧ x ≥ 0) ↔ (Odd x ∨ x < 0) := byx:ℤ⊢ ¬(Even x ∧ x ≥ 0) ↔ Odd x ∨ x < 0
  have : ¬ Odd x ↔ Even x := Int.not_odd_iff_evenx:ℤthis:¬Odd x ↔ Even x⊢ ¬(Even x ∧ x ≥ 0) ↔ Odd x ∨ x < 0
  have : ¬ (x ≥ 0) ↔ x < 0 := Int.not_lex:ℤthis✝:¬Odd x ↔ Even xthis:¬x ≥ 0 ↔ x < 0⊢ ¬(Even x ∧ x ≥ 0) ↔ Odd x ∨ x < 0
  tautoAll goals completed! 🐙

example (x:ℤ) : ¬ (x ≥ 2 ∧ x ≤ 6) ↔ (x < 2 ∨ x > 6) := byx:ℤ⊢ ¬(x ≥ 2 ∧ x ≤ 6) ↔ x < 2 ∨ x > 6
  have : ¬ (x ≥ 2) ↔ (x < 2) := Int.not_lex:ℤthis:¬x ≥ 2 ↔ x < 2⊢ ¬(x ≥ 2 ∧ x ≤ 6) ↔ x < 2 ∨ x > 6
  have : ¬ (x ≤ 6) ↔ (x > 6) := Int.not_lex:ℤthis✝:¬x ≥ 2 ↔ x < 2this:¬x ≤ 6 ↔ x > 6⊢ ¬(x ≥ 2 ∧ x ≤ 6) ↔ x < 2 ∨ x > 6
  tautoAll goals completed! 🐙

example (John_brown_hair John_black_hair:Prop) :
  (¬ (John_brown_hair ∨ John_black_hair)) ↔ (¬ John_brown_hair ∧  ¬ John_black_hair) := byJohn_brown_hair:PropJohn_black_hair:Prop⊢ ¬(John_brown_hair ∨ John_black_hair) ↔ ¬John_brown_hair ∧ ¬John_black_hair
  simpAll goals completed! 🐙

example (x:ℝ) : ¬ (x ≥ 1 ∧ x ≤ -1) ↔ (x < 1 ∨ x > -1) := byx:ℝ⊢ ¬(x ≥ 1 ∧ x ≤ -1) ↔ x < 1 ∨ x > -1
  have : ¬ (x ≥ 1) ↔ (x < 1) := not_lex:ℝthis:¬x ≥ 1 ↔ x < 1⊢ ¬(x ≥ 1 ∧ x ≤ -1) ↔ x < 1 ∨ x > -1
  have : ¬ (x ≤ -1) ↔ (x > -1) := not_lex:ℝthis✝:¬x ≥ 1 ↔ x < 1this:¬x ≤ -1 ↔ x > -1⊢ ¬(x ≥ 1 ∧ x ≤ -1) ↔ x < 1 ∨ x > -1
  tautoAll goals completed! 🐙

example (x:ℤ) : ¬ (Even x ∨ Odd x) ↔ (¬ Even x ∧ ¬ Odd x) := byx:ℤ⊢ ¬(Even x ∨ Odd x) ↔ ¬Even x ∧ ¬Odd x
  tautoAll goals completed! 🐙

example (X:Prop) : ¬ (¬ X) ↔ X := byX:Prop⊢ ¬¬X ↔ X
  simpAll goals completed! 🐙

Тоді і тільки тоді (iff)

example {X Y: Prop} (hXY: X ↔ Y) (hX: X) : Y := byX:PropY:ProphXY:X ↔ YhX:X⊢ Y
  rw [hXY] at hXX:PropY:ProphXY:X ↔ YhX:Y⊢ Y
  exact hXAll goals completed! 🐙

example {X Y: Prop} (hXY: X ↔ Y) (hY: Y) : X := byX:PropY:ProphXY:X ↔ YhY:Y⊢ X
  rw [←hXY] at hYX:PropY:ProphXY:X ↔ YhY:X⊢ X
  exact hYAll goals completed! 🐙

example {X Y: Prop} (hXY: X ↔ Y) (hX: X) : Y := byX:PropY:ProphXY:X ↔ YhX:X⊢ Y
  exact hXY.mp hXAll goals completed! 🐙

example {X Y: Prop} (hXY: X ↔ Y) (hY: Y) : X := byX:PropY:ProphXY:X ↔ YhY:Y⊢ X
  exact hXY.mpr hYAll goals completed! 🐙

example {X Y: Prop} (hXY: X ↔ Y) : X=Y := byX:PropY:ProphXY:X ↔ Y⊢ X = Y
  simp [hXY]All goals completed! 🐙

example (x:ℝ) : x = 3 ↔ 2 * x = 6 := byx:ℝ⊢ x = 3 ↔ 2 * x = 6
  constructormpx:ℝ⊢ x = 3 → 2 * x = 6mprx:ℝ⊢ 2 * x = 6 → x = 3
  .mpx:ℝ⊢ x = 3 → 2 * x = 6 intro hmpx:ℝh:x = 3⊢ 2 * x = 6
    linarithAll goals completed! 🐙
  intro hmprx:ℝh:2 * x = 6⊢ x = 3
  linarithAll goals completed! 🐙

example : ¬ (∀ x:ℝ, x = 3 ↔ x^2 = 9) := by⊢ ¬∀ (x : ℝ), x = 3 ↔ x ^ 2 = 9
  simp⊢ ∃ x, ¬(x = 3 ↔ x ^ 2 = 9)
  use -3h⊢ ¬(-3 = 3 ↔ (-3) ^ 2 = 9)
  norm_castAll goals completed! 🐙

example {X Y: Prop} (hXY: X ↔ Y) (hX: ¬ X) : ¬ Y := byX:PropY:ProphXY:X ↔ YhX:¬X⊢ ¬Y
  by_contra thisX:PropY:ProphXY:X ↔ YhX:¬Xthis:Y⊢ False
  rw [←hXY] at thisX:PropY:ProphXY:X ↔ YhX:¬Xthis:X⊢ False
  contradictionAll goals completed! 🐙

example : (2+2=5) ↔ (4+4=10) := by⊢ 2 + 2 = 5 ↔ 4 + 4 = 10
  simpAll goals completed! 🐙

example {X Y Z:Prop} (hXY: X ↔ Y) (hXZ: X ↔ Z) : [X,Y,Z].TFAE := byX:PropY:PropZ:ProphXY:X ↔ YhXZ:X ↔ Z⊢ [X, Y, Z].TFAE
  tfae_have 1 ↔ 2 := byX:PropY:PropZ:ProphXY:X ↔ YhXZ:X ↔ Z⊢ [X, Y, Z].TFAE exact hXYAll goals completed! 🐙  -- Цей рядок необов'язковий
  tfae_have 1 ↔ 3 := byX:PropY:PropZ:ProphXY:X ↔ YhXZ:X ↔ Z⊢ [X, Y, Z].TFAE exact hXZAll goals completed! 🐙  -- Цей рядок необов'язковий
  tfae_finishAll goals completed! 🐙

Зверніть увагу, що для методу invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant ?m.62224.out індексація починається з 0, на відміну від тактики unknown identifier 'tfae_have'tfae_have.

example {X Y Z:Prop} (h: [X,Y,Z].TFAE) : X ↔ Y := byX:PropY:PropZ:Proph:[X, Y, Z].TFAE⊢ X ↔ Y
  exact h.out 0 1All goals completed! 🐙

Вправа A.1.1. Заповніть перше sorry : ?m.62233sorry чимось прийнятним

declaration uses 'sorry'example {X Y:Prop} : ¬ ((X ∨ Y) ∧ ¬ (X ∧ Y)) ↔ sorry := byX:PropY:Prop⊢ ¬((X ∨ Y) ∧ ¬(X ∧ Y)) ↔ sorry sorryAll goals completed! 🐙

Вправа A.1.2. Заповніть перше sorry : ?m.62238sorry чимось прийнятним

declaration uses 'sorry'example {X Y:Prop} : ¬ (X ↔ Y) ↔ sorry := byX:PropY:Prop⊢ ¬(X ↔ Y) ↔ sorry sorryAll goals completed! 🐙

Вправа A.1.3.

def declaration uses 'sorry'Exercise_A_1_3 : Decidable (∀ (X Y: Prop), (X → Y) → (¬X → ¬ Y) → (X ↔ Y)) := by⊢ Decidable (∀ (X Y : Prop), (X → Y) → (¬X → ¬Y) → (X ↔ Y))
  -- перший рядок цієї конструкції має бути або `apply isTrue`, або `apply isFalse`, залежно від того, чи вважаєте ви дане твердження істинним чи хибним.
  sorryAll goals completed! 🐙

Вправа A.1.4.

def declaration uses 'sorry'Exercise_A_1_4 : Decidable (∀ (X Y: Prop), (X → Y) → (¬Y → ¬ X) → (X ↔ Y)) := by⊢ Decidable (∀ (X Y : Prop), (X → Y) → (¬Y → ¬X) → (X ↔ Y))
  -- перший рядок цієї конструкції має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll goals completed! 🐙

Вправа A.1.5.

def declaration uses 'sorry'Exercise_A_1_5 : Decidable (∀ (X Y Z: Prop), (X ↔ Y) → (Y ↔ Z) → [X,Y,Z].TFAE) := by⊢ Decidable (∀ (X Y Z : Prop), (X ↔ Y) → (Y ↔ Z) → [X, Y, Z].TFAE)
  -- перший рядок цієї конструкції має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll goals completed! 🐙

Вправа A.1.6.

def declaration uses 'sorry'Exercise_A_1_6 : Decidable (∀ (X Y Z: Prop), (X → Y) → (Y → Z) → (Z → X) → [X,Y,Z].TFAE) := by⊢ Decidable (∀ (X Y Z : Prop), (X → Y) → (Y → Z) → (Z → X) → [X, Y, Z].TFAE)
  -- перший рядок цієї конструкції має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll goals completed! 🐙