summer_school_lean_examples.lean

import tactic.tauto tactic.finish

section

variables {A B C D : Prop}

example (h1 : A ∨ B) (h2 : ¬ A) : B :=
or.elim h1
  (assume h3 : A, 
    have h4 : false, from h2 h3,
    show B, from false.elim h4)
  (assume h3 : B, 
    show B, from h3)

example (h1 : A ∨ B) (h2 : ¬ A) : B :=
or.elim h1
  (assume h3 : A, 
    show B, from false.elim (h2 h3))
  (assume h3 : B, 
    show B, from h3)

example (h1 : A ∨ B) (h2 : ¬ A) : B :=
or.elim h1
  (assume h3 : A, 
    show B, from absurd h3 h2)
  (assume h3 : B, 
    show B, from h3)

#check @absurd

example (h1 : A ∨ B) (h2 : ¬ A) : B :=
or.elim h1 (λ h3, absurd h3 h2) (λ h3, h3)

theorem my_favorite_theorem (h1 : A ∨ B) (h2 : ¬ A) : B :=
or.elim h1 (λ h3, absurd h3 h2) (λ h3, h3)

#check @my_favorite_theorem

example (h1 : A ∨ B) (h2 : ¬ A) : B :=
my_favorite_theorem h1 h2

open classical

theorem excluded_middle : A ∨ ¬ A :=
by_contradiction 
  (assume h : ¬ (A ∨ ¬ A),
    have h1 : ¬ A, 
      from (assume a : A, h (or.inl a)),
    show false, from h (or.inr h1))

example : A ∨ ¬ A :=
by_contradiction (λ h : ¬ (A ∨ ¬ A), h (or.inr (λ a, h (or.inl a))))

theorem foo : A ∧ B → B ∧ A :=
begin
  intro h,
  cases h with h1 h2,
  split,
  apply h2,
  apply h1
end

example : A ∨ B → B ∨ A :=
begin
  intro h,
  cases h with h1 h2, 
  apply or.inr, apply h1,
  apply or.inl, apply h2
end

example : A ∨ B → B ∨ A :=
begin
  intro h,
  cases h with h1 h2,
  right, assumption,
  left, assumption
end

example (h1 : A ∨ B) (h2 : ¬ A) : B :=
by finish

example (h1 : A ∨ B) (h2 : ¬ A) : B :=
begin
  cases h1 with h1 h1,
  exact absurd h1 h2,
  apply h1
end

example (h1 : A ∨ B) (h2 : ¬ A) : B :=
begin
  exact 
    begin
      exact sorry
    end
end

#print foo

end

section

variables α β γ : Type

#check nat
#check ℕ
#check ℕ → ℕ 
#check α × ℕ → bool

#check 2
#check (2 + 2 : ℕ) 

#check λ x, x + 3

def f : ℕ → ℕ := λ x, x + 3

#check f

#eval f 5

def g (x : ℕ) : ℕ := x + 3

variables A B C : Prop

theorem bar : A → A := λ h, h

theorem bar' (h : A) : A := h

def g' (x : ℕ) := x + 3

#check nat.add
#check nat.mul
#check nat.lt

#eval 5 % 2

def even (x : ℕ) : Prop :=
∃ k : ℕ, x = 2 * k    -- x % 2 = 0

#eval (3 - 6 : ℤ)

#check nat × nat  -- \times 

-- ∀ \all
-- ∃ \ex
-- <
-- ≤

def statement_of_fermats_last_theorem : Prop :=
  ∀ n : nat, n > 2 → ¬ ∃ a b c : nat, 
    a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ 
      a^n + b^n = c^n

#print statement_of_fermats_last_theorem

end

section

variables {α : Type} -- \a
variables A B : α → Prop

example : (∀ x : α, A x ∧ B x) → ∀ x, A x :=
assume h1 : ∀ x, A x ∧ B x,
assume y : α,
have h2 : A y ∧ B y, from h1 y,
show A y, from and.left h2

example : (∀ x : α, A x ∧ B x) → ∀ x, A x :=
assume h1 (y : α),
have h2 : A y ∧ B y, from h1 y,
show A y, from and.left h2

example (h1 : ∀ x : α, A x ∧ B x) (y : α) : A y :=
have h2 : A y ∧ B y, from h1 y,
show A y, from and.left h2

example : (∀ x : α, A x ∧ B x) → ∀ x, A x :=
λ h1 y, (h1 y).left

example (h : ∃ x, A x ∧ B x) : ∃ x, A x :=
exists.elim h
  (assume y h1,
    have h2 : A y, from h1.left,
    exists.intro y h2)

example (h : ∃ x, A x ∧ B x) : ∃ x, A x :=
exists.elim h $
assume (y : α) (h1 : A y ∧ B y),
have h2 : A y, from h1.left,
show ∃ x, A x, from exists.intro y h2

example : (∀ x : α, A x ∧ B x) → ∀ x, A x :=
begin
  intro h,
  intro y,
  have h1 := h y,
  cases h1 with h2 h3,
  exact h2
end

example : (∀ x : α, A x ∧ B x) → ∀ x, A x :=
begin
  intros h y,
  cases (h y),
  assumption
end

example (h : ∃ x, A x ∧ B x) : ∃ x, A x :=
begin
  cases h with y h1,
  cases h1 with h1 h2,
  existsi y,
  assumption
  -- split, exact h1
  -- apply exists.intro y, apply h1,
  -- exact exists.intro y h1
end

section
  variables (f : ℕ → ℕ) (x : ℕ)
  #check f (f x) 
  #check f $ f x
end

end

section

variable α : Type

variables a b c d e : α 
variables (h1 : a = b) (h2 : b = c) (h3 : d = c) 
variables (h4 : c = e)

  #check eq.refl a

  example : a = a := eq.refl _
  example : a = a := rfl

  example : 2 + 2 = 4 := rfl

  #check eq.symm h1
  #check eq.symm h3
  #check eq.trans h1 h2

  example : a = d :=
  eq.trans (eq.trans h1 h2) (eq.symm h3)


example : a = d :=
calc
  a = b : h1
  ... = c : h2 
  ... = d : h3.symm   -- eq.symm h3

include h1 h2 h3 h4

example : a = d :=
begin
  rw h1, rw h2, rw h3.symm
end

example : a = d :=
by rw [h1, h2, h3]

example : a = d :=
by simp [h1, h2, h3]

example : a = d :=
by simp *

end

inductive Nat 
| zero : Nat
| succ : Nat → Nat

#check Nat
#check Nat.zero
#check Nat.succ
#check @Nat.rec

namespace Nat

--instance : has_zero Nat := ⟨zero⟩

def add : Nat → Nat → Nat 
| x zero        := x
| x (succ y) := succ (add x y)

--instance : has_add Nat := ⟨add⟩

def mul : Nat → Nat → Nat 
| x zero := zero
| x (succ y) := add (mul x y) x

-- instance : has_mul Nat := ⟨mul⟩ 

lemma zero_add (x : Nat) : add zero x = x :=
begin
  induction x with x ih, 
  rw [add],
  rw [add, ih]
end

lemma succ_add (x y : Nat) : succ (add y x) = add (succ y) x :=
begin
  induction x with x ih,
  rw [add, add],
  rw [add, add, ih]
end

theorem add_comm (x y : Nat) : add x y = add y x :=
begin
  induction y with y ih,
  rw [add, zero_add],
  rw [add, ih, succ_add]
end

end Nat