Lean

lean.lean

#check true

constant m : nat

#check m

#check nat
#check Type 0
#check Type 100

#reduce 2+3
#eval 2+3

def foo : (nat -> nat) -> nat := λ f, f 0
#check foo

def foo' (f : nat -> nat) : nat := f 0
#check foo'

def compose (α β γ : Type) (g : β -> γ) (f : α -> β) (x : α) : γ := g (f x)

section useful
  variables α β γ : Type
  variable g : β -> γ
  variable f : α -> β

  def compose1 (x : α) : γ := g (f x)

  variables a b c : ℕ
  variables x y z : ℤ
  #check ↑a + x
end useful

#check compose1

namespace listpi
  universe u
  constant list : Type u -> Type u

  constant cons : Π (α : Type u), α -> list α -> list α
  constant nil  : Π (α : Type u), list α
  constant head : Π (α : Type u), list α -> α
  constant tail : Π (α : Type u), list α -> list α
  constant app  : Π (α : Type u), list α -> list α -> list α
end listpi

#check listpi.cons

namespace propositional
  constant and' : Prop -> Prop -> Prop
  constant or' : Prop -> Prop -> Prop
  constant not' : Prop -> Prop
  constant implies' : Prop -> Prop -> Prop

  variables p q r : Prop

  #check and' p q
end propositional


theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp
#check t1

section
  variables p q : Prop

  example (hp : p) (hq : q) : p ∧ q := and.intro hp hq
  example (h : p ∧ q) : p := and.elim_left h
  example (h : p ∧ q) : q := and.elim_right h

  example (hp : p) (hq : q) : p ∧ q := ⟨ hp, hq ⟩
  example (h : p ∧ q) : p := and.left h
  example (h : p ∧ q) : q := and.right h

  example (hp : p) : p ∨ q := or.intro_left q hp
  example (hq : q) : p ∨ q := or.intro_right p hq
  example (h : p ∨ q) : q ∨ p :=
    or.elim h (λ hp, or.inr hp) (assume hq, or.inl hq)

  example (hpq : p → q) (hnq : ¬q) : ¬p :=
    assume hp : p, show false,
    from hnq (hpq hp)

  example (hp : p) (hnp : ¬p) : q :=
    false.elim (hnp hp)

  example (h : p ∧ q) : q ∧ p :=
    have hp : p, from and.left h,
    suffices hq : q, from and.intro hq hp,
    show q, from and.right h

  #check classical.em
  #check classical.by_cases
  #check classical.by_contradiction
end


section
  variables (α : Type) (p q : α → Prop)

  example (h : ∀ x : α, p x ∧ q x) : (∀ y : α, q y) :=
    assume y : α,
    show q y,
    from (h y).right
end

section
  #check @eq.refl
  #check @eq.symm
  #check @eq.trans
  #check @eq.subst

  open eq

  variables (α : Type) (a b c d : α)
  variables (hab : a = b) (hcb : c = b) (hcd : c = d)

  example : (a = d) :=
    trans (trans hab (symm hcb)) hcd

  example : (2 + 3 = 5) :=
    refl _

  #check congr_arg
  #check congr_fun
  #check congr

  #check ℕ
  #check ℤ
end

