From b2a1b88a4e98f0d447af070458e0e207f134693f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Mar 2022 19:01:26 -0700 Subject: [PATCH] doc: a certified type checker --- doc/examples.md | 1 + doc/examples/tc.lean | 116 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 117 insertions(+) create mode 100644 doc/examples/tc.lean diff --git a/doc/examples.md b/doc/examples.md index f8336fdb3f..048b51844e 100644 --- a/doc/examples.md +++ b/doc/examples.md @@ -1,4 +1,5 @@ Examples ======== +- [A Certified Type Checker](https://github.com/leanprover/lean4/blob/master/doc/examples/tc.lean) - [The Well-Typed Interpreter](https://github.com/leanprover/lean4/blob/master/doc/examples/interp.lean) diff --git a/doc/examples/tc.lean b/doc/examples/tc.lean new file mode 100644 index 0000000000..61c87f5a6c --- /dev/null +++ b/doc/examples/tc.lean @@ -0,0 +1,116 @@ +/-| +========================================== +A Certified Type Checker +========================================== + +In this tutorial, we build a certified type checker for a simple expression +language. + +Remark: this tutorial is based on an example in the book [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/) by Adam Chlipala. +-/ +inductive Expr where + | nat : Nat → Expr + | plus : Expr → Expr → Expr + | bool : Bool → Expr + | and : Expr → Expr → Expr + +/-| +We define a simple language of types using the inductive datatype `Ty`, and +its typing rules using the inductive predicate `HasType`. +-/ +inductive Ty where + | nat + | bool + deriving DecidableEq + +inductive HasType : Expr → Ty → Prop + | nat : HasType (.nat v) .nat + | plus : HasType a .nat → HasType b .nat → HasType (.plus a b) .nat + | bool : HasType (.bool v) .bool + | and : HasType a .bool → HasType b .bool → HasType (.and a b) .bool + +/-| +We can easily show that if `e` has type `t₁` and type `t₂`, then `t₁` and `t₂` must be equal +by using the the `cases` tactic. This tactic creates a new subgoal for every constructor, +and automatically discharges unreachable cases. The tactic combinator `tac₁ <;> tac₂` applies +`tac₂` to each subgoal produced by `tac₁`. Then, the tactic `rfl` is used to close all produced +goals using reflexivity. +-/ +theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by + cases h₁ <;> cases h₂ <;> rfl + +/-| +The inductive type `Maybe p` has two contructors: `found a h` and `unknown`. +The former contains an element `a : α` and a proof that `a` satisfies the predicate `p`. +The constructor `unknown` is used to encode "failure". +-/ + +inductive Maybe (p : α → Prop) where + | found : (a : α) → p a → Maybe p + | unknown + +/-| +We define a notation for `Maybe` that is similar to the builtin notation for the Lean builtin type `Subtype`. +-/ +notation "{{ " x " | " p " }}" => Maybe (fun x => p) + +/-| +The function `Expr.typeCheck e` returns a type `ty` and a proof that `e` has type `ty`, +or `unknown`. +Recall that, `def Expr.typeCheck ...` in Lean is notation for `namespace Expr def typeCheck ... end Expr`. +The term `.found .nat .nat` is sugar for `Maybe.found Ty.nat HasType.nat`. Lean can infer the namespaces using +the expected types. +-/ +def Expr.typeCheck (e : Expr) : {{ ty | HasType e ty }} := + match e with + | nat .. => .found .nat .nat + | bool .. => .found .bool .bool + | plus a b => + match a.typeCheck, b.typeCheck with + | .found .nat h₁, .found .nat h₂ => .found .nat (.plus h₁ h₂) + | _, _ => .unknown + | and a b => + match a.typeCheck, b.typeCheck with + | .found .bool h₁, .found .bool h₂ => .found .bool (.and h₁ h₂) + | _, _ => .unknown + + +-- TODO: for simplifying the following proof we need: ematching for forward reasoning, and `match` blast for case analysis +/-| +Now, we prove that if `Expr.typeCheck e` returns `Maybe.unknown`, then forall `ty`, `HasType e ty` does not hold. +The notation `e.typeCheck` is sugar for `Expr.typeCheck e`. Lean can infer this because we explicitly said that `e` has type `Expr`. +The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to to rename "inaccessible" variables. +We say a variable is inaccessible if it is introduced by a tactic (e.g., `cases`) or has been shadowed by another variable introduced +by the user. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes +the cases corresponding to the constructors `Expr.nat` and `Expr.bool`. +-/ +theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := by + induction e with simp [typeCheck] + | plus a b iha ihb => + revert iha ihb + cases typeCheck a <;> cases typeCheck b <;> simp <;> intros <;> intro h <;> cases h <;> try contradiction + rename_i ty₁ _ ty₂ _ h _ _ + cases ty₁ <;> cases ty₂ <;> simp at h + . have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction + . have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction + . have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction + | and a b iha ihb => + revert iha ihb + cases typeCheck a <;> cases typeCheck b <;> simp <;> intros <;> intro h <;> cases h <;> try contradiction + rename_i ty₁ _ ty₂ _ h _ _ + cases ty₁ <;> cases ty₂ <;> simp at h + . have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction + . have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction + . have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction + +/-| +Finally, we show that type checking for `e` can be decided using `Expr.typeCheck`. +-/ +instance (e : Expr) (t : Ty) : Decidable (HasType e t) := + match h' : e.typeCheck with + | .found t' ht' => + if heq : t = t' then + isTrue (heq ▸ ht') + else + isFalse fun ht => heq (HasType.det ht ht') + | .unknown => isFalse (Expr.typeCheck_complete h')