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 (Expr.plus a 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 (Expr.and a 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 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: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det
(
h₁: HasType e t₁
h₁
:
HasType: Expr → Ty → Prop
HasType
e: Expr
e
t₁: Ty
t₁
) (
h₂: HasType e t₂
h₂
:
HasType: Expr → Ty → Prop
HasType
e: Expr
e
t₂: Ty
t₂
) :
t₁: Ty
t₁
=
t₂: Ty
t₂
:=
e: Expr
t₁, t₂: Ty
h₁: HasType e t₁
h₂: HasType e t₂

t₁ = t₂
t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v) t₂

nat
Ty.nat = t₂
t₂: Ty
a✝², b✝: Expr
h₂: HasType (Expr.plus a✝² b) t₂
Ty.nat = t₂
t₂: Ty
v✝: Bool
h₂: HasType (Expr.bool v) t₂
Ty.bool = t₂
t₂: Ty
a✝², b✝: Expr
h₂: HasType (Expr.and a✝² b) t₂
Ty.bool = t₂
t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v) t₂

nat
Ty.nat = t₂
t₂: Ty
a✝², b✝: Expr
h₂: HasType (Expr.plus a✝² b) t₂
Ty.nat = t₂
t₂: Ty
v✝: Bool
h₂: HasType (Expr.bool v) t₂
Ty.bool = t₂
t₂: Ty
a✝², b✝: Expr
h₂: HasType (Expr.and a✝² b) t₂
Ty.bool = t₂
v✝: Nat

nat.nat
Ty.nat = Ty.nat
a✝⁴, b✝: Expr

plus.plus
Ty.nat = Ty.nat

Goals accomplished! 🐙

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: {α : 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.Syntax
x
" | "
p: Lean.Syntax
p
" }}" => Maybe (fun
x: Lean.Syntax
x
=>
p: Lean.Syntax
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 }}
Expr.typeCheck
(
e: Expr
e
:
Expr: Type
Expr
) : {{
ty: Ty
ty
|
HasType: Expr → Ty → Prop
HasType
e: Expr
e
ty: Ty
ty
}} := match
e: Expr
e
with |
nat: Nat → Expr
nat
.. =>
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found
.nat: Ty
.nat
.nat: ∀ {v : Nat}, HasType (nat v) Ty.nat
.nat
|
bool: Bool → Expr
bool
.. =>
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found
.bool: Ty
.bool
.bool: ∀ {v : Bool}, HasType (bool v) Ty.bool
.bool
|
plus: Expr → Expr → Expr
plus
a: Expr
a
b: Expr
b
=> match
a: Expr
a
.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck
,
b: Expr
b
.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck
with |
.found .nat h₁: {{ ty | HasType a ty }}
.found
.nat: Ty
.nat
.found .nat h₁: {{ ty | HasType a ty }}
h₁: HasType a Ty.nat
h₁
,
.found .nat h₂: {{ ty | HasType b ty }}
.found
.nat: Ty
.nat
.found .nat h₂: {{ ty | HasType b ty }}
h₂: HasType b Ty.nat
h₂
=>
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found
.nat: Ty
.nat
(
.plus: ∀ {a b : Expr}, HasType a Ty.nat → HasType b Ty.nat → HasType (plus a b) Ty.nat
.plus
h₁: HasType a Ty.nat
h₁
h₂: HasType b Ty.nat
h₂
) | _, _ =>
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown
|
and: Expr → Expr → Expr
and
a: Expr
a
b: Expr
b
=> match
a: Expr
a
.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck
,
b: Expr
b
.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck
with |
.found .bool h₁: {{ ty | HasType a ty }}
.found
.bool: Ty
.bool
.found .bool h₁: {{ ty | HasType a ty }}
h₁: HasType a Ty.bool
h₁
,
.found .bool h₂: {{ ty | HasType b ty }}
.found
.bool: Ty
.bool
.found .bool h₂: {{ ty | HasType b ty }}
h₂: HasType b Ty.bool
h₂
=>
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found
.bool: Ty
.bool
(
.and: ∀ {a b : Expr}, HasType a Ty.bool → HasType b Ty.bool → HasType (and a b) Ty.bool
.and
h₁: HasType a Ty.bool
h₁
h₂: HasType b Ty.bool
h₂
) | _, _ =>
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown
theorem
Expr.typeCheck_correct: ∀ {e : Expr} {ty : Ty} {h : HasType e ty}, HasType e ty → typeCheck e ≠ Maybe.unknown → typeCheck e = Maybe.found ty h
Expr.typeCheck_correct
(
h₁: HasType e ty
h₁
:
HasType: Expr → Ty → Prop
HasType
e: Expr
e
ty: Ty
ty
) (
h₂: typeCheck e ≠ Maybe.unknown
h₂
:
e: Expr
e
.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown
) :
e: Expr
e
.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck
=
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found
ty: Ty
ty
h: HasType e ty
h
:=
e: Expr
ty: Ty
h, h₁: HasType e ty
h₂: typeCheck e Maybe.unknown