section
  variables (a b c d e : ℕ)
  variable h₁ : a = b
  variable h₂ : b = c + 1
  variable h₃ : c = d
  variable h₄ : e = 1 + d

  include h₁ h₂ h₃ h₄
  example : (a = e) :=
    calc
      a = b : by rw h₁
      ... = c + 1 : by rw h₂
      ... = d + 1 : by rw h₃
      ... = 1 + d : by rw add_comm
      ... = e : by rw h₄

  example (x y : ℕ) :
    (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
  by simp [mul_add]
end

section
  open nat

  #check @exists.intro
  #check @exists.elim

  example : ∃ x : ℕ, x > 0 :=
    have h : 1 > 0, from zero_lt_succ 0,
    exists.intro 1 h

  example : ∃ x : ℕ, x > 0 :=
    have h : 1 > 0, from zero_lt_succ 0,
    ⟨1, h⟩

  variables (α : Type) (p q : α -> Prop)

  example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
    exists.elim h (λ w (hw : p w ∧ q w), ⟨w, hw.right, hw.left⟩)

  example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
    match h with ⟨w, hw⟩ :=
      ⟨w, hw.right, hw.left⟩
    end

  example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
    let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩
end

section
  variable f : ℕ → ℕ
  variable h : ∀ x : ℕ, f x ≤ f (x + 1)

  example : f 0 ≤ f 3 :=
    have h₁ : f 0 ≤ f 1, from h 0,
    have h₂ : f 0 ≤ f 2, from le_trans h₁ (h 1),
    have h₃ : f 0 ≤ f 3, from le_trans h₂ (h 2),
    show f 0 ≤ f 3, from by assumption
end

section
  theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p :=
  begin
    apply and.intro,
      exact hp,
      apply and.intro,
        exact hq,
        exact hp
  end

  example : ∀ a b c : ℕ, a = b → a = c → c = b :=
  begin
    intros a b c h₁ h₂,
    apply eq.trans,
    apply eq.symm,
    assumption,
    assumption
  end

  example : ∀ a b c : ℕ, a = b → a = c → c = b :=
  begin
    intros a b c h₁ h₂,
    rw ← h₁,
    rw ← h₂
  end

  #check @exists.intro

  example : ∃ a : ℕ, 5 = a :=
  begin
    fapply exists.intro,
      exact 5,
      refl
  end

  example (p q : Prop) : p ∨ q → q ∨ p :=
  begin
    intro h,
    cases h with hp hq,
      right, assumption,
      left, assumption
  end

  example (p q : Prop) : p ∧ q → q ∧ p :=
    assume : p ∧ q,
    have p, from ‹p ∧ q›.left,
    have q, from ‹p ∧ q›.right,
    show q ∧ p, from and.intro ‹q› ‹p›

  example (p q : Prop) : p ∧ q → q ∧ p :=
  begin
    intro h,
    cases h with hp hq,
    constructor, repeat { assumption }
  end

  example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
  begin
    constructor,
    { intro h,
      cases h with hp hpr,
      cases hpr with hp hr,
      { left, constructor, repeat { assumption }, },
      { right, constructor, repeat { assumption }, },
    },
    { intro h,
      cases h with hpq hpr,
      { cases hpq with hp hq, constructor, assumption, left, assumption },
      { cases hpr with hp hr, constructor, assumption, right, assumption },
    }
  end
end

section
  open nat

  example (P : ℕ → Prop) (h₀ : P 0) (h₁ : ∀ n, P (succ n)) (m : ℕ) : P m :=
  begin
    cases m with m',
      assumption,
      apply h₁
  end

  example (n : ℕ) : n + 1 = succ n :=
  begin
    refl
  end

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

section
  meta def my_tac : tactic unit :=
  `[ repeat { {left, assumption} <|> right <|> assumption } ]

  example (p q r : Prop) (hp : p) : p ∨ q ∨ r :=
  by my_tac

  example (p q r : Prop) (hq : q) : p ∨ q ∨ r :=
  by my_tac

  example (p q r : Prop) (hr : r) : p ∨ q ∨ r :=
  by my_tac
end

section
  variables (x y z w : ℕ) (p : ℕ → Prop)

  example : (x + 0) * (0 + y * 1 + z * 0) = x * y :=
  by simp

  example (h : p (x * y + z * w * x)) : p (x * w * z + y * x) :=
  begin
    simp,
    simp at h,
    assumption
  end
end

section
  parameters {α : Type} (r : α -> α -> Type)
  parameters transr : ∀ {x y z}, r x y → r y z → r x z

  variables {a b c d e : α}

  theorem th1 (h₁ : r a b) (h₂ : r b c) (h₃ : r c d) : r a d :=
    transr h₁ (transr h₂ h₃)

  #check th1
end
#check th1

namespace abc
  variables {α : Type} (r : α → α → Prop)

  definition reflexive  : Prop := ∀ (a : α), r a a
  definition symmetric  : Prop := ∀ ⦃a b : α⦄, r a b → r b a
  definition transitive : Prop := ∀ ⦃a b c : α⦄, r a b → r b c → r a c
  definition euclidean  : Prop := ∀ ⦃a b c : α⦄, r a b → r a c → r b c

  variable {r}

  theorem th1 (reflr : reflexive r) (euclr : euclidean r) : symmetric r :=
    assume a b : α, assume : r a b,
    show r b a, from euclr this (reflr _)

  theorem th2 (symmr : symmetric r) (euclr : euclidean r) : transitive r :=
    assume (a b c : α), assume (rab : r a b) (rbc : r b c),
    euclr (symmr rab) rbc

  theorem th3 (reflr : reflexive r) (euclr : euclidean r) : transitive r :=
    th2 (th1 reflr euclr) euclr
end abc

#print abc.th3
#print options

namespace abc
  inductive weekday : Type
  | sunday
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday

  #check weekday.sunday
  #check @weekday.rec_on

  namespace weekday
    def number_of_day (d : weekday) : ℕ :=
      weekday.cases_on d 1 2 3 4 5 6 7

    def next (d : weekday) : weekday :=
      weekday.cases_on d monday tuesday wednesday thursday friday saturday sunday

    def previous (d : weekday) : weekday :=
      weekday.cases_on d saturday sunday monday tuesday wednesday thursday friday

    theorem next_previous (d : weekday) : next (previous d) = d :=
    by { cases d; refl }

    theorem next_previous1 (d : weekday) : next (previous d) = d :=
      weekday.cases_on d rfl rfl rfl rfl rfl rfl rfl
  end weekday
end abc

namespace hide
  inductive prod (α : Type) (β : Type)
  | mk : α → β → prod

  inductive sum (α : Type) (β : Type)
  | inl {} : α → sum
  | inr {} : β → sum

  #check @prod.rec_on
  #check @prod.cases_on
  #check @sum.rec_on

  def fst {α : Type} {β : Type} (p : prod α β) : α :=
    prod.cases_on p (λ a b, a)

  def snd {α : Type} {β : Type} (p : prod α β) : β :=
    prod.cases_on p (λ a b, b)

  def sum_example (s : sum ℕ ℕ) : ℕ :=
    sum.cases_on s (λ n, 2 * n) (λ n, 2 * n + 1)

  structure color := (red : ℕ) (green : ℕ) (blue : ℕ)
  def yellow := color.mk 255 255 0

  structure semigroup :=
    (carrier : Type)
    (mul : carrier → carrier → carrier)
    (mul_assoc : ∀ a b c : carrier, mul (mul a b) c = mul a (mul b c))

  inductive sigma {α : Type} {β : α → Type}
  | dpair : Π (a : α), β a → sigma

  inductive nat : Type
  | zero : nat
  | succ : nat → nat

  #check @nat.rec_on
  #check @nat.cases_on

  def add (m n : nat) : nat := nat.rec_on n m (λ n accum, nat.succ accum)

  #reduce add (nat.succ nat.zero) (nat.succ (nat.succ nat.zero))

  example (n : nat) : add nat.zero n = n :=
  begin
    apply (nat.rec_on n),
    { refl },
    { intros a h,
      have h₁ : add nat.zero (nat.succ a) = nat.succ (add nat.zero a),
      from rfl,
      rw [h₁, h]
    }
  end

  inductive list (α : Type)
  | nil {} : list
  | cons : α → list → list

  #check list.nil
  #check list.cons

  inductive vector (α : Type) : nat → Type
  | nil {} : vector nat.zero
  | cons {n : nat} (a : α) (v : vector n) : vector (nat.succ n)

  inductive eq {α : Type} (a : α) : α → Prop
  | refl : eq a

  #check list
  #check vector
  #check eq

  inductive tree₁ (α : Type) : Type
  | mk : α → list tree₁ → tree₁

  mutual inductive tree₂, list_tree₂ (α : Type)
  with tree₂ : Type
       | mk : α → list_tree₂ → tree₂
  with list_tree₂ : Type
       | nil {} : list_tree₂
       | cons : tree₂ → list_tree₂ → list_tree₂
end hide

section struct
  structure point (α : Type) :=
  mk :: (x : α) (y : α)

  #check point.rec_on
  #check point.x
  #reduce point.x (point.mk 10 100)
  #reduce point.y { point . x := 10, y := 100}

  structure point₁ :=
  mk :: {α : Type} {β : Type} (a : α) (b : β)
  #check { point₁ . a := 10, b := true}
end struct

namespace hide
  class inhabited (α : Type) := (value : α)

  instance Prop_inhabited : inhabited Prop := inhabited.mk true
  instance bool_inhabited : inhabited bool := inhabited.mk tt
  instance nat_inhabited : inhabited ℕ := inhabited.mk 0
  instance unit_inhabited : inhabited unit := ⟨()⟩
  instance prod_inhabited {α β : Type} [inhabited α] [inhabited β] : inhabited (prod α β) :=
    ⟨⟨inhabited.value α, inhabited.value β⟩⟩

  def default (α : Type) [s : inhabited α] : α := inhabited.value α
  #eval (default ℕ)

  class inductive decidable (p : Prop) : Type
  | is_false : ¬p → decidable
  | is_true : p → decidable
  #print and.decidable

  class has_add (α : Type) := (add : α → α → α)
  def add₁ {α : Type} [has_add α] : α → α → α := has_add.add
  local notation a `+` b := add₁ a b

  instance nat_has_add : has_add ℕ := ⟨nat.add⟩
  #check 2+2

  instance prod_has_add {α : Type} {β : Type} [has_add α] [has_add β] : has_add (prod α β) :=
    ⟨λ ⟨a₁, b₁⟩ ⟨a₂, b₂⟩, ⟨a₁+a₂, b₁+b₂⟩⟩

  #reduce prod.mk 1 2 + prod.mk 2 3

  #print classes
  #print instances inhabited
end hide

section hide
  def tail₁ {α : Type} : list α → list α
  | [] := []
  | (h :: t) := t

  def tail₂ : Π {α : Type}, list α → list α
  | α [] := []
  | α (h :: t) := t

  def tail₃ {α : Type} : list α → list α := λ l,
  match l with
  | [] := []
  | (h :: t) := t
  end
end hide

namespace hide
  open classical
  local attribute [instance] prop_decidable

  noncomputable def choose (p : ℕ → Prop) : ℕ :=
    if h : (∃ n : ℕ, p n) then classical.some h else 0

  variable p : ℕ → Prop
  variable h : (∃ n : ℕ, p n)
  #check classical.some
  #check classical.some h
end hide

namespace monad
  def nth {α : Type} : list α → ℕ → option α
  | [] n := none
  | (a :: l) 0 := some a
  | (a :: l) (n+1) := nth l n

  def foo (l₁ l₂ l₃ : list ℕ) : option (list ℕ) :=
  do v₁ ← nth l₁ 0,
     v₂ ← nth l₂ 1,
     v₃ ← nth l₃ 2,
     return [v₁, v₂, v₃]

  #eval foo [1,2,3] [1,2,3] [1,2,4]
  #eval foo [1,2,3] [1,2,3] [1,2]
end monad