Better docs, implement negation

Changes

6 changed files (+86/-38)

• .gitignore (new)
  • @@ -0,0 +1,1 @@
    + /.lake
• Main.lean
  • @@ -1,48 +1,80 @@
    import Std.Data.HashMap + -- A type checker for simply typed lambda calculus (equivalent to propositional logic) + + /-- + Types in our toy language + + We use Greek letters for variables with type `Typ` + -/ inductive Typ - | var : String → Typ + /-- New named type -/ + | new : String → Typ + /-- Function type -/ | fn : Typ → Typ → Typ + /-- Product type -/ | prod : Typ → Typ → Typ + /-- Sum type -/ | sum : Typ → Typ → Typ + /-- False (no terms of this type) -/ + | fls : Typ deriving BEq + /-- Terms in our toy language -/ inductive Term - | var : Typ → String → Term - | fn : Typ → String → Term → Term - | app : Typ → Term → Term → Term - | prod : Typ → Term → Term → Term - | sum : Typ → Term → Term → Term - - def Term.getTyp : Term → Typ - | .var τ _ => τ - | .fn τ _ _ => τ - | .app τ _ _ => τ - | .prod τ _ _ => τ - | .sum τ _ _ => τ - - def check (env : Std.HashMap String Typ) : Term → Bool - | .var τ x => + /-- Variable -/ + | var : String → Term + /-- Lambda -/ + | lam : String → Typ × Term → Term + /-- Function application -/ + | app : Typ × Term → Typ × Term → Term + /-- Construct a product -/ + | and : Typ × Term → Typ × Term → Term + /-- Get first element of product -/ + | and1 : Typ × Term → Term + /-- Get second element of product -/ + | and2 : Typ × Term → Term + /-- Construct a sum -/ + | or : Typ × Term → Term + + -- TODO: Convert `Term` into Lurk s-expression + + /-- + The type checker! + + TODO: Port to Lurk + -/ + def check (env : Std.HashMap String Typ) : Typ → Term → Bool + | τ, .var x => (· == τ) <$> env[x]? |>.getD false - | .fn τ x b => - match τ with - | .fn α β => b.getTyp == β && check (env.insert x α) b - | _ => false - | .app τ f x => - match f.getTyp with - | .fn α β => x.getTyp == α && β == τ && check env f && check env x - | _ => false - | .prod τ x y => - match τ with - | .prod α β => - x.getTyp == α && y.getTyp == β && check env x && check env y - | _ => false - | .sum τ x y => - match τ with - | .sum α β => - x.getTyp == α && y.getTyp == β && check env x && check env y - | _ => false - - def ab_imp_ba := Term.fn (.fn (.var "A") (.fn (.var "B") (.prod (.var "B") (.var "A")))) "a" (.fn (.fn (.var "B") (.prod (.var "B") (.var "A"))) "b" (.prod (.prod (.var "B") (.var "A")) (.var (.var "B") "b") (.var (.var "A") "a"))) - - #eval check (.ofList []) ab_imp_ba + | .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 + | _, _ => false + + -- theorem false_empty (h : ∀ x, (_ : x ∈ env.keys) → env[x]'(by grind) != .fls) : check env .fls t == false := by + -- cases t <;> try grind [check] + + /-- 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")))) + + #guard check (.ofList []) a_imp_b_imp_ba.1 a_imp_b_imp_ba.2 + + /-- 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")))) + + #guard check (.ofList []) ab_imp_ba.1 ab_imp_ba.2 + + /-- ¬(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"))))) + + #guard check (.ofList []) not_ab_imp_not_a.1 not_ab_imp_not_a.2
• README.md (new)
  • @@ -0,0 +1,6 @@
    + # 6-5610-project + + How to install Lurk: + 1. `git clone https://github.com/lurk-lab/lurk.git` + 2. `cd lurk` + 3. `cargo install --path . --locked`
• lake-manifest.json (new)
  • @@ -0,0 +1,6 @@
    + {"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "«6-5610-project»", + "lakeDir": ".lake", + "fixedToolchain": false}
• lakefile.toml (new)
  • @@ -0,0 +1,2 @@
    + name = "6-5610-project" + version = "0.1.0"
• lean-toolchain (new)
  • @@ -0,0 +1,1 @@
    + leanprover/lean4:v4.30.0-rc1