typeCheck e = Maybe.found ty h
e: Expr
ty: Ty
h, h₁: HasType e ty

typeCheck e Maybe.unknown typeCheck e = Maybe.found ty h
e: Expr
ty: Ty
h, h₁: HasType e ty
x✝: {{ ty | HasType e ty }}

x Maybe.unknown x = Maybe.found ty h
e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'

found
Maybe.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'

found
Maybe.found ty' h' = Maybe.found ty h
;
e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
this: ty = ty'

found
Maybe.found ty' h' = Maybe.found ty h
;
e: Expr
ty: Ty
h, h₁, h': HasType e ty

found
Maybe.found ty h' = Maybe.found ty h
;

Goals accomplished! 🐙
e: Expr
ty: Ty
h, h₁: HasType e ty

unknown
Maybe.unknown Maybe.unknown Maybe.unknown = Maybe.found ty h
e: Expr
ty: Ty
h, h₁: HasType e ty

unknown
Maybe.unknown = Maybe.found ty h
;

Goals 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 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: ∀ {ty : Ty} {e : Expr}, typeCheck e = Maybe.unknown → ¬HasType e ty
Expr.typeCheck_complete
{
e: Expr
e
:
Expr: Type
Expr
} :
e: Expr
e
.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck
=
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown
¬
HasType: Expr → Ty → Prop
HasType
e: Expr
e
ty: Ty
ty
:=
ty: Ty
e: Expr

typeCheck e = Maybe.unknown ¬HasType e ty
ty: Ty
e: Expr

typeCheck e = Maybe.unknown ¬HasType e ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty

and
(match typeCheck a, typeCheck b with | Maybe.found Ty.bool h₁, Maybe.found Ty.bool h₂ => Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool) | x, x_1 => Maybe.unknown) = Maybe.unknown ¬HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty

