Changes

3 changed files (+312/-659)

• Dependent.lean
  • @@ -1,67 +1,246 @@
    - -- Trying to implement dependent types wheee + -- μLean, a very simple proof assistant with dependent types and polymorphism! inductive Term - -- Terms that cannot be types - /-- Variable -/ + -- The basic stuff + /-- Variable with de Bruijn index -/ | var (x : Nat) /-- Lambda -/ | lam (b β : Term) /-- Function application -/ | app (f φ a α : Term) -- Types - /-- New named type -/ - | new (x : Nat) + /-- Type of types -/ + | typ /-- Dependent function type -/ | fn (α β : Term) -- Inductive types /-- Dependent product type -/ | prod (α β : Term) /-- Constructor for product -/ - | and (a α b β : Term) - /-- Get first element of product -/ - | and1 (p π : Term) - /-- Get second element of product -/ - | and2 (p π : Term) + | pair + /-- Recursor for product -/ + | prod_rec /-- Sum type -/ | sum (α β : Term) - /-- Construct a sum -/ - | or (c γ : Term) + /-- Left constructor for sum -/ + | inl + /-- Right constructor for sum -/ + | inr + /-- Recursor for sum -/ + | sum_rec /-- Equality type -/ | eq (a a' α : Term) /-- Constructor for equality -/ - | rfl (a α : Term) - /-- Eliminator for equality -/ - | rw (a a' α f h ha : Term) + | rfl + /-- Recursor for equality -/ + | eq_rec /-- Natural number type -/ | nat - /-- Zero as a nat -/ + /-- Zero constructor for nats -/ | zero - /-- One or greater as a nat -/ - | succ (n ν : Term) - /-- Eliminator for nats -/ - | nat_elim (α n ν b β f φ : Term) - /-- False (no terms of this type) -/ + /-- Successor constructor for nats -/ + | succ + /-- Recursor for nats -/ + | nat_rec + /-- False (empty type) -/ | fls - /-- Eliminator for false -/ - | fls_elim (a α : Term) - -- Universe stuff (only two universes for now) - /-- Type of types -/ - | typ + /-- Recursor for false -/ + | fls_rec + /-- New named variable -/ + | new (s : String) (t : Term) + /-- Use of named variable -/ + | name (s : String) deriving BEq, ReflBEq, LawfulBEq + open Term + + def Term.toString : Term → String + | var x => s!"(list 0n {x})" + | lam b β => s!"(list 1n {toString b} {toString β})" + | app f φ a α => s!"(list 2n {toString f} {toString φ} {toString a} {toString α})" + | typ => "'(3n)" + | fn α β => s!"(list 4n {toString α} {toString β})" + | prod α β => s!"(list 5n {toString α} {toString β})" + | pair => "'(6n)" + | prod_rec => "'(7n)" + | sum α β => s!"(list 8n {toString α} {toString β})" + | inl => "'(9n)" + | inr => "'(10n)" + | sum_rec => "'(11n)" + | eq a a' α => s!"(list 12n {toString a} {toString a'} {toString α})" + | rfl => "'(13n)" + | eq_rec => "'(14n)" + | nat => "'(15n)" + | zero => "'(16n)" + | succ => "'(17n)" + | nat_rec => "'(18n)" + | fls => "'(19n)" + | fls_rec => "'(20n)" + | _ => "bad" + + -- instance : ToString Term := ⟨Term.toString⟩ + + -- instance : ToString (Term × Term) := ⟨fun p ↦ s!"(cons {p.1} {p.2})"⟩ + + -- `infixr` doesn't work at compile time or something + notation α " ⇨ " β => fn α β -- \he + notation "𝒰" => typ -- \McU + notation "⊥" => fls -- \bo + notation "ℕ" => nat -- \N + -- `max` fixes some precedence issues when parsing + syntax:max "’" ident : term -- \rq + macro_rules + | `(’$s:ident) => `(name $(Lean.Syntax.mkStrLit s.getId.toString)) + syntax ident "◆" term:max : term -- \di + macro_rules + | `($s:ident ◆ $t) => `(new $(Lean.Syntax.mkStrLit s.getId.toString) $t) + /-- Increment free variables by 1 -/ def incr (d : Nat) : Term → Term - | .var x => - .var (if d ≤ x then x + 1 else x) - | .lam b β => - .lam (incr (d + 1) b) (incr (d + 1) β) - | .app f φ a α => - .app (incr d f) (incr d φ) (incr d a) (incr d α) - | .fn α β => - .fn (incr d α) (incr d β) - | x => x - - mutual + | var x => + var (if d ≤ x then x + 1 else x) + | lam b β => + lam (incr (d + 1) b) (incr (d + 1) β) + | app f φ a α => + app (incr d f) (incr d φ) (incr d a) (incr d α) + | α ⇨ β => + incr d α ⇨ incr (d + 1) β + | prod α β => + prod (incr d α) (incr (d + 1) β) + | sum α β => + sum (incr d α) (incr d β) + | eq a a' α => + eq (incr d a) (incr d a') (incr d α) + | t => t + + /-- Substitute `s` at index `n` in a term -/ + def sub (n : Nat) (s : Term) : Term → Term + | var x => + if x == n then s else var (if n < x then x - 1 else x) + | lam b β => + lam (sub (n + 1) (incr 0 s) b) (sub (n + 1) (incr 0 s) β) + | app f φ a α => + app (sub n s f) (sub n s φ) (sub n s a) (sub n s α) + | α ⇨ β => + sub n s α ⇨ sub (n + 1) (incr 0 s) β + | prod α β => + prod (sub n s α) (sub (n + 1) (incr 0 s) β) + | sum α β => + sum (sub n s α) (sub n s β) + | eq a a' α => + eq (sub n s a) (sub n s a') (sub n s α) + | t => t + + /-- Convenience wrapper around `lam` with currying -/ + def la (b : Term) : Term → Nat → Term + | .new s _ ⇨ β, n + 1 => lam (.new s (la b β n)) (.new s β) + | _, _ => b + + /-- Bundle the type with `la` -/ + def la' b β n := (la b β n, β) + + /-- Convenience wrapper around `app` with currying -/ + def ap (f : Term) : Term → List Term → Term + -- Need to eval both these guys? + | α ⇨ β, x :: xs => ap (app f (α ⇨ β) x α) (sub 0 x β) xs + | _, _ => f + + /-- Convert from variable names to de Bruijn indices -/ + def debruijn (names : List String) : Term → Term + | name s => + var (names.idxOf s) + | new s t => + debruijn (s :: names) t + | lam b β => + lam (debruijn names b) (debruijn names β) + | app f φ a α => + app (debruijn names f) (debruijn names φ) (debruijn names a) (debruijn names α) + | new s α ⇨ β => + debruijn names α ⇨ debruijn (s :: names) β + | α ⇨ β => + debruijn names α ⇨ debruijn ("" :: names) β + | prod (new s α) β => + prod (debruijn names α) (debruijn (s :: names) β) + | prod α β => + prod (debruijn names α) (debruijn ("" :: names) β) + | sum α β => + sum (debruijn names α) (debruijn names β) + | eq a a' α => + eq (debruijn names a) (debruijn names a') (debruijn names α) + | t => t + + #guard debruijn [] (α◆𝒰 ⇨ β◆𝒰 ⇨ ’α ⇨ ’β ⇨ prod ’α ’β) == 𝒰 ⇨ 𝒰 ⇨ var 1 ⇨ var 1 ⇨ prod (var 3) (var 3) + + /-- Get type of built-in functions -/ + def Term.btype (t : Term) := + match t with + | pair => + α◆𝒰 ⇨ β◆𝒰 ⇨ ’α ⇨ ’β ⇨ prod ’α ’β + | prod_rec => + let μ := prod ’α ’β ⇨ 𝒰 + α◆𝒰 ⇨ β◆𝒰 ⇨ m◆μ ⇨ (a◆’α ⇨ b◆’β ⇨ ap ’m μ [ap pair pair.btype [’a, ’b]]) ⇨ p◆(prod ’α ’β) ⇨ ap ’m μ [’p] + | inl => + α◆𝒰 ⇨ β◆𝒰 ⇨ ’α ⇨ sum ’α ’β + | inr => + α◆𝒰 ⇨ β◆𝒰 ⇨ ’β ⇨ sum ’α ’β + | sum_rec => + let μ := sum ’α ’β ⇨ 𝒰 + α◆𝒰 ⇨ β◆𝒰 ⇨ m◆μ ⇨ (a◆’α ⇨ ap ’m μ [ap inl inl.btype [’a]]) ⇨ (b◆’β ⇨ ap ’m μ [ap inr inr.btype [’b]]) ⇨ s◆(sum ’α ’β) ⇨ ap ’m μ [’s] + | rfl => + α◆𝒰 ⇨ a◆’α ⇨ eq ’a ’a ’α + | eq_rec => + let μ := x◆’α ⇨ eq ’a ’x ’α ⇨ 𝒰 + α◆𝒰 ⇨ a◆’α ⇨ m◆μ ⇨ ap ’m μ [’a, ap rfl rfl.btype [’α, ’a]] ⇨ b◆’α ⇨ h◆(eq ’a ’b ’α) ⇨ ap ’m μ [’b, ’h] + | zero => + ℕ + | succ => + ℕ ⇨ ℕ + | nat_rec => + let μ := ℕ ⇨ 𝒰 + m◆μ ⇨ z◆(ap ’m μ [zero]) ⇨ s◆(n◆ℕ ⇨ ap ’m μ [’n] ⇨ ap ’m μ [ap succ succ.btype [’n]]) ⇨ t◆ℕ ⇨ ap ’m μ [’t] + | fls_rec => + m◆(fls ⇨ 𝒰) ⇨ f◆fls ⇨ ap ’m (fls ⇨ 𝒰) [’f] + | _ => + name "bad" + termination_by + match t with + | prod_rec | sum_rec | eq_rec | nat_rec => 1 + | _ => 0 + + /-- `t` should be well-typed or bad things will happen! -/ + partial def eval (t : Term) : Term := + match t with + | lam b β => + lam (eval b) (eval β) + -- | app (app (app .fst _ _ _) _ _ _) _ (app (app (app (app .and _ _ _) _ _ _) _ a _) _ _ _) _ => + -- eval a + -- | app (app (app .snd _ _ _) _ _ _) _ (app (app (app (app .and _ _ _) _ _ _) _ _ _) _ b _) _ => + -- eval b + | app (app (app (app .nat_rec _ m _) _ z _) _ f φ) _ n _ => + match n with + | zero => eval z + -- TODO replace ν with the type of .nat_rec + | app succ _ n _ => eval (ap f φ [n, ap .nat_rec Term.nat_rec.btype [m, z, f, n]]) + | _ => t + -- eq_rec seems useless? + -- | app (app (app (app (app (app eq_rec ε α _) _ a _) _ m _) _ r _) _ a' _) _ h _ => + | app f φ a α => + -- TODO handle dependent funcs + let a' := eval a + match eval f with + | lam b _ => eval (sub 0 (incr 0 a') b) + | x => app x φ a' α -- Probably want to eval again here + | α ⇨ β => + eval α ⇨ eval β + | prod α β => + prod (eval α) (eval β) + | sum α β => + sum (eval α) (eval β) + | eq a a' α => + eq (eval a) (eval a') (eval α) + | t => + t + -- /-- -/ -- def defeq (env : List Term) a a' α := -- check env a α && check env a' α' && eval env a α == eval env a' α'
  • @@ -69,105 +248,143 @@ mutual
    -- TODO: A lot of the `==`s here should use defeq /-- Janky type checker -/ def check (env : List Term) : Term → Term → Bool - | .var x, α => + | var x, α => if _ : x < env.length then env[x] == α else false - | .lam b β, .fn α β' => - β' == β && (β == .typ || check (α :: env) β .typ) && check (α :: env) b β - | .app f (.fn α β) a α', β' => - α' == α && β' == β && check env f (.fn α β) && check env a α - | .new x, .typ => - true - | .fn α β, .typ => - check env α .typ && check env β .typ - | .prod α β, .typ => - check env α .typ && check env β .typ - | .and a α b β, .prod α' β' => - α' == α && β' == β && (β == .typ || check (α :: env) β .typ) && check env a α && check env b β - | .and1 p (.prod α β), α' => - α' == α && check env p (.prod α β) - | .and2 p (.prod α β), β' => - β' == β && (β == .typ || check (α :: env) β .typ) && check env p (.prod α β) - | .sum α β, .typ => - check env α .typ && check env β .typ - | .or c γ, .sum α β => - (γ == α || γ == β) && check env c γ - | .eq a a' α, .typ => - check env a α && check env a' α && check env α .typ - | .rfl a α, .eq a' a'' α' => - α' == α && a' == a && a'' == a && check env a α - | .rw a a' α m h ha, ha' => - -- TODO this needs eval for sure - check env h (.eq a a' α) --&& check env ha (.app (.app m (.fn α (.fn (.eq ) .typ)) a α)) -- && check env ha' (.app p (.fn α .typ) a' α) - | .nat, .typ | .zero, .nat => - true - | .succ n .nat, .nat => - check env n .nat - | .nat_elim α n .nat a α₁ f (.fn .nat (.fn α₂ α₃)), .fn .nat α₄ => - α₁ == α && α₂ == α && α₃ == α && α₄ == α && check env n .nat && check env a α && check env f (.fn .nat (.fn α α)) - | .fls, .typ => + | lam b β, α ⇨ β' => + β' == β && check (incr 0 <$> (α :: env)) b β + -- β' == β && (β == 𝒰 || check (incr 0 <$> (α :: env)) β 𝒰) && check (incr 0 <$> (α :: env)) b β + | app f (α ⇨ β) a α', β' => + α' == α && β' == sub 0 a β && check env f (α ⇨ β) && check env a α + | .nat, 𝒰 + | ⊥, 𝒰 => true - | .fls_elim a .fls, _ => - check env a .fls - | _, _ => - false + | α ⇨ β, 𝒰 => + check env α 𝒰 && check (incr 0 <$> (α :: env)) β 𝒰 + | prod α β, 𝒰 + | sum α β, 𝒰 => + check env α 𝒰 && check env β 𝒰 + | eq a a' α, 𝒰 => + check env a α && check env a' α && check env α 𝒰 + | t, τ => + debruijn [] t.btype == τ - end + def check' (t : Term × Term) := + check [] (debruijn [] t.1) (debruijn [] t.2) /-- A → A -/ - def a_imp_a := (Term.lam (.var 0) (.new 0), Term.fn (.new 0) (.new 0)) + def a_imp_a := la' ’a (α◆𝒰 ⇨ a◆’α ⇨ ’α) 2 + + #guard check' a_imp_a + + /-- A → B → A ∧ B -/ + def a_imp_b_imp_ab := la' (ap pair pair.btype [’α, ’β]) (α◆𝒰 ⇨ β◆𝒰 ⇨ ’α ⇨ ’β ⇨ prod ’α ’β) 2 - #guard check [] a_imp_a.1 a_imp_a.2 + #guard check' a_imp_b_imp_ab /-- A → B → B ∧ A -/ - def a_imp_b_imp_ba := (Term.lam (.lam (.and (.var 0) (.new 1) (.var 1) (.new 0)) (.prod (.new 1) (.new 0))) (.fn (.new 1) (.prod (.new 1) (.new 0))), Term.fn (.new 0) (.fn (.new 1) (.prod (.new 1) (.new 0)))) + def a_imp_b_imp_ba := la' (ap pair pair.btype [’β, ’α, ’b, ’a]) (α◆𝒰 ⇨ β◆𝒰 ⇨ a◆’α ⇨ b◆’β ⇨ prod ’β ’α) 4 - #guard check [] a_imp_b_imp_ba.1 a_imp_b_imp_ba.2 + #guard check' a_imp_b_imp_ba + + /-- Get first element of product -/ + def fst α β p := ap prod_rec prod_rec.btype [α, β, la α (prod α β ⇨ 𝒰) 1, la ’a (new "a" α ⇨ β ⇨ α) 2, p] + + /-- Get second element of product -/ + def snd α β p := ap prod_rec prod_rec.btype [α, β, la β (prod α β ⇨ 𝒰) 1, la ’b (α ⇨ new "b" β ⇨ β) 2, p] /-- A ∧ B → B ∧ A -/ - def ab_imp_ba := (Term.lam (.and (.and2 (.var 0) (.prod (.new 0) (.new 1))) (.new 1) (.and1 (.var 0) (.prod (.new 0) (.new 1))) (.new 0)) (.prod (.new 1) (.new 0)), Term.fn (.prod (.new 0) (.new 1)) (.prod (.new 1) (.new 0))) + def ab_imp_ba := la' (and (snd ₸0 ₸1 ’0) ₸1 (fst ₸0 ₸1 ’0) ₸0) (prod ₸0 ₸1 ⇨ prod ₸1 ₸0) 1 #guard check [] ab_imp_ba.1 ab_imp_ba.2 + /-- Convenience wrapper around `.inl` -/ + def inl α β a := app .inl (𝒰 ⇨ 𝒰 ⇨ ’1 ⇨ sum ’2 ’1) [α, β, a] + /-- ¬(A ∨ B) → ¬A -/ - def not_ab_imp_not_a := (Term.lam (.lam (.app (.var 1) (.fn (.sum (.new 0) (.new 1)) .fls) (.or (.var 0) (.new 0)) (.sum (.new 0) (.new 1))) (.fls)) (.fn (.new 0) .fls), Term.fn (.fn (.sum (.new 0) (.new 1)) .fls) (.fn (.new 0) .fls)) + def not_ab_imp_not_a := la' (app ’1 (sum ₸0 ₸1 ⇨ ⊥) [inl ₸0 ₸1 ’0]) ((sum ₸0 ₸1 ⇨ ⊥) ⇨ ₸0 ⇨ ⊥) 2 #guard check [] not_ab_imp_not_a.1 not_ab_imp_not_a.2 /-- A → ¬¬A -/ - def a_imp_not_not_a := (Term.lam (.lam (.app (.var 0) (.fn (.new 0) .fls) (.var 1) (.new 0)) (.fls)) (.fn (.fn (.new 0) .fls) .fls), Term.fn (.new 0) (.fn (.fn (.new 0) .fls) .fls)) + def a_imp_not_not_a := la' (app ’0 (₸0 ⇨ ⊥) [’1]) (₸0 ⇨ (₸0 ⇨ ⊥) ⇨ ⊥) 2 #guard check [] a_imp_not_not_a.1 a_imp_not_not_a.2 /-- ¬¬¬A → ¬A -/ - def not_not_not_a_imp_not_a := (Term.lam (.lam (.app (.var 1) (.fn (.fn (.fn (.new 0) .fls) .fls) .fls) (.app a_imp_not_not_a.1 a_imp_not_not_a.2 (.var 0) (.new 0)) (.fn (.fn (.new 0) .fls) .fls)) (.fls)) (.fn (.new 0) .fls), Term.fn (.fn (.fn (.fn (.new 0) .fls) .fls) .fls) (.fn (.new 0) .fls)) + def not_not_not_a_imp_not_a := la' (app ’1 (((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) [app a_imp_not_not_a.1 a_imp_not_not_a.2 [’0]]) ((((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) ⇨ ₸0 ⇨ ⊥) 2 #guard check [] not_not_not_a_imp_not_a.1 not_not_not_a_imp_not_a.2 + /-- Alternative proof of ¬¬¬A → ¬A -/ + def not_not_not_a_imp_not_a' := la' (app ’1 (((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) [lam (app ’0 (₸0 ⇨ ⊥) [’1]) ⊥]) ((((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) ⇨ ₸0 ⇨ ⊥) 2 + + #guard check [] not_not_not_a_imp_not_a'.1 not_not_not_a_imp_not_a'.2 + + /-- Convenience wrapper around `.rfl` -/ + def rfl' a α := app .rfl (𝒰 ⇨ ’0 ⇨ eq ’0 ’0 ’1) [α, a] + /-- ∀ a : A, a = a -/ - def a_eq_a := (Term.lam (.rfl (.var 0) (.new 0)) (.eq (.var 0) (.var 0) (.new 0)), Term.fn (.new 0) (.eq (.var 0) (.var 0) (.new 0))) + def a_eq_a := la' (rfl' ’0 ₸0) (₸0 ⇨ eq ’0 ’0 ₸0) 1 #guard check [] a_eq_a.1 a_eq_a.2 - /-- 2 exists (yeah I know this is not super exciting) -/ - def two := (Term.succ (.succ .zero .nat) .nat, Term.nat) + /-- Convenience wrapper around `.succ` -/ + def succ n := app .succ (ℕ ⇨ ℕ) [n] + + -- /-- 2 exists (yeah I know this is not super exciting) -/ + def two := (succ (succ zero), ℕ) #guard check [] two.1 two.2 /-- 4 exists -/ - def four := (Term.succ (.succ two.1 two.2) .nat, Term.nat) + def four := (succ (succ two.1), ℕ) #guard check [] four.1 four.2 + #check Nat.rec + + /-- `.nat_rec` where the motive always returns `ℕ` -/ + def nat_rec_nat z f := Termapp (app (app .nat_rec ((ℕ ⇨ 𝒰) ⇨ app ’0 (ℕ ⇨ 𝒰) zero ℕ ⇨ (ℕ ⇨ app ’2 (ℕ ⇨ 𝒰) ’0 ℕ ⇨ app ’3 (ℕ ⇨ 𝒰) (app .succ (ℕ ⇨ ℕ) ’1 ℕ) ℕ) ⇨ ℕ ⇨ app ’0 ℕ ’3 (ℕ ⇨ 𝒰)) (lam ℕ 𝒰) (ℕ ⇨ 𝒰)) (ℕ ⇨ (ℕ ⇨ ℕ ⇨ ℕ) ⇨ ℕ ⇨ ℕ) z ℕ) ((ℕ ⇨ ℕ ⇨ ℕ) ⇨ ℕ ⇨ ℕ) f (ℕ ⇨ ℕ ⇨ ℕ) + + #eval nat_rec_nat ₸0 ₸1 + + def nat_rec_nat' z f := app .nat_rec ((ℕ ⇨ 𝒰) ⇨ app ’0 (ℕ ⇨ 𝒰) zero ℕ ⇨ (ℕ ⇨ app ’2 (ℕ ⇨ 𝒰) ’0 ℕ ⇨ app ’3 (ℕ ⇨ 𝒰) (app .succ (ℕ ⇨ ℕ) ’1 ℕ) ℕ) ⇨ ℕ ⇨ app ’0 ℕ ’3 (ℕ ⇨ 𝒰)) [lam ℕ 𝒰, z, f] + + #eval nat_rec_nat' ₸0 ₸1 + + #check Nat.rec + /-- Addition -/ - def add := (Term.lam (.nat_elim .nat .zero .nat (.var 0) .nat (.lam (.lam (.succ (.var 2) .nat) .nat) (.fn .nat .nat)) (.fn .nat (.fn .nat .nat))) (.fn .nat .nat), Term.fn .nat (.fn .nat .nat)) + def add := la' (nat_rec_nat ’0 (lam (succ ’0) (ℕ ⇨ ℕ) 1)) (ℕ ⇨ ℕ ⇨ ℕ) 1 #guard check [] add.1 add.2 - def two_plus_two := (Term.app (.app add.1 add.2 two.1 two.2) (.fn .nat .nat) two.1 two.2, Term.nat) + def zero_plus_zero := app add.1 add.2 [zero, zero] + + #eval eval (eval zero_plus_zero) + + def zero_plus_one := app add.1 add.2 [zero, succ zero] + + #eval eval (eval zero_plus_one) + + -- example : eval zero_plus_zero.1 = zero := by + -- unfold zero_plus_zero add + -- simp + -- unfold nat_rec_nat + + def two_plus_two := app add.1 add.2 [two.1, two.1] + + #eval eval (eval two_plus_two) == four.1 + + + def eq_rec_type := 𝒰 ⇨ ’0 ⇨ (’1 ⇨ eq ’1 ’0 ’2 ⇨ 𝒰) ⇨ app ’0 (’2 ⇨ eq ’2 ’0 ’3 ⇨ 𝒰) [’1, app .rfl (𝒰 ⇨ ’0 ⇨ eq ’0 ’0 ’1) [’2, ’2]] ⇨ ’3 ⇨ eq ’3 ’0 ’4 ⇨ app ’3 (’5 ⇨ eq ’5 ’0 ’6 ⇨ 𝒰) [’1, ’0] + + def rw := lam (app eq_rec eq_rec_type [’5, ’4, lam (app ’5 (’7 ⇨ 𝒰) [’1]) (’5 ⇨ (eq ’5 ’0 ’6) ⇨ 𝒰) 2]) (𝒰 ⇨ ’0 ⇨ ’1 ⇨ (’2 ⇨ 𝒰) ⇨ eq ’2 ’1 ’3 ⇨ app ’1 (’4 ⇨ 𝒰) [’3] ⇨ app ’2 (’5 ⇨ 𝒰) [’3]) 6 - #guard check [] two_plus_two.1 two_plus_two.2 + -- #guard check [] two_plus_two.1 two_plus_two.2 - /-- 2 + 2 = 4 -/ - def two_plus_two_eq_four := (Term.fls, Term.eq two_plus_two.1 four.1 .nat) + -- /-- 2 + 2 = 4 -/ + -- def two_plus_two_eq_four := (Term.fls, Termeq two_plus_two.1 four.1 ℕ) - #guard check [] two_plus_two_eq_four.1 two_plus_two_eq_four.2 + -- #guard check [] two_plus_two_eq_four.1 two_plus_two_eq_four.2 + -- -/
• DependentEval.lean (deleted)
  • @@ -1,328 +0,0 @@
    - -- μLean, a very simple proof assistant with dependent types and polymorphism! - - inductive Term - -- The basic stuff - /-- Variable with de Bruijn index -/ - | var (x : Nat) - /-- Lambda -/ - | lam (b β : Term) - /-- Function application -/ - | app (f φ a α : Term) - -- Types - /-- Type of types -/ - | typ - /-- New named type -/ - | new (x : Nat) - /-- Dependent function type -/ - | fn (α β : Term) - -- Inductive types - /-- Dependent product type -/ - | prod (α β : Term) - /-- Constructor for product -/ - | and - /-- Get first element of product -/ - | fst - /-- Get second element of product -/ - | snd - /-- Sum type -/ - | sum (α β : Term) - /-- Construct a sum using left type -/ - | inl - /-- Construct a sum using right type -/ - | inr - /-- Equality type -/ - | eq (a a' α : Term) - /-- Constructor for equality -/ - | rfl - /-- Recursor for equality -/ - | eq_rec - /-- Natural number type -/ - | nat - /-- Zero as a nat -/ - | zero - /-- One or greater as a nat -/ - | succ - /-- Recursor for nats -/ - | nat_rec - /-- False (empty type) -/ - | fls - /-- Recursor for false -/ - | fls_rec - deriving BEq, ReflBEq, LawfulBEq - - def Term.toString : Term → String - | .var x => s!"(list 0n {x})" - | .lam b β => s!"(list 1n {toString b} {toString β})" - | .app f φ a α => s!"(list 2n {toString f} {toString φ} {toString a} {toString α})" - | .typ => "'(3n)" - | .new x => s!"(list 4n {x})" - | .fn α β => s!"(list 5n {toString α} {toString β})" - | .prod α β => s!"(list 6n {toString α} {toString β})" - | .and => "'(7n)" - | .fst => "'(8n)" - | .snd => "'(9n)" - | .sum α β => s!"(list 10n {toString α} {toString β})" - | .inl => "'(11n)" - | .inr => "'(12n)" - | .eq a a' α => s!"(list 13n {toString a} {toString a'} {toString α})" - | .rfl => "'(14n)" - | .eq_rec => "'(15n)" - | .nat => "'(16n)" - | .zero => "'(17n)" - | .succ => "'(18n)" - | .nat_rec => "'(19n)" - | .fls => "'(20n)" - | .fls_rec => "'(21n)" - - instance : ToString Term := ⟨Term.toString⟩ - - instance : ToString (Term × Term) := ⟨fun p ↦ s!"(cons {p.1} {p.2})"⟩ - - -- `infixr` doesn't work at compile time or something - notation l " ⇨ " r => Term.fn l r -- \he - -- `max` fixes some precedence issues when parsing - notation "λ " b:max β:max => Term.lam b β -- \fu - notation:max "’" r:max => Term.var r -- \rq - notation:max "₸" r:max => Term.new r -- \te - notation "𝒰" => Term.typ -- \McU - notation "⊥" => Term.fls -- \bo - notation "ℕ" => Term.nat -- \N - - /-- Increment free variables by 1 -/ - def incr (d : Nat) : Term → Term - | ’x => - ’(if d ≤ x then x + 1 else x) - | (λ b β) => -- Need parentheses to avoid parsing as a Lean lambda - λ (incr (d + 1) b) (incr (d + 1) β) - | .app f φ a α => - .app (incr d f) (incr d φ) (incr d a) (incr d α) - | α ⇨ β => - incr d α ⇨ incr (d + 1) β - | .prod α β => - .prod (incr d α) (incr (d + 1) β) - | .sum α β => - .sum (incr d α) (incr d β) - | .eq a a' α => - .eq (incr d a) (incr d a') (incr d α) - | x => x - - /-- Substitute `s` at index `n` in a term -/ - def sub (n : Nat) (s : Term) : Term → Term - | ’x => - if x == n then s else ’(if n < x then x - 1 else x) - | (λ b β) => - λ (sub (n + 1) (incr 0 s) b) (sub (n + 1) (incr 0 s) β) - | .app f φ a α => - .app (sub n s f) (sub n s φ) (sub n s a) (sub n s α) - | α ⇨ β => - sub n s α ⇨ sub (n + 1) (incr 0 s) β - | .prod α β => - .prod (sub n s α) (sub (n + 1) (incr 0 s) β) - | .sum α β => - .sum (sub n s α) (sub n s β) - | .eq a a' α => - .eq (sub n s a) (sub n s a') (sub n s α) - | x => x - - /-- Convenience wrapper around .app with currying -/ - def app (f : Term) : Term → List Term → Term - -- Need to eval both these guys? - -- Probably need to `incr 0 <$> xs`? Actually no - | α ⇨ β, x :: xs => app (.app f (α ⇨ β) x α) (sub 0 x β) xs - | _, _ => f - - def clean := 𝒰 ⇨ ’0 ⇨ (’1 ⇨ .eq ’1 ’0 ’2 ⇨ 𝒰) ⇨ app ’0 (’2 ⇨ .eq ’2 ’0 ’3 ⇨ 𝒰) [’1, app .rfl (𝒰 ⇨ ’0 ⇨ .eq ’0 ’0 ’1) [’2, ’2]] ⇨ ’3 ⇨ .eq ’3 ’0 ’4 ⇨ app ’3 (’5 ⇨ .eq ’5 ’0 ’6 ⇨ 𝒰) [’1, ’0] - - #reduce clean - #reduce 𝒰 ⇨ ’0 ⇨ (’1 ⇨ .eq ’1 ’0 ’2 ⇨ 𝒰) ⇨ .app (.app ’0 (’2 ⇨ .eq ’2 ’0 ’3 ⇨ 𝒰) ’1 ’2) (.eq ’1 ’1 ’2 ⇨ 𝒰) (.app (.app .rfl (𝒰 ⇨ ’0 ⇨ .eq ’0 ’0 ’1) ’2 𝒰) (’2 ⇨ .eq ’0 ’0 ’3) ’2 ’3) (.eq ’1 ’1 ’2) ⇨ ’3 ⇨ .eq ’3 ’0 ’4 ⇨ .app (.app ’3 (’5 ⇨ .eq ’5 ’0 ’6 ⇨ 𝒰) ’1 ’5) (.eq ’4 ’1 ’5) ’0 (.eq ’4 ’1 ’5) - - -- /-- -/ - -- def defeq (env : List Term) a a' α := - -- check env a α && check env a' α' && eval env a α == eval env a' α' - - -- TODO: A lot of the `==`s here should use defeq - /-- Janky type checker -/ - def check (env : List Term) : Term → Term → Bool - | ’x, α => - if _ : x < env.length then env[x] == α else false - | λ b β, α ⇨ β' => - β' == β && (β == 𝒰 || check (incr 0 <$> (α :: env)) β 𝒰) && check (incr 0 <$> (α :: env)) b β - | .app f (α ⇨ β) a α', β' => - α' == α && β' == sub 0 a β && check env f (α ⇨ β) && check env a α - | .new _, 𝒰 - | .nat, 𝒰 - | ⊥, 𝒰 => - true - | α ⇨ β, 𝒰 => - check env α 𝒰 && check (incr 0 <$> (α :: env)) β 𝒰 - | .prod α β, 𝒰 - | .sum α β, 𝒰 => - check env α 𝒰 && check env β 𝒰 - | .eq a a' α, 𝒰 => - check env a α && check env a' α && check env α 𝒰 - | .and, 𝒰 ⇨ 𝒰 ⇨ ’1 ⇨ ’1 ⇨ .prod ’3 ’3 - | .fst, 𝒰 ⇨ 𝒰 ⇨ .prod ’1 ’1 ⇨ ’2 - | .snd, 𝒰 ⇨ 𝒰 ⇨ .prod ’1 ’1 ⇨ ’1 - | .inl, 𝒰 ⇨ 𝒰 ⇨ ’1 ⇨ .sum ’2 ’1 - | .inr, 𝒰 ⇨ 𝒰 ⇨ ’0 ⇨ .sum ’2 ’1 - | .rfl, 𝒰 ⇨ ’0 ⇨ .eq ’0 ’0 ’1 - | .eq_rec, 𝒰 ⇨ ’0 ⇨ (’1 ⇨ .eq ’1 ’0 ’2 ⇨ 𝒰) ⇨ .app (.app ’0 (’2 ⇨ .eq ’2 ’0 ’3 ⇨ 𝒰) ’1 ’2) (.eq ’1 ’1 ’2 ⇨ 𝒰) (.app (.app .rfl (𝒰 ⇨ ’0 ⇨ .eq ’0 ’0 ’1) ’2 𝒰) (’2 ⇨ .eq ’0 ’0 ’3) ’2 ’3) (.eq ’1 ’1 ’2) ⇨ ’3 ⇨ .eq ’3 ’0 ’4 ⇨ .app (.app ’3 (’5 ⇨ .eq ’5 ’0 ’6 ⇨ 𝒰) ’1 ’5) (.eq ’4 ’1 ’5) ’0 (.eq ’4 ’1 ’5) - | .nat_rec, (ℕ ⇨ 𝒰) ⇨ .app ’0 (ℕ ⇨ 𝒰) .zero ℕ ⇨ (ℕ ⇨ .app ’2 (ℕ ⇨ 𝒰) ’0 ℕ ⇨ .app ’3 (ℕ ⇨ 𝒰) (.app .succ (ℕ ⇨ ℕ) ’1 ℕ) ℕ) ⇨ ℕ ⇨ .app ’0 ℕ ’3 (ℕ ⇨ 𝒰) - | .zero, ℕ - | .succ, ℕ ⇨ ℕ - | .fls_rec, ⊥ ⇨ _ => - true - | _, _ => - false - - /-- `t` should be well-typed or bad things will happen! -/ - partial def eval (t : Term) := - match t with - | (λ b β) => - λ (eval b) (eval β) - | .app (.app (.app .fst _ _ _) _ _ _) _ (.app (.app (.app (.app .and _ _ _) _ _ _) _ a _) _ _ _) _ => - eval a - | .app (.app (.app .snd _ _ _) _ _ _) _ (.app (.app (.app (.app .and _ _ _) _ _ _) _ _ _) _ b _) _ => - eval b - | .app (.app (.app (.app .nat_rec τ₁ m τ₂) τ₃ z ℕ) τ₄ f φ) τ₅ n ℕ => - match n with - | .zero => eval z - | .app .succ (ℕ ⇨ ℕ) n' ℕ => eval (.app (.app f φ n ℕ) (.app m τ₂ n' ℕ ⇨ .app m τ₂ n ℕ) (.app (.app (.app (.app .nat_rec τ₁ m τ₂) τ₃ z ℕ) τ₄ f φ) τ₅ n' ℕ) (.app m τ₂ n ℕ)) - | _ => t - | .app f φ a α => - let a' := eval a - match eval f with - | (λ b _) => eval (sub 0 (incr 0 a') b) - | x => .app x φ a' α - | α ⇨ β => - eval α ⇨ eval β - | .prod α β => - .prod (eval α) (eval β) - | .sum α β => - .sum (eval α) (eval β) - | .eq a a' α => - .eq (eval a) (eval a') (eval α) - -- eq_rec - | x => - x - - /-- A → A -/ - def a_imp_a := (λ ’0 ₸0, ₸0 ⇨ ₸0) - - #guard check [] a_imp_a.1 a_imp_a.2 - - /-- ∀ A : 𝒰, A → A -/ - def a_imp_a' := (λ (λ ’0 ’1) (’0 ⇨ ’1), 𝒰 ⇨ ’0 ⇨ ’1) - - #guard check [] a_imp_a'.1 a_imp_a'.2 - - /-- A → B → A ∧ B -/ - def a_imp_b_imp_ab := (app .and (𝒰 ⇨ 𝒰 ⇨ ’1 ⇨ ’1 ⇨ .prod ’3 ’3) [₸0, ₸1], ₸0 ⇨ ₸1 ⇨ .prod ₸0 ₸1) - - #guard check [] a_imp_b_imp_ab.1 a_imp_b_imp_ab.2 - - /-- Convenience wrapper around `.and` -/ - def and a α b β := app .and (𝒰 ⇨ 𝒰 ⇨ ’1 ⇨ ’1 ⇨ .prod ’3 ’3) [α, β, a, b] - - /-- A → B → B ∧ A -/ - def a_imp_b_imp_ba := (λ (λ (and ’0 ₸1 ’1 ₸0) (.prod ₸1 ₸0)) (₸1 ⇨ .prod ₸1 ₸0), ₸0 ⇨ ₸1 ⇨ .prod ₸1 ₸0) - - #guard check [] a_imp_b_imp_ba.1 a_imp_b_imp_ba.2 - - /-- Convenience wrapper around `.fst` -/ - def fst α β p := app .fst (𝒰 ⇨ 𝒰 ⇨ .prod ’1 ’1 ⇨ ’2) [α, β, p] - - /-- Convenience wrapper around `.snd` -/ - def snd α β p := app .snd (𝒰 ⇨ 𝒰 ⇨ .prod ’1 ’1 ⇨ ’1) [α, β, p] - - /-- A ∧ B → B ∧ A -/ - def ab_imp_ba := (λ (and (snd ₸0 ₸1 ’0) ₸1 (fst ₸0 ₸1 ’0) ₸0) (.prod ₸1 ₸0), .prod ₸0 ₸1 ⇨ .prod ₸1 ₸0) - - #guard check [] ab_imp_ba.1 ab_imp_ba.2 - - /-- Convenience wrapper around `.inl` -/ - def inl α β a := app .inl (𝒰 ⇨ 𝒰 ⇨ ’1 ⇨ .sum ’2 ’1) [α, β, a] - - /-- ¬(A ∨ B) → ¬A -/ - def not_ab_imp_not_a := (λ (λ (app ’1 (.sum ₸0 ₸1 ⇨ ⊥) [inl ₸0 ₸1 ’0]) ⊥) (₸0 ⇨ ⊥), (.sum ₸0 ₸1 ⇨ ⊥) ⇨ ₸0 ⇨ ⊥) - - #guard check [] not_ab_imp_not_a.1 not_ab_imp_not_a.2 - - /-- A → ¬¬A -/ - def a_imp_not_not_a := (λ (λ (app ’0 (₸0 ⇨ ⊥) [’1]) ⊥) ((₸0 ⇨ ⊥) ⇨ ⊥), ₸0 ⇨ (₸0 ⇨ ⊥) ⇨ ⊥) - - #guard check [] a_imp_not_not_a.1 a_imp_not_not_a.2 - - /-- ¬¬¬A → ¬A -/ - def not_not_not_a_imp_not_a := (λ (λ (app ’1 (((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) [app a_imp_not_not_a.1 a_imp_not_not_a.2 [’0]]) ⊥) (₸0 ⇨ ⊥), (((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) ⇨ ₸0 ⇨ ⊥) - - #guard check [] not_not_not_a_imp_not_a.1 not_not_not_a_imp_not_a.2 - - /-- Alternative proof of ¬¬¬A → ¬A -/ - def not_not_not_a_imp_not_a' := (λ (λ (app ’1 (((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) [λ (app ’0 (₸0 ⇨ ⊥) [’1]) ⊥]) ⊥) (₸0 ⇨ ⊥), (((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) ⇨ ₸0 ⇨ ⊥) - - #guard check [] not_not_not_a_imp_not_a'.1 not_not_not_a_imp_not_a'.2 - - /-- Convenience wrapper around `.rfl` -/ - def rfl' a α := app .rfl (𝒰 ⇨ ’0 ⇨ .eq ’0 ’0 ’1) [α, a] - - /-- ∀ a : A, a = a -/ - def a_eq_a := (λ (rfl' ’0 ₸0) (.eq ’0 ’0 ₸0), ₸0 ⇨ .eq ’0 ’0 ₸0) - - #guard check [] a_eq_a.1 a_eq_a.2 - - /-- Convenience wrapper around `.succ` -/ - def succ n := app .succ (ℕ ⇨ ℕ) [n] - - -- /-- 2 exists (yeah I know this is not super exciting) -/ - def two := (succ (succ .zero), ℕ) - - #guard check [] two.1 two.2 - - /-- 4 exists -/ - def four := (succ (succ two.1), ℕ) - - #guard check [] four.1 four.2 - - #check Nat.rec - - /-- `.nat_rec` where the motive always returns `ℕ` -/ - def nat_rec_nat z f := Term.app (.app (.app .nat_rec ((ℕ ⇨ 𝒰) ⇨ .app ’0 (ℕ ⇨ 𝒰) .zero ℕ ⇨ (ℕ ⇨ .app ’2 (ℕ ⇨ 𝒰) ’0 ℕ ⇨ .app ’3 (ℕ ⇨ 𝒰) (.app .succ (ℕ ⇨ ℕ) ’1 ℕ) ℕ) ⇨ ℕ ⇨ .app ’0 ℕ ’3 (ℕ ⇨ 𝒰)) (λ ℕ 𝒰) (ℕ ⇨ 𝒰)) (ℕ ⇨ (ℕ ⇨ ℕ ⇨ ℕ) ⇨ ℕ ⇨ ℕ) z ℕ) ((ℕ ⇨ ℕ ⇨ ℕ) ⇨ ℕ ⇨ ℕ) f (ℕ ⇨ ℕ ⇨ ℕ) - - #eval nat_rec_nat ₸0 ₸1 - - def nat_rec_nat' z f := app .nat_rec ((ℕ ⇨ 𝒰) ⇨ .app ’0 (ℕ ⇨ 𝒰) .zero ℕ ⇨ (ℕ ⇨ .app ’2 (ℕ ⇨ 𝒰) ’0 ℕ ⇨ .app ’3 (ℕ ⇨ 𝒰) (.app .succ (ℕ ⇨ ℕ) ’1 ℕ) ℕ) ⇨ ℕ ⇨ .app ’0 ℕ ’3 (ℕ ⇨ 𝒰)) [λ ℕ 𝒰, z, f] - - #eval nat_rec_nat' ₸0 ₸1 - - #check Nat.rec - - /-- Addition -/ - def add := (λ (nat_rec_nat ’0 (λ (λ (succ ’0) (ℕ ⇨ ℕ)) ℕ)) (ℕ ⇨ ℕ), ℕ ⇨ ℕ ⇨ ℕ) - - #guard check [] add.1 add.2 - - def zero_plus_zero := app add.1 add.2 [.zero, .zero] - - #eval eval (eval zero_plus_zero) - - def zero_plus_one := app add.1 add.2 [.zero, succ .zero] - - #eval eval (eval zero_plus_one) - - -- example : eval zero_plus_zero.1 = .zero := by - -- unfold zero_plus_zero add - -- simp - -- unfold nat_rec_nat - - def two_plus_two := app add.1 add.2 [two.1, two.1] - - #eval eval (eval two_plus_two) == four.1 - - -- #guard check [] two_plus_two.1 two_plus_two.2 - - -- /-- 2 + 2 = 4 -/ - -- def two_plus_two_eq_four := (Term.fls, Term.eq two_plus_two.1 four.1 ℕ) - - -- #guard check [] two_plus_two_eq_four.1 two_plus_two_eq_four.2 - -- -/
• DependentRefactor.lean (deleted)
  • @@ -1,236 +0,0 @@
    - -- μLean, a very simple proof assistant with dependent types! - - inductive Term - -- The basic stuff - /-- Variable with de Bruijn index -/ - | var (x : Nat) - /-- Lambda -/ - | lam (b β : Term) - /-- Function application -/ - | app (f φ a α : Term) - -- Types - /-- Type of types -/ - | typ - /-- New named type -/ - | new (x : Nat) - /-- Dependent function type -/ - | fn (α β : Term) - -- Inductive types - /-- Dependent product type -/ - | prod (α β : Term) - /-- Constructor for product -/ - | and - /-- Get first element of product -/ - | fst - /-- Get second element of product -/ - | snd - /-- Sum type -/ - | sum (α β : Term) - /-- Construct a sum using left type -/ - | inl - /-- Construct a sum using right type -/ - | inr - /-- Equality type -/ - | eq (a a' α : Term) - /-- Constructor for equality -/ - | rfl - /-- Recursor for equality -/ - | eq_rec - /-- Natural number type -/ - | nat - /-- Zero as a nat -/ - | zero - /-- One or greater as a nat -/ - | succ - /-- Recursor for nats -/ - | nat_rec - /-- False (empty type) -/ - | fls - /-- Recursor for false -/ - | fls_rec - deriving BEq, ReflBEq, LawfulBEq - - /-- Increment free variables by 1 -/ - def incr (d : Nat) : Term → Term - | .var x => - .var (if d ≤ x then x + 1 else x) - | .lam b β => - .lam (incr (d + 1) b) (incr (d + 1) β) - | .app f φ a α => - .app (incr d f) (incr d φ) (incr d a) (incr d α) - | .fn α β => - .fn (incr d α) (incr d β) - | .prod α β => - .prod (incr d α) (incr d β) - | .sum α β => - .sum (incr d α) (incr d β) - | .eq a a' α => - .eq (incr d a) (incr d a') (incr d α) - | x => x - - /-- Substitute `s` at index `n` in a term -/ - def sub (n : Nat) (s : Term) : Term → Term - | .var x => - if x == n then s else .var (if n < x then x - 1 else x) - | .lam b β => - .lam (sub (n + 1) (incr 0 s) b) (sub (n + 1) (incr 0 s) β) - | .app f φ a α => - .app (sub n s f) (sub n s φ) (sub n s a) (sub n s α) - | .fn α β => - .fn (sub n s α) (sub n s β) - | .prod α β => - .prod (sub n s α) (sub n s β) - | .sum α β => - .sum (sub n s α) (sub n s β) - | .eq a a' α => - .eq (sub n s a) (sub n s a') (sub n s α) - | x => x - - notation "𝒰" => Term.typ - notation "ℕ" => Term.nat - -- `infixr` doesn't work? - notation l " →ₘ " r => Term.fn l r - -- The `max` fixes some precedence issues when parsing or something - notation:max "’" r:max => Term.var r - - mutual - -- /-- -/ - -- def defeq (env : List Term) a a' α := - -- check env a α && check env a' α' && eval env a α == eval env a' α' - - -- TODO: A lot of the `==`s here should use defeq - /-- Janky type checker -/ - def check (env : List Term) : Term → Term → Bool - | .var x, α => - if _ : x < env.length then env[x] == α else false - | .lam b β, α →ₘ β' => - β' == β && (β == 𝒰 || check (α :: env) β 𝒰) && check (α :: env) b β - | .app f (α →ₘ β) a α', β' => - α' == α && β' == β && check env f (α →ₘ β) && check env a α - | .new x, 𝒰 - | .nat, 𝒰 - | .fls, 𝒰 => - true - | .fn α β, 𝒰 - | .prod α β, 𝒰 - | .sum α β, 𝒰 => - check env α 𝒰 && check env β 𝒰 - | .eq a a' α, 𝒰 => - check env a α && check env a' α && check env α 𝒰 - | .and, 𝒰 →ₘ 𝒰 →ₘ ’1 →ₘ ’1 →ₘ .prod ’3 ’2 - | .fst, 𝒰 →ₘ 𝒰 →ₘ .prod ’1 ’0 →ₘ ’2 - | .snd, 𝒰 →ₘ 𝒰 →ₘ .prod ’1 ’0 →ₘ ’1 - | .inl, 𝒰 →ₘ 𝒰 →ₘ ’1 →ₘ .sum ’2 ’1 - | .inr, 𝒰 →ₘ 𝒰 →ₘ ’0 →ₘ .sum ’2 ’1 - | .rfl, 𝒰 →ₘ ’0 →ₘ .eq ’0 ’0 ’1 - -- https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types/#inductive-families - | .eq_rec, 𝒰 →ₘ ’0 →ₘ (’1 →ₘ .eq ’1 ’0 ’2 →ₘ 𝒰) →ₘ .app (.app ’0 (’2 →ₘ .eq ’2 ’0 ’3 →ₘ 𝒰) ’1 ’2) (.eq ’1 ’1 ’2 →ₘ 𝒰) (.app (.app .rfl (𝒰 →ₘ ’0 →ₘ .eq ’0 ’0 ’1) ’2 𝒰) (’2 →ₘ .eq ’0 ’0 ’3) ’2 ’3) (.eq ’1 ’1 ’2) →ₘ ’3 →ₘ .eq ’3 ’0 ’4 →ₘ .app (.app ’3 (’5 →ₘ .eq ’5 ’0 ’6 →ₘ 𝒰) ’1 ’5) (.eq ’4 ’1 ’5) ’0 (.eq ’4 ’1 ’5) - | .nat_rec, (ℕ →ₘ 𝒰) →ₘ .app ’0 (ℕ →ₘ 𝒰) .zero ℕ →ₘ (ℕ →ₘ .app ’2 (ℕ →ₘ 𝒰) ’0 ℕ →ₘ .app ’3 (ℕ →ₘ 𝒰) (.app .succ (ℕ →ₘ ℕ) ’1 ℕ) ℕ) - | .zero, ℕ - | .succ, .fn ℕ ℕ - | .fls_rec, .fn .fls _ => - true - | _, _ => - false - - end - - /-- A → A -/ - def a_imp_a := (Term.lam ’0 (.new 0), .new 0 →ₘ .new 0) - - #guard check [] a_imp_a.1 a_imp_a.2 - - def and a α b β := Term.app (.app (.app (.app .and (𝒰 →ₘ 𝒰 →ₘ ’1 →ₘ ’1 →ₘ .prod ’3 ’2) α 𝒰) (𝒰 →ₘ α →ₘ ’1 →ₘ .prod α ’2) β 𝒰) (α →ₘ β →ₘ .prod α β) a α) (β →ₘ .prod α β) b β - - /-- A → B → A ∧ B -/ - def a_imp_b_imp_ab := (Term.app (.app .and (𝒰 →ₘ 𝒰 →ₘ ’1 →ₘ ’1 →ₘ .prod ’3 ’2) (.new 0) 𝒰) (𝒰 →ₘ (.new 0) →ₘ ’1 →ₘ .prod (.new 0) ’2) (.new 1) 𝒰, .new 0 →ₘ .new 1 →ₘ .prod (.new 0) (.new 1)) - - example : check [] a_imp_b_imp_ab.1 a_imp_b_imp_ab.2 = true := by - unfold check a_imp_b_imp_ab - simp only [BEq.rfl, Bool.true_and, Bool.and_eq_true, beq_iff_eq] - - - - - #guard check [] a_imp_b_imp_ab.1 a_imp_b_imp_ab.2 - - - /-- A → B → B ∧ A -/ - def a_imp_b_imp_ba := (Term.lam (.lam (and ’0 (.new 1) ’1 (.new 0)) (.prod (.new 1) (.new 0))) (.new 1 →ₘ .prod (.new 1) (.new 0)), .new 0 →ₘ .new 1 →ₘ .prod (.new 1) (.new 0)) - - -- example : check [] a_imp_b_imp_ba.1 a_imp_b_imp_ba.2 = true := by - -- unfold check a_imp_b_imp_ba - -- simp - -- have : check [Term.new 0] (Term.new 1 →ₘ (Term.new 1).prod (Term.new 0)) 𝒰 = true := by decide - -- simp [this] - -- unfold check - -- simp - -- have : check [Term.new 1, Term.new 0] ((Term.new 1).prod (Term.new 0)) 𝒰 = true := by decide - -- simp [this] - -- unfold _root_.and check - -- simp - -- have : check [Term.new 1, Term.new 0] (’1) (Term.new 0) = true := by decide - -- simp [this] - -- unfold check - -- simp - -- have : check [Term.new 1, Term.new 0] (’0) (Term.new 1) = true := by decide - -- simp [this] - -- unfold check - - - - - - - #eval a_imp_b_imp_ba.1 - - #guard check [] a_imp_b_imp_ba.1 a_imp_b_imp_ba.2 - - /-- A ∧ B → B ∧ A -/ - def ab_imp_ba := (Term.lam (.and (.and2 (.var 0) (.prod (.new 0) (.new 1))) (.new 1) (.and1 (.var 0) (.prod (.new 0) (.new 1))) (.new 0)) (.prod (.new 1) (.new 0)), Term.fn (.prod (.new 0) (.new 1)) (.prod (.new 1) (.new 0))) - - #guard check [] ab_imp_ba.1 ab_imp_ba.2 - - /-- ¬(A ∨ B) → ¬A -/ - def not_ab_imp_not_a := (Term.lam (.lam (.app (.var 1) (.fn (.sum (.new 0) (.new 1)) .fls) (.or (.var 0) (.new 0)) (.sum (.new 0) (.new 1))) (.fls)) (.fn (.new 0) .fls), Term.fn (.fn (.sum (.new 0) (.new 1)) .fls) (.fn (.new 0) .fls)) - - #guard check [] not_ab_imp_not_a.1 not_ab_imp_not_a.2 - - /-- A → ¬¬A -/ - def a_imp_not_not_a := (Term.lam (.lam (.app (.var 0) (.fn (.new 0) .fls) (.var 1) (.new 0)) (.fls)) (.fn (.fn (.new 0) .fls) .fls), Term.fn (.new 0) (.fn (.fn (.new 0) .fls) .fls)) - - #guard check [] a_imp_not_not_a.1 a_imp_not_not_a.2 - - /-- ¬¬¬A → ¬A -/ - def not_not_not_a_imp_not_a := (Term.lam (.lam (.app (.var 1) (.fn (.fn (.fn (.new 0) .fls) .fls) .fls) (.app a_imp_not_not_a.1 a_imp_not_not_a.2 (.var 0) (.new 0)) (.fn (.fn (.new 0) .fls) .fls)) (.fls)) (.fn (.new 0) .fls), Term.fn (.fn (.fn (.fn (.new 0) .fls) .fls) .fls) (.fn (.new 0) .fls)) - - #guard check [] not_not_not_a_imp_not_a.1 not_not_not_a_imp_not_a.2 - - /-- ∀ a : A, a = a -/ - def a_eq_a := (Term.lam (.rfl (.var 0) (.new 0)) (.eq (.var 0) (.var 0) (.new 0)), Term.fn (.new 0) (.eq (.var 0) (.var 0) (.new 0))) - - #guard check [] a_eq_a.1 a_eq_a.2 - - /-- 2 exists (yeah I know this is not super exciting) -/ - def two := (Term.succ (.succ .zero .nat) .nat, Term.nat) - - #guard check [] two.1 two.2 - - /-- 4 exists -/ - def four := (Term.succ (.succ two.1 two.2) .nat, Term.nat) - - #guard check [] four.1 four.2 - - /-- Addition -/ - def add := (Term.lam (.nat_rec .nat .zero .nat (.var 0) .nat (.lam (.lam (.succ (.var 2) .nat) .nat) (.fn .nat .nat)) (.fn .nat (.fn .nat .nat))) (.fn .nat .nat), Term.fn .nat (.fn .nat .nat)) - - #guard check [] add.1 add.2 - - def two_plus_two := (Term.app (.app add.1 add.2 two.1 two.2) (.fn .nat .nat) two.1 two.2, Term.nat) - - #guard check [] two_plus_two.1 two_plus_two.2 - - /-- 2 + 2 = 4 -/ - def two_plus_two_eq_four := (Term.fls, Term.eq two_plus_two.1 four.1 .nat) - - #guard check [] two_plus_two_eq_four.1 two_plus_two_eq_four.2