Analysis I, Appendix A.2: Implication

An introduction to implications. Showcases some basic tactics and Lean syntax.

example {X Y: Prop} (hX: X) : (X → Y) ↔ Y := byX:PropY:ProphX:X⊢ X → Y ↔ Y tautoAll goals completed! 🐙

example {X Y: Prop} (hX: ¬X) : X → Y := byX:PropY:ProphX:¬X⊢ X → Y
  intro hX'X:PropY:ProphX:¬XhX':X⊢ Y
  contradictionAll goals completed! 🐙

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

example {X Y: Prop} (hXY: X → Y) (hX: X) : Y := hXY hX

example {X Y: Prop} (hXY: X → Y) (hY: ¬ Y) : ¬ X := byX:PropY:ProphXY:X → YhY:¬Y⊢ ¬X
  contrapose! hYX:PropY:ProphXY:X → YhY:X⊢ Y
  exact hXY hYAll goals completed! 🐙

theorem example_A_2_1 (x:ℤ) : x = 2 → x^2 = 4 := byx:ℤ⊢ x = 2 → x ^ 2 = 4
  intro hx:ℤh:x = 2⊢ x ^ 2 = 4
  rw [h]x:ℤh:x = 2⊢ 2 ^ 2 = 4
  rflAll goals completed! 🐙

example : (2:ℤ) = 2 → (2:ℤ)^2 = 4 := example_A_2_1 2example : (3:ℤ) = 2 → (3:ℤ)^2 = 4 := example_A_2_1 3example : (-2:ℤ) = 2 → (-2:ℤ)^2 = 4 := example_A_2_1 (-2)_root_.not_imp {a b : Prop} : ¬(a → b) ↔ a ∧ ¬b#check _root_.not_imp

_root_.not_imp {a b : Prop} : ¬(a → b) ↔ a ∧ ¬b

example : ¬ ((2+2=4) → (4+4)=2) := by⊢ ¬(2 + 2 = 4 → 4 + 4 = 2)
  rw [Classical.not_imp]⊢ 2 + 2 = 4 ∧ ¬4 + 4 = 2
  constructorleft⊢ 2 + 2 = 4right⊢ ¬4 + 4 = 2
  .left⊢ 2 + 2 = 4 norm_numAll goals completed! 🐙
  norm_numAll goals completed! 🐙

example {X Y: Prop} : (X → Y) ↔ (Y ≥ X) := byX:PropY:Prop⊢ X → Y ↔ Y ≥ X simpAll goals completed! 🐙

example {X Y: Prop} : (X → Y) ↔ ((¬X) ≥ ¬Y) := byX:PropY:Prop⊢ X → Y ↔ (¬X) ≥ ¬Y simpX:PropY:Prop⊢ X → Y ↔ ¬Y → ¬X; tautoAll goals completed! 🐙

example {John_left_at_five John_here_now:Prop}
  (h1: John_left_at_five → John_here_now)
  (h2: ¬ John_here_now) :
  ¬ John_left_at_five := byJohn_left_at_five:PropJohn_here_now:Proph1:John_left_at_five → John_here_nowh2:¬John_here_now⊢ ¬John_left_at_five
  contrapose! h2John_left_at_five:PropJohn_here_now:Proph1:John_left_at_five → John_here_nowh2:John_left_at_five⊢ John_here_now
  exact h1 h2All goals completed! 🐙

example {Washington_capital_US:Prop} (h: Washington_capital_US) : (1+1=2) → Washington_capital_US := byWashington_capital_US:Proph:Washington_capital_US⊢ 1 + 1 = 2 → Washington_capital_US
  intro h'Washington_capital_US:Proph:Washington_capital_USh':1 + 1 = 2⊢ Washington_capital_US
  exact hAll goals completed! 🐙

example {NYC_capital_US:Prop} : (2+2=3) → NYC_capital_US := byNYC_capital_US:Prop⊢ 2 + 2 = 3 → NYC_capital_US
  intro hNYC_capital_US:Proph:2 + 2 = 3⊢ NYC_capital_US
  simp at hAll goals completed! 🐙

/-- Proposition A.2.2 -/
example : ((2+2:ℤ)=5) → (4=(10-4:ℤ)) := by⊢ 2 + 2 = 5 → 4 = 10 - 4
  intro hh:2 + 2 = 5⊢ 4 = 10 - 4
  have : (4 + 4:ℤ) = 10 := by⊢ 2 + 2 = 5 → 4 = 10 - 4
    replace h := congr(2*$h)h:2 * (2 + 2) = 2 * 5⊢ 4 + 4 = 10
    convert h using 1All goals completed! 🐙
  rwa [←eq_sub_iff_add_eq]h:2 + 2 = 5this:4 = 10 - 4⊢ 4 = 10 - 4 at this

Theorem A.2.4

theorem theorem_A_2_4 (n:ℤ) : Even (n * (n+1)) := byn:ℤ⊢ Even (n * (n + 1))
  have : Even n ∨ Odd n := Int.even_or_odd nn:ℤthis:Even n ∨ Odd n⊢ Even (n * (n + 1))
  obtain heven | hodd := thisinln:ℤheven:Even n⊢ Even (n * (n + 1))inrn:ℤhodd:Odd n⊢ Even (n * (n + 1))  -- can also use `rcases this with heven | hodd`
  .inln:ℤheven:Even n⊢ Even (n * (n + 1)) exact Even.mul_right heven _All goals completed! 🐙
  have : Even (n+1) := Odd.add_one hoddinrn:ℤhodd:Odd nthis:Even (n + 1)⊢ Even (n * (n + 1))
  exact Even.mul_left this _All goals completed! 🐙

              /-- Corollary A.2.5 -/
