Commit more bad code

Changes

2 changed files (+337/-18)

• DependentEval.lean (new)
  • @@ -0,0 +1,312 @@
    + -- μ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 + + -- `infixr` doesn't work? + notation l " ⇨ " r => Term.fn l r + notation "λ " b:max β:max => Term.lam b β + notation "◆ " f:max φ:max a:max α:max => Term.app f φ a α + -- The `max` fixes some precedence issues when parsing or something + notation:max "’" r:max => Term.var r + notation:max "₸" r:max => Term.new r + notation "𝒰" => Term.typ + notation "⊥" => Term.fls + notation "ℕ" => Term.nat + + /-- 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) β) + | ◆ f φ a α => + ◆ (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) β) + | ◆ f φ a α => + ◆ (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 + + -- /-- -/ + -- 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 β + | ◆ 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 + -- https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types/#inductive-families + | .eq_rec, 𝒰 ⇨ ’0 ⇨ (’1 ⇨ .eq ’1 ’0 ’2 ⇨ 𝒰) ⇨ ◆ (◆ ’0 (’2 ⇨ .eq ’2 ’0 ’3 ⇨ 𝒰) ’1 ’2) (.eq ’1 ’1 ’2 ⇨ 𝒰) (◆ (◆ .rfl (𝒰 ⇨ ’0 ⇨ .eq ’0 ’0 ’1) ’2 𝒰) (’2 ⇨ .eq ’0 ’0 ’3) ’2 ’3) (.eq ’1 ’1 ’2) ⇨ ’3 ⇨ .eq ’3 ’0 ’4 ⇨ ◆ (◆ ’3 (’5 ⇨ .eq ’5 ’0 ’6 ⇨ 𝒰) ’1 ’5) (.eq ’4 ’1 ’5) ’0 (.eq ’4 ’1 ’5) + | .nat_rec, (ℕ ⇨ 𝒰) ⇨ ◆ ’0 (ℕ ⇨ 𝒰) .zero ℕ ⇨ (ℕ ⇨ ◆ ’2 (ℕ ⇨ 𝒰) ’0 ℕ ⇨ ◆ ’3 (ℕ ⇨ 𝒰) (◆ .succ (ℕ ⇨ ℕ) ’1 ℕ) ℕ) ⇨ ℕ ⇨ ◆ ’0 ℕ ’3 (ℕ ⇨ 𝒰) + | .zero, ℕ + | .succ, ℕ ⇨ ℕ + | .fls_rec, ⊥ ⇨ _ => + true + | _, _ => + false + + -- /-- `incr` preserves type -/ + -- theorem check_incr env' (h : check (env' ++ env) t τ) (hd : env'.length = d) : check (env' ++ α :: env) (incr d t) τ := by + -- match t, τ with + -- | .var x, α => + -- grind [check, incr] + -- | .lam b β, .fn α β' => + -- simp [check] at h + -- simpa [check, incr] using ⟨h.1, check_incr (α :: env') h.2 (by grind)⟩ + -- | .app f (.fn α β) a α', β' => + -- simp [check] at h + -- simpa [check, incr] using ⟨⟨h.1.1, check_incr env' h.1.2 hd⟩, check_incr env' h.2 hd⟩ + + -- /-- `sub` preserves type -/ + -- theorem check_sub env' (h : check (env' ++ σ :: env) t τ) (hn : n = env'.length) (hs : check (env' ++ env) s σ) : check (env' ++ env) (sub n s t) τ := by + -- match t, τ with + -- | .var x, α => + -- grind [check, sub] + -- | .lam (b, β), .fn α β' => + -- simp [check] at h + -- simpa [check, sub] using ⟨h.1, check_sub (α :: env') h.2 (by grind) (check_incr [] hs (by rfl))⟩ + -- | .app (f, .fn α β) (a, α'), β' => + -- simp [check] at h + -- simpa [check, sub] using ⟨⟨h.1.1, check_sub env' h.1.2 hn hs⟩, check_sub env' h.2 hn hs⟩ + + /-- Eval without worrying about types -/ + partial def eval_untyped : Term → Term + | (λ b β) => + λ (eval_untyped b) β + | ◆ f φ a α => + let a' := eval_untyped a + match eval_untyped f with + | .lam b _ => eval_untyped (sub 0 (incr 0 a') b) + | x => .app x φ a' α + | α ⇨ β => + (eval_untyped α) ⇨ (eval_untyped β) + | .prod α β => + .prod (eval_untyped α) (eval_untyped β) + -- and + -- fst + -- snd + | .sum α β => + .sum (eval_untyped α) (eval_untyped β) + -- inl + -- inr + | .eq a a' α => + .eq (eval_untyped a) (eval_untyped a') (eval_untyped α) + -- eq_rec + -- nat_rec + | x => + x + + /- + | var (x : Nat) + | lam (b β : Term) + | app (f φ a α : Term) + -- Types + | typ + | new (x : Nat) + | fn (α β : Term) + -- Inductive types + | prod (α β : Term) + | and + | fst + | snd + | sum (α β : Term) + | inl + | inr + | eq (a a' α : Term) + | rfl + | eq_rec + | nat + | zero + | succ + | nat_rec + | fls + | fls_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 + + /-- Convenience wrapper around `.and` -/ + def and a α b β := ◆ (◆ (◆ (◆ .and (𝒰 ⇨ 𝒰 ⇨ ’1 ⇨ ’1 ⇨ .prod ’3 ’3) α 𝒰) (𝒰 ⇨ α ⇨ ’1 ⇨ .prod α ’3) β 𝒰) (α ⇨ β ⇨ .prod α β) a α) (β ⇨ .prod α β) b β + + /-- A → B → A ∧ B -/ + def a_imp_b_imp_ab := (◆ (◆ .and (𝒰 ⇨ 𝒰 ⇨ ’1 ⇨ ’1 ⇨ .prod ’3 ’3) ₸0 𝒰) (𝒰 ⇨ ₸0 ⇨ ’1 ⇨ .prod ₸0 ’3) ₸1 𝒰, ₸0 ⇨ ₸1 ⇨ .prod ₸0 ₸1) + + #guard check [] a_imp_b_imp_ab.1 a_imp_b_imp_ab.2 + + /-- 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 := ◆ (◆ (◆ .fst (𝒰 ⇨ 𝒰 ⇨ .prod ’1 ’1 ⇨ ’2) α 𝒰) (𝒰 ⇨ .prod α ’1 ⇨ α) β 𝒰) (.prod α β ⇨ α) p (.prod α β) + + /-- Convenience wrapper around `.snd` -/ + def snd α β p := ◆ (◆ (◆ .snd (𝒰 ⇨ 𝒰 ⇨ .prod ’1 ’1 ⇨ ’1) α 𝒰) (𝒰 ⇨ .prod α ’1 ⇨ ’1) β 𝒰) (.prod α β ⇨ β) p (.prod α β) + + /-- 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 := ◆ (◆ (◆ .inl (𝒰 ⇨ 𝒰 ⇨ ’1 ⇨ .sum ’2 ’1) α 𝒰) (𝒰 ⇨ α ⇨ .sum α ’1) β 𝒰) (α ⇨ .sum α β) a α + + /-- ¬(A ∨ B) → ¬A -/ + def not_ab_imp_not_a := (λ (λ (◆ ’1 (.sum ₸0 ₸1 ⇨ ⊥) (inl ₸0 ₸1 ’0) (.sum ₸0 ₸1)) ⊥) (₸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 := (λ (λ (◆ ’0 (₸0 ⇨ ⊥) ’1 ₸0) ⊥) ((₸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 := (λ (λ (◆ ’1 (((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) (◆ a_imp_not_not_a.1 a_imp_not_not_a.2 ’0 ₸0) ((₸0 ⇨ ⊥) ⇨ ⊥)) ⊥) (₸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 α := ◆ (◆ .rfl (𝒰 ⇨ ’0 ⇨ .eq ’0 ’0 ’1) α 𝒰) (α ⇨ .eq ’0 ’0 α) 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 := ◆ .succ (ℕ ⇨ ℕ) n .nat + + -- /-- 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 := ◆ (◆ (◆ .nat_rec ((ℕ ⇨ 𝒰) ⇨ ◆ ’0 (ℕ ⇨ 𝒰) .zero ℕ ⇨ (ℕ ⇨ ◆ ’2 (ℕ ⇨ 𝒰) ’0 ℕ ⇨ ◆ ’3 (ℕ ⇨ 𝒰) (◆ .succ (ℕ ⇨ ℕ) ’1 ℕ) ℕ) ⇨ ℕ ⇨ ◆ ’0 ℕ ’3 (ℕ ⇨ 𝒰)) (λ ℕ 𝒰) (ℕ ⇨ 𝒰)) (ℕ ⇨ (ℕ ⇨ ℕ ⇨ ℕ) ⇨ ℕ ⇨ ℕ) z ℕ) ((ℕ ⇨ ℕ ⇨ ℕ) ⇨ ℕ ⇨ ℕ) f (ℕ ⇨ ℕ ⇨ ℕ) + + #check Nat.rec + + /-- Addition -/ + def add := (λ (nat_rec_nat ’0 (λ (λ (succ ’0) (ℕ ⇨ ℕ)) ℕ)) (ℕ ⇨ ℕ), ℕ ⇨ ℕ ⇨ ℕ) + + #guard check [] add.1 add.2 + + -- def two_plus_two := (◆ (◆ add.1 add.2 two.1 two.2) (.fn ℕ ℕ) two.1 two.2, Termℕ) + + -- #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
  • @@ -145,30 +145,37 @@ def and a α b β := Term.app (.app (.app (.app .and (𝒰 →ₘ 𝒰 →ₘ
    /-- 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 + -- 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