plus
(match typeCheck a, typeCheck b with | Maybe.found Ty.nat h₁, Maybe.found Ty.nat h₂ => Maybe.found Ty.nat (_ : HasType (plus a b) Ty.nat) | x, x_1 => Maybe.unknown) = Maybe.unknown ¬HasType (plus a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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

plus.h_1
Maybe.found Ty.nat (_ : HasType (plus a b) Ty.nat) = Maybe.unknown ¬HasType (plus a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
Maybe.unknown = Maybe.unknown ¬HasType (plus a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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

plus.h_1
Maybe.found Ty.nat (_ : HasType (plus a b) Ty.nat) = Maybe.unknown ¬HasType (plus a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
Maybe.unknown = Maybe.unknown ¬HasType (plus a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}

¬HasType (plus a b) ty
;

Goals accomplished! 🐙
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}

plus.h_2
Maybe.unknown = Maybe.unknown ¬HasType (plus a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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), typeCheck a = Maybe.found Ty.nat h₁ typeCheck b = Maybe.found Ty.nat h₂ False

Maybe.unknown = Maybe.unknown ¬HasType (plus a b) ty
Warning: unused variable `h`
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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), typeCheck a = Maybe.found Ty.nat h₁ typeCheck b = Maybe.found Ty.nat h₂ False

Maybe.unknown = Maybe.unknown ¬HasType (plus a b) ty
ht: HasType (plus a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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), typeCheck a = Maybe.found Ty.nat h₁ typeCheck b = Maybe.found Ty.nat h₂ False
h: Maybe.unknown = Maybe.unknown
ht: HasType (plus a b) ty

False
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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), typeCheck a = Maybe.found Ty.nat h₁ typeCheck b = Maybe.found Ty.nat h₂ False
h: Maybe.unknown = Maybe.unknown
ht: HasType (plus a b) ty

False
a, b: Expr
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), typeCheck a = Maybe.found Ty.nat h₁ typeCheck b = Maybe.found Ty.nat h₂ False
h: Maybe.unknown = Maybe.unknown
h₁: HasType a Ty.nat
h₂: HasType b Ty.nat
iha: typeCheck a = Maybe.unknown ¬HasType a Ty.nat
ihb: typeCheck b = Maybe.unknown ¬HasType b Ty.nat

plus
False

Goals accomplished! 🐙
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty

and
(match typeCheck a, typeCheck b with | Maybe.found Ty.bool h₁, Maybe.found Ty.bool h₂ => Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool) | x, x_1 => Maybe.unknown) = Maybe.unknown ¬HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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

and.h_1
Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool) = Maybe.unknown ¬HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
Maybe.unknown = Maybe.unknown ¬HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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

and.h_1
Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool) = Maybe.unknown ¬HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
Maybe.unknown = Maybe.unknown ¬HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}

¬HasType (and a b) ty
;

Goals accomplished! 🐙
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = Maybe.unknown ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}

and.h_2
Maybe.unknown = Maybe.unknown ¬HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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), typeCheck a = Maybe.found Ty.bool h₁ typeCheck b = Maybe.found Ty.bool h₂ False

Maybe.unknown = Maybe.unknown ¬HasType (and a b) ty
Warning: unused variable `h`
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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), typeCheck a = Maybe.found Ty.bool h₁ typeCheck b = Maybe.found Ty.bool h₂ False

Maybe.unknown = Maybe.unknown ¬HasType (and a b) ty
ht: HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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), typeCheck a = Maybe.found Ty.bool h₁ typeCheck b = Maybe.found Ty.bool h₂ False
h: Maybe.unknown = Maybe.unknown
ht: HasType (and a b) ty

False
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown ¬HasType a ty
ihb: typeCheck b = 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), typeCheck a = Maybe.found Ty.bool h₁ typeCheck b = Maybe.found Ty.bool h₂ False
h: Maybe.unknown = Maybe.unknown
ht: HasType (and a b) ty

False
a, b: Expr
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), typeCheck a = Maybe.found Ty.bool h₁ typeCheck b = Maybe.found Ty.bool h₂ False
h: Maybe.unknown = Maybe.unknown
h₁: HasType a Ty.bool
h₂: HasType b Ty.bool
iha: typeCheck a = Maybe.unknown ¬HasType a Ty.bool
ihb: typeCheck b = Maybe.unknown ¬HasType b Ty.bool

and
False

Goals 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': Expr.typeCheck e = Maybe.unknown
h'
:
e: Expr
e
.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck
with |
.found t' ht': {{ ty | HasType e ty }}
.found
t': Ty
t'
.found t' ht': {{ ty | HasType e ty }}
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: {{ ty | HasType e ty }}
.unknown
=>
isFalse: {p : Prop} → ¬p → Decidable p
isFalse
(
Expr.typeCheck_complete: ∀ {ty : Ty} {e : Expr}, Expr.typeCheck e = Maybe.unknown → ¬HasType e ty
Expr.typeCheck_complete
h': Expr.typeCheck e = Maybe.unknown
h'
)