Swap Term and Typ to match the usual convention

Changes

2 changed files (+89/-77)

• Main.lean
  • @@ -29,32 +29,30 @@ deriving BEq
    Terms in our toy language We hardcode all the inductive type constructors and eliminators here instead of implementing them separately as axioms (which would significantly simplify the type checker) to prevent adversies from writing fake proofs that use arbitrary axioms - - The other advantage of that approach is that it enables us to write an evaluator for this toy language, which admittedly isn't very useful -/ inductive Term /-- Variable -/ | var : String → Term /-- Lambda -/ - | lam : String → Typ × Term → Term + | lam : String → Term × Typ → Term /-- Function application -/ - | app : Typ × Term → Typ × Term → Term + | app : Term × Typ → Term × Typ → Term /-- Construct a product -/ - | and : Typ × Term → Typ × Term → Term + | and : Term × Typ → Term × Typ → Term /-- Get first element of product -/ - | and1 : Typ × Term → Term + | and1 : Term × Typ → Term /-- Get second element of product -/ - | and2 : Typ × Term → Term + | and2 : Term × Typ → Term /-- Construct a sum -/ - | or : Typ × Term → Term + | or : Term × Typ → Term /-- Zero as a nat -/ | zero : Term /-- One or greater as a nat -/ - | succ : Typ × Term → Term + | succ : Term × Typ → Term /-- Eliminator (recursor) for nats -/ - | nat_elim : Typ → Typ × Term → Typ × Term → Typ × Term → Term + | nat_elim : Typ → Term × Typ → Term × Typ → Term × Typ → Term /-- Eliminator for false -/ - | fls_elim : Typ × Term → Term + | fls_elim : Term × Typ → Term def Typ.toString : Typ → String | new α => s!"(list 0n \"{α}\")"
  • @@ -67,112 +65,119 @@ def Typ.toString : Typ → String
    instance : ToString Typ := ⟨Typ.toString⟩ mutual - def toString (t : Typ × Term) := s!"(cons {t.1} {t.2.toString})" + def toString (t : Term × Typ) := s!"(cons {t.1.toString} {t.2})" def Term.toString : Term → String | .var x => s!"(list 10n '{x})" | .lam x b => s!"(list 11n '{x} {toString b})" - | .app f x => s!"(list 12n {toString f} {toString x})" + | .app f a => s!"(list 12n {toString f} {toString a})" | .and x y => s!"(list 13n {toString x} {toString y})" | .and1 x => s!"(list 14n {toString x})" - | .and2 y => s!"(list 15n {toString y})" + | .and2 x => s!"(list 15n {toString x})" | .or z => s!"(list 16n {toString z})" | .zero => s!"'(17n)" - | .succ x => s!"(list 18n {toString x})" - | .nat_elim τ a b c => s!"(list 19n {τ} {toString a} {toString b} {toString c})" + | .succ n => s!"(list 18n {toString n})" + | .nat_elim α n x f => s!"(list 19n {α} {toString n} {toString x} {toString f})" | .fls_elim x => s!"(list 20n {toString x})" end - instance : ToString (Typ × Term) := ⟨toString⟩ + instance : ToString (Term × Typ) := ⟨toString⟩ instance : ToString Term := ⟨Term.toString⟩ /-- The type checker! - TODO: Port to Lurk + The variable names are chosen intentionally so that i.e. `a : Term` corresponds to `α : Typ`. -/ - def check (env : Std.HashMap String Typ) : Typ → Term → Bool - | τ, .var x => - (· == τ) <$> env[x]? |>.getD false - | .fn α β, .lam x (β', b) => - β' == β && check (env.insert x α) β' b - | τ, .app (.fn α β, f) (α', x) => - α' == α && β == τ && check env (.fn α β) f && check env α' x - | .prod α β, .and (α', x) (β', y) => - α' == α && β' == β && check env α' x && check env β' y - | τ, .and1 (.prod α β, x) => - τ == α && check env (.prod α β) x - | τ, .and2 (.prod α β, y) => - τ == β && check env (.prod α β) y - | .sum α β, .or (γ, z) => - (γ == α || γ == β) && check env γ z - | .nat, .zero => + def check (env : Std.HashMap String Typ) : Term → Typ → Bool + | .var x, α => + (· == α) <$> env[x]? |>.getD false + | .lam x (b, β), .fn α β' => + β' == β && check (env.insert x α) b β + | .app (f, .fn α β) (a, α'), β' => + α' == α && β' == β && check env f (.fn α β) && check env a α + | .and (a, α) (b, β), .prod α' β' => + α' == α && β' == β && check env a α && check env b β + | .and1 (x, .prod α β), α' => + α' == α && check env x (.prod α β) + | .and2 (x, .prod α β), β' => + β' == β && check env x (.prod α β) + | .or (c, γ), .sum α β => + (γ == α || γ == β) && check env c γ + | .zero, .nat => true - | .nat, .succ (α, x) => - α == .nat && check env α x - | .fn .nat τ, .nat_elim α (.nat, a) (β, b) (.fn .nat (.fn γ δ), c) => - τ == α && τ == β && τ == γ && τ == δ && check env .nat a && check env β b && check env (.fn .nat (.fn γ δ)) c - | _, .fls_elim (.fls, _) => + | .succ (n, .nat), .nat => + check env n .nat + | .nat_elim α (n, .nat) (b, β) (f, .fn .nat (.fn γ δ)), .fn .nat τ => + τ == α && τ == β && τ == γ && τ == δ && check env n .nat && check env b β && check env f (.fn .nat (.fn γ δ)) + | .fls_elim (_, .fls), _ => true | _, _ => false - theorem false_empty : check (.ofList []) .fls t == false := by + theorem false_empty : check (.ofList []) t .fls == false := by sorry -- TODO: Implement eval so we can state 2 + 2 = 4 - -- def eval env (venv : Std.HashMap String Term) τ t (h : check env τ t) (henv : ∀ x, x ∈ env.keys → x ∈ venv.keys) : Term := - -- match τ, t with - -- | _, .var x => - -- venv[x]'(by sorry) - -- | .fn α β, .lam x (β', b) => - -- .lam x (eval (env.insert x α) venv β b (by sorry) (by sorry)) - -- | .app (.fn α β, f) (α', x) => - -- eval - - def a_imp_a := (Typ.fn (.new "A") (.new "A"), Term.lam "a" (.new "A", .var "a")) + -- def eval env (venv : Std.HashMap String Term) t τ (h : check env t τ) (henv : ∀ x, x ∈ venv.keys → x ∈ env.keys) : Term × Typ := + -- match t, τ with + -- | .var x, _ => + -- (venv[x]'(by sorry), env[x]'(by sorry)) + -- | .lam f (b, β'), .fn α β => + -- (.lam f (eval (env.insert f α) venv b β (by sorry) (by sorry)), .fn α β) + -- | .app (f, .fn α β) (a, α'), β' => + -- let (a', α'') := eval env venv a α h henv + -- let (f', _) := eval env venv f (.fn α β) h henv + -- match f' with + -- | .lam x (b, β'') => eval (env.insert x α) (venv.insert x a') b β (by sorry) (by sorry) + -- | _ => nofun + -- | .and (a, α) (b, β), τ => + -- (.and (eval env venv a α (by sorry) henv) (eval env venv b β (by sorry) henv), τ) + + + def a_imp_a := (Term.lam "a" (.var "a", .new "A"), Typ.fn (.new "A") (.new "A")) #guard check (.ofList []) a_imp_a.1 a_imp_a.2 #eval IO.println a_imp_a /-- A → B → B ∧ A -/ - def a_imp_b_imp_ba := (Typ.fn (.new "A") (.fn (.new "B") (.prod (.new "B") (.new "A"))), Term.lam "a" (.fn (.new "B") (.prod (.new "B") (.new "A")), .lam "b" (.prod (.new "B") (.new "A"), .and (.new "B", .var "b") (.new "A", .var "a")))) + def a_imp_b_imp_ba := (Term.lam "a" (.lam "b" (.and (.var "b", .new "B") (.var "a", .new "A"), .prod (.new "B") (.new "A")), .fn (.new "B") (.prod (.new "B") (.new "A"))), Typ.fn (.new "A") (.fn (.new "B") (.prod (.new "B") (.new "A")))) #guard check (.ofList []) a_imp_b_imp_ba.1 a_imp_b_imp_ba.2 #eval IO.println a_imp_b_imp_ba /-- A ∧ B → B ∧ A -/ - def ab_imp_ba := (Typ.fn (.prod (.new "A") (.new "B")) (.prod (.new "B") (.new "A")), Term.lam "ab" (.prod (.new "B") (.new "A"), .and (.new "B", .and2 (.prod (.new "A") (.new "B"), .var "ab")) (.new "A", .and1 (.prod (.new "A") (.new "B"), .var "ab")))) + def ab_imp_ba := (Term.lam "ab" (.and (.and2 (.var "ab", .prod (.new "A") (.new "B")), .new "B") (.and1 (.var "ab", .prod (.new "A") (.new "B")), .new "A"), .prod (.new "B") (.new "A")), Typ.fn (.prod (.new "A") (.new "B")) (.prod (.new "B") (.new "A"))) #guard check (.ofList []) ab_imp_ba.1 ab_imp_ba.2 #eval IO.println ab_imp_ba /-- ¬(A ∨ B) → ¬A -/ - def not_ab_imp_not_a := (Typ.fn (.fn (.sum (.new "A") (.new "B")) .fls) (.fn (.new "A") .fls), Term.lam "f" (.fn (.new "A") .fls, .lam "x" (.fls, .app (.fn (.sum (.new "A") (.new "B")) .fls, .var "f") (.sum (.new "A") (.new "B"), .or (.new "A", .var "x"))))) + def not_ab_imp_not_a := (Term.lam "f" (.lam "a" (.app (.var "f", .fn (.sum (.new "A") (.new "B")) .fls) (.or (.var "a", .new "A"), .sum (.new "A") (.new "B")), .fls), .fn (.new "A") .fls), Typ.fn (.fn (.sum (.new "A") (.new "B")) .fls) (.fn (.new "A") .fls)) #guard check (.ofList []) not_ab_imp_not_a.1 not_ab_imp_not_a.2 #eval IO.println not_ab_imp_not_a /-- 2 exists (yeah I know this is not super exciting) -/ - def two := (Typ.nat, Term.succ (.nat, (.succ (.nat, .zero)))) + def two := (Term.succ ((.succ (.zero, .nat)), .nat), Typ.nat) #guard check (.ofList []) two.1 two.2 /-- 4 exists -/ - def four := (Typ.nat, Term.succ (.nat, (.succ two))) + def four := (Term.succ (.succ two, .nat), Typ.nat) #guard check (.ofList []) four.1 four.2 /-- Addition -/ - def add := (Typ.fn .nat (.fn .nat .nat), Term.lam "a" (.fn .nat .nat, .nat_elim .nat (.nat, .zero) (.nat, .var "a") (.fn .nat (.fn .nat .nat), .lam "_" (.fn .nat .nat, .lam "b" (.nat, .succ (.nat, .var "b")))))) + def add := (Term.lam "a" (.nat_elim .nat (.zero, .nat) (.var "a", .nat) (.lam "_" (.lam "b" (.succ (.var "b", .nat), .nat), .fn .nat .nat), .fn .nat (.fn .nat .nat)), .fn .nat .nat), Typ.fn .nat (.fn .nat .nat)) #guard check (.ofList []) add.1 add.2 - def two_plus_two := (Typ.nat, Term.app (.fn .nat .nat, .app add two) two) + def two_plus_two := (Term.app (.app add two, .fn .nat .nat) two, Typ.nat) #guard check (.ofList []) two_plus_two.1 two_plus_two.2
