Tipos inductivos Lean

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

#check weekday.sunday   -- weekday
#check weekday.monday   -- weekday

open weekday

#check sunday   -- weekday
#check monday   -- weekday

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

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

#reduce number_of_day weekday.sunday   -- 1
#reduce number_of_day weekday.monday   -- 2
#reduce number_of_day weekday.tuesday  -- 3

-- 2ª forma (con cases_on)
def number_of_day2 (d : weekday) : ℕ :=
weekday.cases_on d 1 2 3 4 5 6 7

#reduce number_of_day2 weekday.sunday   -- 1
#reduce number_of_day2 weekday.monday   -- 2
#reduce number_of_day2 weekday.tuesday  -- 3

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

namespace weekday
  @[reducible]
  private def cases_on := @weekday.cases_on

  def number_of_day (d : weekday) : nat :=
  cases_on d 1 2 3 4 5 6 7
end weekday

#reduce weekday.number_of_day weekday.sunday  -- 1

open weekday (renaming cases_on → cases_on)

#reduce number_of_day sunday   -- 1
#check cases_on

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

namespace weekday
  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

  #reduce next (next tuesday)
  #reduce next (previous tuesday)

  example : next (previous tuesday) = tuesday := rfl

  theorem next_previous (d: weekday) :
    next (previous d) = d :=
  weekday.cases_on d
    (show next (previous sunday) = sunday, from rfl)
    (show next (previous monday) = monday, from rfl)
    (show next (previous tuesday) = tuesday, from rfl)
    (show next (previous wednesday) = wednesday, from rfl)
    (show next (previous thursday) = thursday, from rfl)
    (show next (previous friday) = friday, from rfl)
    (show next (previous saturday) = saturday, from rfl)

  -- 2ª demostración
  theorem next_previous2 (d: weekday) :
    next (previous d) = d :=
  weekday.cases_on d rfl rfl rfl rfl rfl rfl rfl

  -- 3ª demostración
  theorem next_previous3 (d: weekday) :
    next (previous d) = d :=
  by apply weekday.cases_on d; refl

  -- 4ª demostración
  theorem next_previous4 (d: weekday) :
    next (previous d) = d :=
  by apply weekday.rec_on d; refl

end weekday

namespace hidden
inductive empty : Type

inductive unit : Type
| star : unit

inductive bool : Type
| ff : bool
| tt : bool

end hidden

namespace hidden

def band (b1 b2 : bool) : bool :=
bool.cases_on b1 ff b2

#reduce band tt tt -- tt
#reduce band tt ff -- ff
#reduce band ff tt -- ff
#reduce band ff ff -- ff

end hidden

namespace hidden

universes u v

inductive prod (α : Type u) (β : Type v)
| mk : α → β → prod

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

end hidden

universes u v

def fst {α : Type u} {β : Type v} (p : α × β) : α :=
prod.rec_on p (λ a b, a)

def snd {α : Type u} {β : Type v} (p : α × β) : β :=
prod.rec_on p (λ a b, b)

def prod_example (p : bool × ℕ) : ℕ :=
prod.rec_on p (λ b n, cond b (2 * n) (2 * n + 1))

#reduce prod_example (tt, 3)  -- 6
#reduce prod_example (ff, 3)  -- 7

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

#reduce sum_example (sum.inl 3)  -- 6
#reduce sum_example (sum.inr 3)  -- 7

namespace hidden

universes u v

inductive prod (α : Type u) (β : Type v)
| mk (fst : α) (snd : β) : prod

inductive sum (α : Type u) (β : Type v)
| inl {} (a : α) : sum
| inr {} (b : β) : sum

end hidden

namespace hidden

structure prod (α β : Type) :=
mk :: (fst : α) (snd : β)

end hidden

open nat

structure color := (red : nat) (green : nat) (blue : nat)

def yellow := color.mk 255 255 0

#reduce color.red   yellow   -- 255
#reduce color.green yellow   -- 255
#reduce color.blue  yellow   -- 0

universe u

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

universes u v

namespace hidden

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

end hidden

universe u

namespace hidden

inductive option (α : Type u)
| none {} : option
| some    : α → option

inductive inhabited (α : Type u)
| mk : α → inhabited

end hidden

namespace hidden

inductive false : Prop

inductive true : Prop
| intro : true

