Analysis
A.1. Mathematical statements

Imports

import Mathlib.Tactic

Analysis I, Appendix A.1: Mathematical Statements

An introduction to mathematical statements. Showcases some basic tactics and Lean syntax.

/- Example A.1.1. What the textbook calls "statements" are objects of type `Prop` in Lean.  Also,
   in Lean we tend to assign "junk" values to expressions that might normally be considered
   undefined, so discussions regarding undefined terms in the textbook should be adjusted
   accordingly. -/   
2 + 2 = 4 : Prop#check 2+2=4

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

2 + 2 = 5 : Prop

/-- Every well-formed statement is either true or false... -/
example (P:Prop) : (P=true) ∨ (P=false) := byP:Prop⊢ P = (true = true) ∨ P = (false = true) simpP:Prop⊢ P ∨ ¬P; tautoAll goals completed! 🐙

/-- .. but not both. -/
example (P:Prop) : ¬ ((P=true) ∧ (P=false)) := byP:Prop⊢ ¬(P = (true = true) ∧ P = (false = true)) simpAll goals completed! 🐙

-- Note: `P=true` and `P=false` simplify to `P` and `¬P` respectively.

/-- To prove that a statement is true, it suffices to show that it is not false, -/
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! 🐙

/-- while to show that a statement is false, it suffices to show that it is not true. -/
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! 🐙

/-- This statement is true, but unlikely to be very useful. -/
example : 2 = 2 := rfl

/-- This statement is also true, but not very efficient. -/
example : 4 ≤ 4 := by⊢ 4 ≤ 4 norm_numAll goals completed! 🐙

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

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

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

/-- Conjunction -/
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! 🐙

/-- Disjunction -/
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

/-- Negation -/
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! 🐙

/-- If and only if (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! 🐙  -- This line is optional
  tfae_have 1 ↔ 3 := byX:PropY:PropZ:ProphXY:X ↔ YhXZ:X ↔ Z⊢ [X, Y, Z].TFAE exact hXZAll goals completed! 🐙  -- This line is optional
  tfae_finishAll goals completed! 🐙

/-- Note for the {name (full := List.TFAE.out)}`out` method that one indexes starting from 0, in
contrast to the {tactic}`tfae_have` tactic. -/
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! 🐙

/-- Exercise A.1.1.  Fill in the first {syntax term}`sorry` with something reasonable. -/
declaration uses `sorry`example {X Y:Prop} : ¬ ((X ∨ Y) ∧ ¬ (X ∧ Y)) ↔ sorry := byX:PropY:Prop⊢ ¬((X ∨ Y) ∧ ¬(X ∧ Y)) ↔ sorry sorryAll goals completed! 🐙

/-- Exercise A.1.2.  Fill in the first {syntax term}`sorry` with something reasonable. -/
declaration uses `sorry`example {X Y:Prop} : ¬ (X ↔ Y) ↔ sorry := byX:PropY:Prop⊢ ¬(X ↔ Y) ↔ sorry sorryAll goals completed! 🐙

Exercise 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))
  --the first line of this construction should be either `apply isTrue` or `apply isFalse`,
  --depending on whether you believe the given statement to be true or false. 
  sorryAll goals completed! 🐙

Exercise 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))
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

Exercise 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)
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

Exercise 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)
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