example :
  let n:ℤ := (253+142)*123-(423+198)^342+538-213
  Even (n * (n+1)) := theorem_A_2_4 _example : ∀ x:ℝ, x = 2 → x^2 = 4 := by⊢ ∀ (x : ℝ), x = 2 → x ^ 2 = 4
  intro x hx:ℝh:x = 2⊢ x ^ 2 = 4
  simp [h]x:ℝh:x = 2⊢ 2 ^ 2 = 4
  norm_numAll goals completed! 🐙example : ¬ ∀ x:ℝ, x^2 = 4 → x = 2 := by⊢ ¬∀ (x : ℝ), x ^ 2 = 4 → x = 2
  simp⊢ ∃ x, x ^ 2 = 4 ∧ ¬x = 2
  use -2h⊢ (-2) ^ 2 = 4 ∧ ¬-2 = 2
  norm_castAll goals completed! 🐙example {X Y : Prop} : (X ↔ Y) = ((X → Y) ∧ (Y → X)) := byX:PropY:Prop⊢ (X ↔ Y) = ((X → Y) ∧ (Y → X))
  simpX:PropY:Prop⊢ (X ↔ Y) ↔ (X → Y) ∧ (Y → X); tautoAll goals completed! 🐙example (x:ℝ) : x = 2 ↔ 2*x = 4 := byx:ℝ⊢ x = 2 ↔ 2 * x = 4
  constructormpx:ℝ⊢ x = 2 → 2 * x = 4mprx:ℝ⊢ 2 * x = 4 → x = 2
  .mpx:ℝ⊢ x = 2 → 2 * x = 4 intro hmpx:ℝh:x = 2⊢ 2 * x = 4
    linarithAll goals completed! 🐙
  intro hmprx:ℝh:2 * x = 4⊢ x = 2
  linarithAll goals completed! 🐙example {X Y :Prop} : (X ↔ Y) = (X = Y) := byX:PropY:Prop⊢ (X ↔ Y) = (X = Y) simpAll goals completed! 🐙example : (3 = 2) → (6 = 4) := by⊢ 3 = 2 → 6 = 4 simpAll goals completed! 🐙example : ∃ (X Y:Prop), (X → Y) ≠ (Y → X) := by⊢ ∃ X Y, (X → Y) ≠ (Y → X)
  set x := -2x:ℤ := -2⊢ ∃ X Y, (X → Y) ≠ (Y → X)
  use x = 2, x^2 = 4hx:ℤ := -2⊢ (x = 2 → x ^ 2 = 4) ≠ (x ^ 2 = 4 → x = 2)
  simp [x]All goals completed! 🐙theorem contrapositive {X Y: Prop} (hXY: X → Y) : ¬ Y → ¬ X := byX:PropY:ProphXY:X → Y⊢ ¬Y → ¬X
  intro hYX:PropY:ProphXY:X → YhY:¬Y⊢ ¬X
  by_contra hXX:PropY:ProphXY:X → YhY:¬YhX:X⊢ False
  have := hXY hXX:PropY:ProphXY:X → YhY:¬YhX:Xthis:Y⊢ False
  contradictionAll goals completed! 🐙theorem imp_example (x:ℝ) : (x = 2) → (x^2 = 4) := byx:ℝ⊢ x = 2 → x ^ 2 = 4
  intro hx:ℝh:x = 2⊢ x ^ 2 = 4
  rw [h]x:ℝh:x = 2⊢ 2 ^ 2 = 4
  norm_numAll goals completed! 🐙theorem imp_contrapositive (x:ℝ) : (x^2 ≠ 4) → (x ≠ 2) := byx:ℝ⊢ x ^ 2 ≠ 4 → x ≠ 2
  convert contrapositive (imp_example x)All goals completed! 🐙/-- Proposition A.2.6 -/
example {x:ℝ} (h:x>0) (hsin: Real.sin x = 1) : x ≥ Real.pi / 2 := byx:ℝh:x > 0hsin:Real.sin x = 1⊢ x ≥ Real.pi / 2
  by_contra! h'x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2⊢ False
  have h1 : Real.sin 0 < Real.sin x := byx:ℝh:x > 0hsin:Real.sin x = 1⊢ x ≥ Real.pi / 2
    apply Real.sin_lt_sin_of_lt_of_le_pi_div_two _ _ hx:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2⊢ -(Real.pi / 2) ≤ 0x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2⊢ x ≤ Real.pi / 2
    .x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2⊢ -(Real.pi / 2) ≤ 0 have : Real.pi > 0 := Real.pi_posx:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2this:Real.pi > 0⊢ -(Real.pi / 2) ≤ 0
      linarithAll goals completed! 🐙
    linarithAll goals completed! 🐙
  have h2 : Real.sin x < Real.sin (Real.pi / 2) := byx:ℝh:x > 0hsin:Real.sin x = 1⊢ x ≥ Real.pi / 2
  -- the <;> tactic applies the next tactic to all currently visible goals.
    apply Real.sin_lt_sin_of_lt_of_le_pi_div_two _ _ h'x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2h1:Real.sin 0 < Real.sin x⊢ -(Real.pi / 2) ≤ xx:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2h1:Real.sin 0 < Real.sin x⊢ Real.pi / 2 ≤ Real.pi / 2 <;>x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2h1:Real.sin 0 < Real.sin x⊢ -(Real.pi / 2) ≤ xx:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2h1:Real.sin 0 < Real.sin x⊢ Real.pi / 2 ≤ Real.pi / 2 linarithAll goals completed! 🐙
  simp at h1 h2x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2h1:0 < Real.sin xh2:Real.sin x < 1⊢ False
  linarithAll goals completed! 🐙