inductive and (a b : Prop) : Prop
| intro : a → b → and

inductive or (a b : Prop) : Prop
| intro_left  : a → or
| intro_right : b → or

end hidden

universe u

namespace hidden

inductive Exists {α : Type u} (p : α → Prop) : Prop
| intro : ∀ (a : α), p a → Exists

def exists.intro := @Exists.intro

end hidden

universe u

namespace hidden

inductive subtype {α : Type u} (p : α → Prop)
| mk : Π x : α, p x → subtype

end hidden

universe u
namespace hidden

structure subtype {α : Sort u} (p : α → Prop) :=
(val : α) (property : p val)

section
variables {α : Type u} (p : α → Prop)

#check subtype p
#check { x : α // p x}
end

end hidden

namespace hidden

-- Definición de los naturales
-- ===========================

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

-- Tipo de nat.rec_on
-- ==================

#check @nat.rec_on

-- Da
--    Π {C : nat → Sort u_1} (n : nat), 
--    C nat.zero → (Π (a : nat), C a → C (nat.succ a)) → C n 

namespace nat

-- Definición de suma
def add (m n : nat) : nat :=
nat.rec_on n m (λ n add_m_n, succ add_m_n)

-- Cálculo de suma
#reduce add (succ zero) (succ (succ zero))   -- succ (succ (succ zero))

-- Notación para la suma
instance : has_zero nat := has_zero.mk zero
instance : has_add nat := has_add.mk add

-- Ecuaciones de la suma
theorem add_zero (m : nat) : m + 0 = m := rfl
theorem add_succ (m n : nat) : m + succ n = succ (m + n) := rfl

end nat

end hidden

namespace hidden
open nat

-- 1ª demostración
theorem zero_add (n : ℕ) : 0 + n = n :=
nat.rec_on n
  (show 0 + 0 = 0, from rfl)
  (assume n,
    assume ih : 0 + n = n,
    show 0 + succ n = succ n, from
      calc
        0 + succ n = succ (0 + n) : rfl
               ... = succ n       : by rw ih)

-- 2ª demostración
theorem zero_add2 (n : ℕ) : 0 + n = n :=
nat.rec_on n rfl (λ n ih, by rw [add_succ, ih])

-- 2ª demostración
theorem zero_add3 (n : ℕ) : 0 + n = n :=
nat.rec_on n rfl (λ n ih, by simp only [add_succ, ih])

end hidden

namespace hidden
open nat

-- 1ª demostración
theorem add_assoc (m n k : ℕ) : (m + n) + k = m + (n + k) :=
nat.rec_on k
  (show (m + n) + 0 = m + (n + 0), from rfl)
  (assume k,
    assume ih : (m + n) + k = m + (n + k),
    show (m + n) + succ k = m + (n + succ k), from
      calc
        (m + n) + succ k = succ ((m + n) + k) : rfl
          ... = succ (m + (n + k)) : by rw ih
          ... = m + succ (n + k) : rfl
          ... = m + (n + succ k) : rfl)

-- 2ª demostración
theorem add_assoc2 (m n k : ℕ) : m + n + k = m + (n + k) :=
nat.rec_on k rfl (λ k ih, by simp only [add_succ, ih])

end hidden

namespace hidden
open nat

-- 1ª demostración
-- ===============

theorem add_assoc (m n k : ℕ) : m + n + k = m + (n + k) :=
nat.rec_on k
  (show m + n + 0 = m + (n + 0), from rfl)
  (assume k,
    assume ih : m + n + k = m + (n + k),
    show m + n + succ k = m + (n + succ k), from
      calc
        m + n + succ k = succ (m + n + k) : rfl
          ... = succ (m + (n + k)) : by rw ih
          ... = m + succ (n + k) : rfl
          ... = m + (n + succ k) : rfl)

theorem succ_add (m n : nat) : succ m + n = succ (m + n) :=
nat.rec_on n
  (show succ m + 0 = succ (m + 0), from rfl)
  (assume n,
    assume ih : succ m + n = succ (m + n),
    show succ m + succ n = succ (m + succ n), from
      calc
        succ m + succ n = succ (succ m + n) : rfl
          ... = succ (succ (m + n)) : by rw ih
          ... = succ (m + succ n) : rfl)

-- 2ª demostración
-- ===============

