ss20_lecture.lean

import tactic
open_locale classical

#check 2
#check 2 + 2

#check 2 + 2 = 4

#check (2.05 : real)

#check ℕ    -- \nat
#check nat

theorem foo : 2 + 2 = 4 := rfl

#check foo

variables p q r : Prop

#check p

#check p ∧ q   -- \and
#check p /\ q
#check and p q
#check p → q  -- \to \implies \r
#check p ∨ q
#check ¬ p

example : p → p :=
begin
  intro h,
  apply h
end

example : p → (q → p) :=
begin
  intro h,
  intro h1,
  apply h
end

example : (p ∧ q) → (q ∧ p) :=
begin
  intro h,
  cases h with hp hq,
  split,
  apply hq,
  apply hp
end

example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) :=
begin
  intro h,
  cases h with h1 h2,
  cases h2 with h3 h3,
  left,
  split,
  assumption,
  assumption,
  right,
  split,
  assumption,
  assumption
end

#check ¬ p
#check false
#check p → false

-- ex falso sequitur quodlibet
-- exfalso

example : p ∧ (p → q) → q :=
begin
  intro h,
  cases h with h1 h2,
  apply h2,
  apply h1
end

example : p ∧ ¬ p → q :=
begin
  intro h,
  cases h with h1 h2,
  exfalso,
  apply h2,
  apply h1
end

example : ¬ ¬ p → p :=
begin
  intro h,
  by_contradiction h1,
  apply h,
  apply h1
end

example : ¬ ¬ p → p :=
begin
  intro h,
  --by_cases h1 : p, -- excluded middle
  cases (classical.em p) with h1 h1,
  apply h1,
  exfalso,
  apply h,
  apply h1
end

example : ¬ (p ↔ ¬ p) :=
begin

end

theorem fermats_last_theorem : ∀ x y z n : ℕ,
  x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 ∧ n > 2 → x^n + y^n ≠ z^n :=
begin

end