A Certified Type Checker
In this example, we build a certified type checker for a simple expression language.
Remark: this example is based on an example in the book Certified Programming with Dependent Types by Adam Chlipala.
inductive Expr: Type
Expr where
| nat: Nat → Expr
nat : Nat: Type
Nat → Expr: Type
Expr
| plus: Expr → Expr → Expr
plus : Expr: Type
Expr → Expr: Type
Expr → Expr: Type
Expr
| bool: Bool → Expr
bool : Bool: Type
Bool → Expr: Type
Expr
| and: Expr → Expr → Expr
and : Expr: Type
Expr → Expr: Type
Expr → Expr: Type
Expr
We define a simple language of types using the inductive datatype Ty
, and
its typing rules using the inductive predicate HasType
.
inductive Ty: Type
Ty where
| nat: Ty
nat
| bool: Ty
bool
deriving DecidableEq: Sort u → Sort (max 1 u)
DecidableEq
inductive HasType: Expr → Ty → Prop
HasType : Expr: Type
Expr → Ty: Type
Ty → Prop: Type
Prop
| nat: ∀ {v : Nat}, HasType (Expr.nat v) Ty.nat
nat : HasType: Expr → Ty → Prop
HasType (.nat: Nat → Expr
.nat v: Nat
v) .nat: Ty
.nat
| plus: ∀ {a b : Expr}, HasType a Ty.nat → HasType b Ty.nat → HasType (a.plus b) Ty.nat
plus : HasType: Expr → Ty → Prop
HasType a: Expr
a .nat: Ty
.nat → HasType: Expr → Ty → Prop
HasType b: Expr
b .nat: Ty
.nat → HasType: Expr → Ty → Prop
HasType (.plus: Expr → Expr → Expr
.plus a: Expr
a b: Expr
b) .nat: Ty
.nat
| bool: ∀ {v : Bool}, HasType (Expr.bool v) Ty.bool
bool : HasType: Expr → Ty → Prop
HasType (.bool: Bool → Expr
.bool v: Bool
v) .bool: Ty
.bool
| and: ∀ {a b : Expr}, HasType a Ty.bool → HasType b Ty.bool → HasType (a.and b) Ty.bool
and : HasType: Expr → Ty → Prop
HasType a: Expr
a .bool: Ty
.bool → HasType: Expr → Ty → Prop
HasType b: Expr
b .bool: Ty
.bool → HasType: Expr → Ty → Prop
HasType (.and: Expr → Expr → Expr
.and a: Expr
a b: Expr
b) .bool: Ty
.bool
We can easily show that if e
has type t₁
and type t₂
, then t₁
and t₂
must be equal
by using 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.
theoremHasType.det (HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂h₁ :h₁: HasType e t₁HasTypeHasType: Expr → Ty → Propee: Exprt₁) (t₁: Tyh₂ :h₂: HasType e t₂HasTypeHasType: Expr → Ty → Propee: Exprt₂) :t₂: Tyt₁ =t₁: Tyt₂ :=t₂: TyGoals accomplished! 🐙t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v✝) t₂
natTy.nat = t₂t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.nat
a✝: HasType b✝ Ty.nat
h₂: HasType (a✝².plus b✝) t₂Ty.nat = t₂t₂: Ty
v✝: Bool
h₂: HasType (Expr.bool v✝) t₂Ty.bool = t₂t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.bool
a✝: HasType b✝ Ty.bool
h₂: HasType (a✝².and b✝) t₂Ty.bool = t₂t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v✝) t₂
natTy.nat = t₂t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.nat
a✝: HasType b✝ Ty.nat
h₂: HasType (a✝².plus b✝) t₂Ty.nat = t₂t₂: Ty
v✝: Bool
h₂: HasType (Expr.bool v✝) t₂Ty.bool = t₂t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.bool
a✝: HasType b✝ Ty.bool
h₂: HasType (a✝².and b✝) t₂Ty.bool = t₂a✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.nat
a✝²: HasType b✝ Ty.nat
a✝¹: HasType a✝⁴ Ty.nat
a✝: HasType b✝ Ty.nat
plus.plusTy.nat = Ty.natv✝: Nat
nat.natTy.nat = Ty.nata✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.nat
a✝²: HasType b✝ Ty.nat
a✝¹: HasType a✝⁴ Ty.nat
a✝: HasType b✝ Ty.natTy.nat = Ty.natv✝: BoolTy.bool = Ty.boola✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.bool
a✝²: HasType b✝ Ty.bool
a✝¹: HasType a✝⁴ Ty.bool
a✝: HasType b✝ Ty.boolTy.bool = Ty.boolGoals accomplished! 🐙
The inductive type Maybe p
has two constructors: 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: {α : Sort u_1} → (α → Prop) → Sort (max 1 u_1)
Maybe (p: α → Prop
p : α: Sort u_1
α → Prop: Type
Prop) where
| found: {α : Sort u_1} → {p : α → Prop} → (a : α) → p a → Maybe p
found : (a: α
a : α: Sort u_1
α) → p: α → Prop
p a: α
a → Maybe: {α : Sort u_1} → (α → Prop) → Sort (max 1 u_1)
Maybe p: α → Prop
p
| unknown: {α : Sort u_1} → {p : α → Prop} → Maybe p
unknown
We define a notation for Maybe
that is similar to the builtin notation for the Lean builtin type Subtype
.
notation "{{ " x: Lean.TSyntax `term
x " | " p: Lean.TSyntax `term
p " }}" => Maybe: {α : Sort u_1} → (α → Prop) → Sort (max 1 u_1)
Maybe (fun x: Lean.TSyntax `term
x => p: Lean.TSyntax `term
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.
defExpr.typeCheck (Expr.typeCheck: (e : Expr) → {{ ty | HasType e ty }}e :e: ExprExpr) : {{Expr: Typety |ty: TyHasTypeHasType: Expr → Ty → Propee: Exprty }} := matchty: Tye with |e: Exprnat .. =>nat: Nat → Expr.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.nat.nat: Ty.nat |.nat: ∀ {v : Nat}, HasType (nat v) Ty.natbool .. =>bool: Bool → Expr.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.bool.bool: Ty.bool |.bool: ∀ {v : Bool}, HasType (bool v) Ty.boolplusplus: Expr → Expr → Expraa: Exprb => matchb: Expra.a: ExprtypeCheck,typeCheck: (e : Expr) → {{ ty | HasType e ty }}b.b: ExprtypeCheck with |typeCheck: (e : Expr) → {{ ty | HasType e ty }}.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.nat.nat: Tyh₁,h₁: HasType a Ty.nat.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.nat.nat: Tyh₂ =>h₂: HasType b Ty.nat.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.nat (.nat: Ty.plus.plus: ∀ {a b : Expr}, HasType a Ty.nat → HasType b Ty.nat → HasType (a.plus b) Ty.nath₁h₁: HasType a Ty.nath₂) | _, _ =>h₂: HasType b Ty.nat.unknown |.unknown: {α : Type} → {p : α → Prop} → Maybe pandand: Expr → Expr → Expraa: Exprb => matchb: Expra.a: ExprtypeCheck,typeCheck: (e : Expr) → {{ ty | HasType e ty }}b.b: ExprtypeCheck with |typeCheck: (e : Expr) → {{ ty | HasType e ty }}.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.bool.bool: Tyh₁,h₁: HasType a Ty.bool.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.bool.bool: Tyh₂ =>h₂: HasType b Ty.bool.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.bool (.bool: Ty.and.and: ∀ {a b : Expr}, HasType a Ty.bool → HasType b Ty.bool → HasType (a.and b) Ty.boolh₁h₁: HasType a Ty.boolh₂) | _, _ =>h₂: HasType b Ty.bool.unknown theorem.unknown: {α : Type} → {p : α → Prop} → Maybe pExpr.typeCheck_correct (Expr.typeCheck_correct: ∀ {e : Expr} {ty : Ty} {h : HasType e ty}, HasType e ty → e.typeCheck ≠ Maybe.unknown → e.typeCheck = Maybe.found ty hh₁ :h₁: HasType e tyHasTypeHasType: Expr → Ty → Propee: Exprty) (ty: Tyh₂ :h₂: e.typeCheck ≠ Maybe.unknowne.e: ExprtypeCheck ≠typeCheck: (e : Expr) → {{ ty | HasType e ty }}.unknown) :.unknown: {α : Type} → {p : α → Prop} → Maybe pe.e: ExprtypeCheck =typeCheck: (e : Expr) → {{ ty | HasType e ty }}.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe ptyty: Tyh :=h: HasType e tyGoals accomplished! 🐙e: Expr
ty: Ty
h, h₁: HasType e tye.typeCheck ≠ Maybe.unknown → e.typeCheck = Maybe.found ty he: Expr
ty: Ty
h, h₁: HasType e ty
x✝: {{ ty | HasType e ty }}x✝ ≠ Maybe.unknown → x✝ = Maybe.found ty he: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
foundMaybe.found ty' h' ≠ Maybe.unknown → Maybe.found ty' h' = Maybe.found ty h;e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
h₂✝: Maybe.found ty' h' ≠ Maybe.unknown
foundMaybe.found ty' h' = Maybe.found ty h;e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
h₂✝: Maybe.found ty' h' ≠ Maybe.unknown
this: ty = ty'
foundMaybe.found ty' h' = Maybe.found ty h;e: Expr
ty: Ty
h, h₁, h': HasType e ty
h₂✝: Maybe.found ty h' ≠ Maybe.unknown
foundMaybe.found ty h' = Maybe.found ty hGoals accomplished! 🐙e: Expr
ty: Ty
h, h₁: HasType e ty
unknownMaybe.unknown ≠ Maybe.unknown → Maybe.unknown = Maybe.found ty h;e: Expr
ty: Ty
h, h₁: HasType e ty
h₂✝: Maybe.unknown ≠ Maybe.unknown
unknownMaybe.unknown = Maybe.found ty hGoals accomplished! 🐙
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 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
.
theoremExpr.typeCheck_complete {Expr.typeCheck_complete: ∀ {ty : Ty} {e : Expr}, e.typeCheck = Maybe.unknown → ¬HasType e tye :e: ExprExpr} :Expr: Typee.e: ExprtypeCheck =typeCheck: (e : Expr) → {{ ty | HasType e ty }}.unknown → ¬.unknown: {α : Type} → {p : α → Prop} → Maybe pHasTypeHasType: Expr → Ty → Propee: Exprty :=ty: TyGoals accomplished! 🐙ty: Ty
e: Expre.typeCheck = Maybe.unknown → ¬HasType e tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
plus(match a.typeCheck, b.typeCheck with | Maybe.found Ty.nat h₁, Maybe.found Ty.nat h₂ => Maybe.found Ty.nat ⋯ | x, x_1 => Maybe.unknown) = Maybe.unknown → ¬HasType (a.plus b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
plus(match a.typeCheck, b.typeCheck with | Maybe.found Ty.nat h₁, Maybe.found Ty.nat h₂ => Maybe.found Ty.nat ⋯ | x, x_1 => Maybe.unknown) = Maybe.unknown → ¬HasType (a.plus b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat
heq✝¹: a.typeCheck = Maybe.found Ty.nat h₁✝
heq✝: b.typeCheck = Maybe.found Ty.nat h₂✝
plus.h_1Maybe.found Ty.nat ⋯ = Maybe.unknown → ¬HasType (a.plus b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (a.plus b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat
heq✝¹: a.typeCheck = Maybe.found Ty.nat h₁✝
heq✝: b.typeCheck = Maybe.found Ty.nat h₂✝
plus.h_1Maybe.found Ty.nat ⋯ = Maybe.unknown → ¬HasType (a.plus b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (a.plus b) ty;ty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat
heq✝¹: a.typeCheck = Maybe.found Ty.nat h₁✝
heq✝: b.typeCheck = Maybe.found Ty.nat h₂✝
a✝: Maybe.found Ty.nat ⋯ = Maybe.unknown¬HasType (a.plus b) tyGoals accomplished! 🐙ty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → False
plus.h_2Maybe.unknown = Maybe.unknown → ¬HasType (a.plus b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (a.plus b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (a.plus b) tyht: HasType (a.plus b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (a.plus b) tyFalsety: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (a.plus b) tyFalsea, b: Expr
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → False
h: Maybe.unknown = Maybe.unknown
h₁: HasType a Ty.nat
h₂: HasType b Ty.nat
iha: a.typeCheck = Maybe.unknown → ¬HasType a Ty.nat
ihb: b.typeCheck = Maybe.unknown → ¬HasType b Ty.nat
plusFalseGoals accomplished! 🐙ty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
and(match a.typeCheck, b.typeCheck with | Maybe.found Ty.bool h₁, Maybe.found Ty.bool h₂ => Maybe.found Ty.bool ⋯ | x, x_1 => Maybe.unknown) = Maybe.unknown → ¬HasType (a.and b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool
heq✝¹: a.typeCheck = Maybe.found Ty.bool h₁✝
heq✝: b.typeCheck = Maybe.found Ty.bool h₂✝
and.h_1Maybe.found Ty.bool ⋯ = Maybe.unknown → ¬HasType (a.and b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (a.and b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool
heq✝¹: a.typeCheck = Maybe.found Ty.bool h₁✝
heq✝: b.typeCheck = Maybe.found Ty.bool h₂✝
and.h_1Maybe.found Ty.bool ⋯ = Maybe.unknown → ¬HasType (a.and b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (a.and b) ty;ty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool
heq✝¹: a.typeCheck = Maybe.found Ty.bool h₁✝
heq✝: b.typeCheck = Maybe.found Ty.bool h₂✝
a✝: Maybe.found Ty.bool ⋯ = Maybe.unknown¬HasType (a.and b) tyGoals accomplished! 🐙ty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False
and.h_2Maybe.unknown = Maybe.unknown → ¬HasType (a.and b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (a.and b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (a.and b) tyht: HasType (a.and b) tyty: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (a.and b) tyFalsety: Ty
a, b: Expr
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (a.and b) tyFalsea, b: Expr
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False
h: Maybe.unknown = Maybe.unknown
h₁: HasType a Ty.bool
h₂: HasType b Ty.bool
iha: a.typeCheck = Maybe.unknown → ¬HasType a Ty.bool
ihb: b.typeCheck = Maybe.unknown → ¬HasType b Ty.bool
andFalseGoals accomplished! 🐙
Finally, we show that type checking for e
can be decided using Expr.typeCheck
.
instance: (e : Expr) → (t : Ty) → Decidable (HasType e t)
instance (e: Expr
e : Expr: Type
Expr) (t: Ty
t : Ty: Type
Ty) : Decidable: Prop → Type
Decidable (HasType: Expr → Ty → Prop
HasType e: Expr
e t: Ty
t) :=
match h': e.typeCheck = Maybe.unknown
h' : e: Expr
e.typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck with
| .found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found t': Ty
t' ht': HasType e t'
ht' =>
if heq: t = t'
heq : t: Ty
t = t': Ty
t' then
isTrue: {p : Prop} → p → Decidable p
isTrue (heq: t = t'
heq ▸ ht': HasType e t'
ht')
else
isFalse: {p : Prop} → ¬p → Decidable p
isFalse fun ht: HasType e t
ht => heq: ¬t = t'
heq (HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det ht: HasType e t
ht ht': HasType e t'
ht')
| .unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown => isFalse: {p : Prop} → ¬p → Decidable p
isFalse (Expr.typeCheck_complete: ∀ {ty : Ty} {e : Expr}, e.typeCheck = Maybe.unknown → ¬HasType e ty
Expr.typeCheck_complete h': e.typeCheck = Maybe.unknown
h')