theorem add_assoc2 (m n k : ℕ) : m + n + k = m + (n + k) :=
nat.rec_on k rfl (λ k ih, by simp only [add_succ, ih])

theorem succ_add2 (m n : nat) : succ m + n = succ (m + n) :=
nat.rec_on n rfl (λ n ih, by simp only [succ_add, ih])

-- Conmutativa
-- ===========

theorem add_comm (m n : nat) : m + n = n + m :=
nat.rec_on n
  (by simp only [zero_add, add_zero])
  (λ n ih, by simp only [add_succ, ih, succ_add])

end hidden

universe u

namespace hidden

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

namespace list

variable {α : Type}

notation h :: t  := cons h t

def append (s t : list α) : list α :=
list.rec t (λ x l u, x::u) s

notation s ++ t := append s t

theorem nil_append (t : list α) : nil ++ t = t := rfl

theorem cons_append (x : α) (s t : list α) :
  (x::s) ++ t = x::(s ++ t) := rfl

end list

end hidden

universe u

namespace hidden

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

namespace list

notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l

section
  open nat
  #check [1, 2, 3, 4, 5]
  #check ([1, 2, 3, 4, 5] : list int)
end

end list

end hidden

inductive binary_tree
| leaf : binary_tree
| node : binary_tree → binary_tree → binary_tree

inductive cbtree
| leaf : cbtree
| sup : (ℕ → cbtree) → cbtree

namespace cbtree

def succ (t : cbtree) : cbtree :=
sup (λ n, t)

def omega : cbtree :=
sup (λ n, nat.rec_on n leaf (λ n t, succ t))

end cbtree

open nat
variable p : ℕ → Prop

example (hz : p 0) (hs : ∀ n, p (succ n)) : ∀ n, p n :=
begin
  intro n,
  cases n,
  { exact hz },  
  apply hs       
end

open nat

example (n : ℕ) (h : n ≠ 0) : succ (pred n) = n :=
begin
  cases n with m,
    { apply (absurd rfl h) },
  reflexivity
end

def f (n : ℕ) : ℕ :=
begin
  cases n, exact 3, exact 7
end

example : f 0 = 3 := rfl
example : f 5 = 7 := rfl

universe u

