Lean formalized in Lean

tc.lean

import data.option data.list.basic data.int.order

attribute [derive decidable_eq] name

namespace tc

inductive level
| var : ℕ → level
| zero : level
| succ : level → level
| max : level → level → level
| imax : level → level → level

namespace level
instance : has_zero level := ⟨zero⟩

def maxvar : level → ℕ
| (var n) := n + 1
| 0 := 0
| (succ l) := maxvar l
| (max l₁ l₂) := _root_.max (maxvar l₁) (maxvar l₂)
| (imax l₁ l₂) := _root_.max (maxvar l₁) (maxvar l₂)

def subst_gen_var (n : ℕ) : list level → ℕ → level
| []     i     := var (i + n)
| (a::s) 0     := a
| (a::s) (i+1) := subst_gen_var s i

def subst_gen (s : list level) (n : ℕ) : level → level
| (var i) := subst_gen_var n s i
| 0 := 0
| (succ l) := succ (subst_gen l)
| (max l₁ l₂) := max (subst_gen l₁) (subst_gen l₂)
| (imax l₁ l₂) := imax (subst_gen l₁) (subst_gen l₂)

def lift (l : level) (n : ℕ := 1) : level := subst_gen [] n l

def subst (s : level) (l : level) : level := subst_gen [s] 0 l

@[simp] def eval (s : list ℕ) : level → ℕ
| (var n)      := s.inth n
| 0            := 0
| (succ l)     := eval l + 1
| (max l₁ l₂)  := _root_.max (eval l₁) (eval l₂)
| (imax l₁ l₂) :=
  match eval l₂ with
  | 0 := 0
  | n := _root_.max (eval l₁) n
  end

def add_nat (l : level) : ℕ → level
| 0     := l
| (n+1) := succ (add_nat n)

instance : has_le level :=
⟨λ l₁ l₂, ∀ v, eval v l₁ ≤ eval v l₂⟩

instance : has_equiv level :=
⟨λ l₁ l₂, ∀ v, eval v l₁ = eval v l₂⟩

def le_add (l₁ l₂ n) := ∀ v, (eval v l₁ : ℤ) ≤ eval v l₂ + n
#print acc
instance : ∀ l₁ l₂ n, decidable (le_add l₁ l₂ n) := sorry
/-
| 0 l₂ (n : ℕ) := is_true (λ v, by simp)
| l₁ 0 -[1+ n] := is_false (λ h, begin
    have := h [], simp at this,
    exact not_lt_of_le this
      (lt_of_lt_of_le (int.neg_succ_lt_zero _) (int.coe_zero_le _))
  end)
| (var i) (var j) n := decidable_of_iff (i = j ∧ n ≥ 0) (begin
    have := h [], simp at this,
    exact not_lt_of_le this
      (lt_of_lt_of_le (int.neg_succ_lt_zero _) (int.coe_zero_le _))
  end)
-/

instance decidable_le : @decidable_rel level (≤) :=
λ l₁ l₂, decidable_of_iff (le_add l₁ l₂ 0)
  (forall_congr $ λ v, by simp [int.coe_nat_le])

end level

inductive expr : Type
| var {} : ℕ → expr
| const : name → list level → expr → expr
| sort {} : level → expr
| app : expr → expr → expr
| lam : expr → expr → expr
| pi : expr → expr → expr

namespace expr

def maxuvar : expr → ℕ
| (var n) := 0
| (const a l α) := (level.maxvar <$> l).foldl max 0
| (sort u) := level.maxvar u
| (app e₁ e₂) := max (maxuvar e₁) (maxuvar e₂)
| (lam e₁ e₂) := max (maxuvar e₁) (maxuvar e₂)
| (pi e₁ e₂) := max (maxuvar e₁) (maxuvar e₂)

def lift' (n : ℕ) : expr → ℕ → expr
| (var i) m := var $ if i < m then i else i + n
| (app e₁ e₂) m := app (lift' e₁ m) (lift' e₂ m)
| (lam e₁ e₂) m := lam (lift' e₁ m) (lift' e₂ (m+1))
| (pi e₁ e₂) m := pi (lift' e₁ m) (lift' e₂ (m+1))
| e m := e

def lift (e : expr) (n : ℕ := 1) : expr := lift' n e 0

def subst_gen_var (m n : ℕ) : list expr → ℕ → expr
| []     i     := var (i + m + n)
| (a::s) 0     := lift a m
| (a::s) (i+1) := subst_gen_var s i

def subst_gen (s : list expr) (n : ℕ) : expr → ℕ → expr
| (var i) m := if i < m then var i else subst_gen_var m n s (i-m)
| (app e₁ e₂) m := app (subst_gen e₁ m) (subst_gen e₂ m)
| (lam e₁ e₂) m := lam (subst_gen e₁ m) (subst_gen e₂ (m+1))
| (pi e₁ e₂) m := pi (subst_gen e₁ m) (subst_gen e₂ (m+1))
| e m := e

def subst (s : expr) (e : expr) : expr :=
subst_gen [s] 0 e 0