• main.lurk
  • @@ -21,47 +21,54 @@
    ;; NEED defrec instead of def for recursive functions ;; TODO: Implement nats - !(defrec check (lambda (env typ term) + !(defrec check (lambda (env term typ) + ;; Variable (if (= (car term) 10n) (eq typ (eval (arg1 term) env)) - (if (and (= (car typ) 1n) (= (car term) 11n)) - (and (eq (arg2 typ) (arg2a term)) + ;; Lambda + (if (and (= (car term) 11n) (= (car typ) 1n)) + (and (eq (arg2 typ) (arg2b term)) ;; Crazy eval magic (check (eval (list 'let (list (list (arg1 term) (list 'quote (arg1 typ)))) '(current-env)) env) (arg2a term) (arg2b term))) - (if (and (= (car term) 12n) (= (car (arg1a term)) 1n)) - (and (eq (arg1 (arg1a term)) (arg2a term)) (and (eq (arg2 (arg1a term)) typ) - (and (check env (arg1a term) (arg1b term)) - (check env (arg2a term) (arg2b term))))) - (if (and (= (car typ) 2n) (= (car term) 13n)) - (and (eq (arg1a term) (arg1 typ)) (and (eq (arg2a term) (arg2 typ)) + ;; Application + (if (and (= (car term) 12n) (= (car (arg1b term)) 1n)) + (and (eq (arg1 (arg1b term)) (arg2b term)) (and (eq (arg2 (arg1b term)) typ) (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term))))) - (if (and (= (car term) 14n) (= (car (arg1a term)) 2n)) - (and (eq (arg1 (arg1a term)) typ) + ;; And + (if (and (= (car term) 13n) (= (car typ) 2n)) + (and (eq (arg1b term) (arg1 typ)) (and (eq (arg2b term) (arg2 typ)) + (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term))))) + ;; And1 + (if (and (= (car term) 14n) (= (car (arg1b term)) 2n)) + (and (eq (arg1 (arg1b term)) typ) (check env (arg1a term) (arg1b term))) - (if (and (= (car term) 15n) (= (car (arg1a term)) 2n)) - (and (eq (arg2 (arg1a term)) typ) + ;; And2 + (if (and (= (car term) 15n) (= (car (arg1b term)) 2n)) + (and (eq (arg2 (arg1b term)) typ) (check env (arg1a term) (arg1b term))) - (if (and (= (car typ) 3n) (= (car term) 16n)) - (and (or (eq (arg1a term) (arg1 typ)) (eq (arg1a term) (arg2 typ))) + ;; Or + (if (and (= (car term) 16n) (= (car typ) 3n)) + (and (or (eq (arg1b term) (arg1 typ)) (eq (arg1b term) (arg2 typ))) (check env (arg1a term) (arg1b term))) - (if (and (= (car term) 20n) (eq (car (arg1a term)))) + ;; False elim + (if (and (= (car term) 20n) (eq (car (arg1b term)) 5n)) t nil)))))))))) ; Autogenerated by Main.lean - !(def a_imp_a (cons (list 1n (list 0n "A") (list 0n "A")) (list 11n 'a (cons (list 0n "A") (list 10n 'a))))) + !(def a_imp_a (cons (list 11n 'a (cons (list 10n 'a) (list 0n "A"))) (list 1n (list 0n "A") (list 0n "A")))) (check (empty-env) (car a_imp_a) (cdr a_imp_a)) - !(def a_imp_b_imp_ba (cons (list 1n (list 0n "A") (list 1n (list 0n "B") (list 2n (list 0n "B") (list 0n "A")))) (list 11n 'a (cons (list 1n (list 0n "B") (list 2n (list 0n "B") (list 0n "A"))) (list 11n 'b (cons (list 2n (list 0n "B") (list 0n "A")) (list 13n (cons (list 0n "B") (list 10n 'b)) (cons (list 0n "A") (list 10n 'a))))))))) + !(def a_imp_b_imp_ba (cons (list 11n 'a (cons (list 11n 'b (cons (list 13n (cons (list 10n 'b) (list 0n "B")) (cons (list 10n 'a) (list 0n "A"))) (list 2n (list 0n "B") (list 0n "A")))) (list 1n (list 0n "B") (list 2n (list 0n "B") (list 0n "A"))))) (list 1n (list 0n "A") (list 1n (list 0n "B") (list 2n (list 0n "B") (list 0n "A")))))) (check (empty-env) (car a_imp_b_imp_ba) (cdr a_imp_b_imp_ba)) - !(def ab_imp_ba (cons (list 1n (list 2n (list 0n "A") (list 0n "B")) (list 2n (list 0n "B") (list 0n "A"))) (list 11n 'ab (cons (list 2n (list 0n "B") (list 0n "A")) (list 13n (cons (list 0n "B") (list 15n (cons (list 2n (list 0n "A") (list 0n "B")) (list 10n 'ab)))) (cons (list 0n "A") (list 14n (cons (list 2n (list 0n "A") (list 0n "B")) (list 10n 'ab))))))))) + !(def ab_imp_ba (cons (list 11n 'ab (cons (list 13n (cons (list 15n (cons (list 10n 'ab) (list 2n (list 0n "A") (list 0n "B")))) (list 0n "B")) (cons (list 14n (cons (list 10n 'ab) (list 2n (list 0n "A") (list 0n "B")))) (list 0n "A"))) (list 2n (list 0n "B") (list 0n "A")))) (list 1n (list 2n (list 0n "A") (list 0n "B")) (list 2n (list 0n "B") (list 0n "A"))))) (check (empty-env) (car ab_imp_ba) (cdr ab_imp_ba)) - !(def not_ab_imp_not_a (cons (list 1n (list 1n (list 3n (list 0n "A") (list 0n "B")) '(5n)) (list 1n (list 0n "A") '(5n))) (list 11n 'f (cons (list 1n (list 0n "A") '(5n)) (list 11n 'x (cons '(5n) (list 12n (cons (list 1n (list 3n (list 0n "A") (list 0n "B")) '(5n)) (list 10n 'f)) (cons (list 3n (list 0n "A") (list 0n "B")) (list 16n (cons (list 0n "A") (list 10n 'x))))))))))) + !(def not_ab_imp_not_a (cons (list 11n 'f (cons (list 11n 'a (cons (list 12n (cons (list 10n 'f) (list 1n (list 3n (list 0n "A") (list 0n "B")) '(5n))) (cons (list 16n (cons (list 10n 'a) (list 0n "A"))) (list 3n (list 0n "A") (list 0n "B")))) '(5n))) (list 1n (list 0n "A") '(5n)))) (list 1n (list 1n (list 3n (list 0n "A") (list 0n "B")) '(5n)) (list 1n (list 0n "A") '(5n))))) (check (empty-env) (car not_ab_imp_not_a) (cdr not_ab_imp_not_a))