def tuple (α : Type u) (n : ℕ) :=
  { l : list α // list.length l = n }

variables {α : Type u} {n : ℕ}

def f {n : ℕ} (t : tuple α n) : ℕ :=
begin
  cases n, exact 3, exact 7
end

def my_tuple : tuple ℕ 3 :=  ⟨[0, 1, 2], rfl⟩

example : f my_tuple = 7 := rfl

inductive foo : Type
| bar1 : ℕ → ℕ → foo
| bar2 : ℕ → ℕ → ℕ → foo

def silly (x : foo) : ℕ :=
begin
  cases x with a b c d e,
  exact b,    -- a, b    are in the context
  exact e     -- c, d, e are in the context
end

#reduce silly (foo.bar1 5 7)   -- 7
#reduce silly (foo.bar2 5 7 9) -- 9

inductive foo : Type
| bar1 : ℕ → ℕ → foo
| bar2 : ℕ → ℕ → ℕ → foo

open foo

def silly (x : foo) : ℕ :=
begin
  cases x,
    case bar1 : a b
      { exact b },
    case bar2 : c d e
      { exact e }
end

open nat
variable p : ℕ → Prop

example (hz : p 0) (hs : ∀ n, p (succ n)) (m k : ℕ) :
  p (m + 3 * k) :=
begin
  cases (m + 3 * k),
  { exact hz },  
  apply hs       
end

open nat
variable p : ℕ → Prop

example (hz : p 0) (hs : ∀ n, p (succ n)) (m k : ℕ) :
  p (m + 3 * k) :=
begin
  generalize : m + 3 * k = n,
  cases n,
  { exact hz },  
  apply hs       
end

example (p : Prop) (m n : ℕ)
  (h₁ : m < n → p) (h₂ : m ≥ n → p) : p :=
begin
  cases lt_or_ge m n with hlt hge,
  { exact h₁ hlt },
  exact h₂ hge
end

-- 2ª demostración
example (p : Prop) (m n : ℕ)
  (h₁ : m < n → p) (h₂ : m ≥ n → p) : p :=
begin
  have h : m < n ∨ m ≥ n,
  { exact lt_or_ge m n },
  cases h with hlt hge,
  { exact h₁ hlt },
  exact h₂ hge
end

#check nat.sub_self

example (m n : ℕ) : m - n = 0 ∨ m ≠ n :=
begin
  cases decidable.em (m = n) with heq hne,
  { rw heq,
    left, exact nat.sub_self n },
  right, exact hne
end

def f (m k : ℕ) : ℕ :=
begin
  cases m - k, exact 3, exact 7
end

example : f 5 7 = 3 := rfl
example : f 10 2 = 7 := rfl

namespace hidden
open nat

theorem zero_add (n : ℕ) : 0 + n = n :=
begin
  induction n with n ih,
    refl,
  rw [add_succ, ih]
end

theorem zero_add (n : ℕ) : 0 + n = n :=
begin
  induction n,
  case zero : { refl },
  case succ : n ih { rw [add_succ, ih]}
end

theorem succ_add (m n : ℕ) : succ m + n = succ (m + n) :=
begin
  induction n,
  case zero : { refl },
  case succ : n ih { rw [add_succ, ih] }
end

theorem add_comm (m n : ℕ) : m + n = n + m :=
begin
  induction n,
  case zero : { rw zero_add, refl },
  case succ : n ih { rw [add_succ, ih, succ_add] }
end

end hidden

namespace hidden
open nat

theorem zero_add (n : ℕ) : 0 + n = n :=
by induction n; simp only [*, add_zero, add_succ]

theorem succ_add (m n : ℕ) : succ m + n = succ (m + n) :=
by induction n; simp only [*, add_zero, add_succ]

theorem add_comm (m n : ℕ) : m + n = n + m :=
by induction n;
     simp only [*, add_zero, add_succ, succ_add, zero_add]

theorem add_assoc (m n k : ℕ) : m + n + k = m + (n + k) :=
by induction k; simp only [*, add_zero, add_succ]

end hidden

open nat

example (m n k : ℕ) (h : succ (succ m) = succ (succ n)) :
  n + k = m + k :=
begin
  injection h with h',
  injection h' with h'',
  rw h''
end

open nat

example (m n k : ℕ) (h : succ (succ m) = succ (succ n)) :
  n + k = m + k :=
begin
  injections with h' h'',
  rw h''
end

example (m n k : ℕ) (h : succ (succ m) = succ (succ n)) :
  n + k = m + k :=
by injections; simp *

open nat

example (m n : ℕ) (h : succ m = 0) : n = n + 7 :=
by injections

example (m n : ℕ) (h : succ m = 0) : n = n + 7 :=
by contradiction

example (h : 7 = 4) : false :=
by injections

open nat
universe u
namespace hidden

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

end hidden

universe u
namespace hidden

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

end hidden

universes u v

#check (@eq.rec_on :
  Π {α : Sort u} {a : α} {C : α → Sort v} {b : α},
    a = b → C a → C b)

namespace hidden
universe u

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

@[elab_as_eliminator]
theorem subst {α : Type u} {a b : α} {p : α → Prop}
  (h₁ : eq a b) (h₂ : p a) : p b :=
eq.rec h₂ h₁

end hidden

namespace hidden
universe u

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

@[elab_as_eliminator]
theorem subst {α : Type u} {a b : α} {P : α → Prop}
  (h₁ : eq a b) (h₂ : P a) : P b :=
eq.rec h₂ h₁


theorem symm {α : Type u} {a b : α} (h : eq a b) : eq b a :=
subst h (eq.refl a)

theorem trans {α : Type u} {a b c : α}
  (h₁ : eq a b) (h₂ : eq b c) : eq a c :=
subst h₂ h₁

theorem congr {α β : Type u} {a b : α} (f : α → β)
  (h : eq a b) : eq (f a) (f b) :=
subst h (eq.refl (f a))

end hidden

mutual inductive even, odd
with even : ℕ → Prop
| even_zero : even 0
| even_succ : ∀ n, odd n → even (n + 1)
with odd : ℕ → Prop
| odd_succ : ∀ n, even n → odd (n + 1)

universe u

mutual inductive tree, list_tree (α : Type u)
with tree : Type u
| node : α → list_tree → tree
with list_tree : Type u
| nil {}  : list_tree
| cons    : tree → list_tree → list_tree

inductive tree2 (α : Type u)
| mk : α → list tree2 → tree2