def usubst_gen (s : list level) (n : ℕ) : expr → expr
| (const a l α) := const a (level.subst_gen s n <$> l) α
| (sort u) := sort (level.subst_gen s n u)
| (app e₁ e₂) := app (usubst_gen e₁) (usubst_gen e₂)
| (lam e₁ e₂) := lam (usubst_gen e₁) (usubst_gen e₂)
| (pi e₁ e₂) := pi (usubst_gen e₁) (usubst_gen e₂)
| e := e

def usubsts (s : list level) : expr → expr := usubst_gen s 0

mutual inductive valid, defeq (ext : expr → expr → Prop := λ _ _, false)
with valid : list expr → expr → expr → Prop
| weak {α Γ e t} : valid Γ e t → valid (α::Γ) (lift e) (lift t)
| var {α Γ l} : valid Γ α (sort l) → valid (α::Γ) (var 0) α
| const {Γ n l α u} :
  valid [] α (sort u) → maxuvar α ≤ list.length l →
  valid Γ (const n l α) (usubsts l α)
| sort {l} : valid [] (sort l) (sort l.succ)
| app {Γ e₁ e₂ α β} : valid Γ e₁ (pi α β) → valid Γ e₂ α →
  valid Γ (app e₁ e₂) (subst e₂ β)
| lam {Γ α e β} : valid (α::Γ) e β → valid Γ (lam α e) (pi α β)
| pi {Γ α β u v} : valid Γ α (sort u) → valid (α::Γ) β (sort v) →
  valid Γ (pi α β) (sort (u.imax v))
| defeq {Γ e α β u} : valid Γ e α → valid Γ β (sort u) →
  defeq Γ α β → valid Γ e β

with defeq : list expr → expr → expr → Prop
| refl {Γ e} : defeq Γ e e
| symm {Γ e e'} : defeq Γ e e' → defeq Γ e' e
| trans {Γ e₁ e₂ e₃} : defeq Γ e₁ e₂ → defeq Γ e₂ e₃ → defeq Γ e₁ e₃
| weak {α Γ e e'} : defeq Γ e e' → defeq (α::Γ) (lift e) (lift e')
| sort {l₁ l₂} : l₁ ≈ l₂ → defeq [] (sort l₁) (sort l₂)
| app {Γ e₁ e₂ e₁' e₂'} : defeq Γ e₁ e₁' → defeq Γ e₂ e₂' →
  defeq [] (app e₁ e₂) (app e₁' e₂')
| lam {Γ α e α' e'} : defeq Γ α α' → defeq (α::Γ) e e' →
  defeq [] (lam α e) (lam α' e')
| pi {Γ α e α' e'} : defeq Γ α α' → defeq (α::Γ) e e' →
  defeq [] (pi α e) (pi α' e')
| beta {Γ α e e'} : defeq Γ (app (lam α e) e') (subst e' e)
| eta {Γ e α} : defeq Γ (lam α (app (lift e) (var 0))) e
| irrel {Γ h h' p} : valid Γ p (sort 0) →
  valid Γ h p → valid Γ h' p → defeq Γ h h'
| ext {Γ e e'} : ext e e' → defeq Γ e e'

end expr

structure cnst_spec :=
(name : name)
(uvars : ℕ)
(ty : {e:expr // e.maxuvar ≤ uvars})

structure def_spec extends cnst_spec :=
(val : {e:expr // e.maxuvar ≤ uvars})

inductive env
| nil
| cnst : cnst_spec → env → env
| defn : def_spec → env → env
| ind : cnst_spec → list cnst_spec → env → env

namespace env

namespace ind

def large_elim : cnst_spec → list cnst_spec → bool :=
sorry

def rec_ty : cnst_spec → list cnst_spec → option cnst_spec :=
sorry

end ind

def decls : env → list cnst_spec
| nil := []
| (cnst c e) := c :: decls e
| (defn d e) := d.to_cnst_spec :: decls e
| (ind c l e) :=
  match ind.rec_ty c l with
  | some rt := rt :: l ++ c :: decls e
  | none := decls e
  end

def typeof (e : env) (n : name) : option expr :=
(e.decls.find (λ p : cnst_spec, p.name = n)).map $ λ p, p.ty.1

inductive ext : env → expr → expr → Prop
| weak_cnst {c e a b} : ext e a b → ext (cnst c e) a b
| weak_defn {d e a b} : ext e a b → ext (defn d e) a b
| weak_ind {c l e a b} : ext e a b → ext (ind c l e) a b
| delta {d : def_spec} {e l} : list.length l = d.to_cnst_spec.uvars →
  ext (defn d e) (expr.const d.name l d.ty) (d.val.1.usubsts l)
| iota {d : def_spec} {e l} : list.length l = d.to_cnst_spec.uvars →
  ext (defn d e) (expr.const d.name l d.ty) (d.val.1.usubsts l)

/-
inductive valid' : env → Prop
| nil              : valid' nil
| cnst {n t e}   : valid' e → valid' (cnst n t e)
| defn {n t p e} : valid' e → valid' (defn n t p e)
| ind {n t l e}  : valid' e → ind_valid n t l e → valid' (ind n t l e)
-/


end env

end tc