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.

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₂ := by
Goals accomplished! 🐙
  cases 
h₁: HasType e t₁
h₁
t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v✝) t₂
nat
Ty.nat = t₂
t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.nat
a✝: HasType b✝ Ty.nat
h₂: HasType (a✝².plus b✝) t₂
plus
Ty.nat = t₂
t₂: Ty
v✝: Bool
h₂: HasType (Expr.bool v✝) t₂
bool
Ty.bool = t₂
t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.bool
a✝: HasType b✝ Ty.bool
h₂: HasType (a✝².and b✝) t₂
and
Ty.bool = t₂ <;>
t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v✝) t₂
nat
Ty.nat = t₂
t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.nat
a✝: HasType b✝ Ty.nat
h₂: HasType (a✝².plus b✝) t₂
plus
Ty.nat = t₂
t₂: Ty
v✝: Bool
h₂: HasType (Expr.bool v✝) t₂
bool
Ty.bool = t₂
t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.bool
a✝: HasType b✝ Ty.bool
h₂: HasType (a✝².and b✝) t₂
and
Ty.bool = t₂ cases 
h₂: HasType (a✝².plus b✝) t₂
h₂
v✝: Nat
nat.nat
Ty.nat = Ty.nat <;>
v✝: Nat
nat.nat
Ty.nat = Ty.nat
a✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.nat
a✝²: HasType b✝ Ty.nat
a✝¹: HasType a✝⁴ Ty.nat
a✝: HasType b✝ Ty.nat
plus.plus
Ty.nat = Ty.nat
v✝: Bool
bool.bool
Ty.bool = Ty.bool
a✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.bool
a✝²: HasType b✝ Ty.bool
a✝¹: HasType a✝⁴ Ty.bool
a✝: HasType b✝ Ty.bool
and.and
Ty.bool = Ty.bool rfl
Goals 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.

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: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.nat: Ty
.nat 
h₁: HasType a Ty.nat
h₁, 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.nat: Ty
.nat 
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 (a.plus 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: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.bool: Ty
.bool 
h₁: HasType a Ty.bool
h₁, 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.bool: Ty
.bool 
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 (a.and 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 → e.typeCheck ≠ Maybe.unknown → e.typeCheck = Maybe.found ty h
Expr.typeCheck_correct (
h₁: HasType e ty
h₁ : 
HasType: Expr → Ty → Prop
HasType 
e: Expr
e 
ty: Ty
ty) (
h₂: e.typeCheck ≠ 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 := by
Goals accomplished! 🐙
  revert 
h₂: e.typeCheck ≠ Maybe.unknown
h₂
e: Expr
ty: Ty
h, h₁: HasType e ty
e.typeCheck ≠ Maybe.unknown → e.typeCheck = Maybe.found ty h
  cases 
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck 
e: Expr
e with
e: Expr
ty: Ty
h, h₁: HasType e ty
x✝: {{ ty | HasType e ty }}
x✝ ≠ Maybe.unknown → x✝ = Maybe.found ty h
  | 
found: {α : Sort u_1} → {p : α → Prop} → (a : α) → p a → Maybe p
found 
ty': Ty
ty' 
h': HasType e ty'
h' =>
Goals accomplished! 🐙 intro
e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
h₂✝: Maybe.found ty' h' ≠ Maybe.unknown
found
Maybe.found ty' h' = Maybe.found ty h; have := 
HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det 
h₁: HasType e ty
h₁ 
h': HasType e 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'
found
Maybe.found ty' h' = Maybe.found ty h; subst 
this: ty = ty'
this
e: Expr
ty: Ty
h, h₁, h': HasType e ty
h₂✝: Maybe.found ty h' ≠ Maybe.unknown
found
Maybe.found ty h' = Maybe.found ty h; rfl
Goals accomplished! 🐙
  | 
unknown: {α : Sort u_1} → {p : α → Prop} → Maybe p
unknown =>
Goals accomplished! 🐙 intros
e: Expr
ty: Ty
h, h₁: HasType e ty
h₂✝: Maybe.unknown ≠ Maybe.unknown
unknown
Maybe.unknown = Maybe.found ty h; contradiction
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. 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}, e.typeCheck = 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 := by
Goals accomplished! 🐙
  induction 
e: Expr
e with
ty: Ty
e: Expr
e.typeCheck = Maybe.unknown → ¬HasType e ty simp [
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck]
Goals accomplished! 🐙
  | 
plus: Expr → Expr → Expr
plus 
a: Expr
a 
b: Expr
b 
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
iha 
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
ihb =>
Goals accomplished! 🐙
    split
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₂✝
plus.h_1
Maybe.found Ty.nat ⋯ = 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 }}
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_2
Maybe.unknown = Maybe.unknown → ¬HasType (a.plus b) ty
    next =>
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₂✝
plus.h_1
Maybe.found Ty.nat ⋯ = 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 }}
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_2
Maybe.unknown = Maybe.unknown → ¬HasType (a.plus b) ty intros
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) ty; contradiction
Goals accomplished! 🐙
    next 
ra: {{ ty | HasType a ty }}
ra 
rb: {{ ty | HasType b ty }}
rb 
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
hnp =>
      -- Recall that `hnp` is a hypothesis generated by the `split` tactic
      -- that asserts the previous case was not taken
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_2
Maybe.unknown = Maybe.unknown → ¬HasType (a.plus b) ty
      intro 
h: Maybe.unknown = Maybe.unknown
h 
ht: HasType (a.plus b) ty
ht
ty: 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) ty
False
      cases 
ht: HasType (a.plus b) ty
ht with
ty: 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) ty
False
      | 
plus: ∀ {a b : Expr}, HasType a Ty.nat → HasType b Ty.nat → HasType (a.plus b) Ty.nat
plus 
h₁: HasType a✝ Ty.nat
h₁ 
h₂: HasType b✝ Ty.nat
h₂ =>
Goals accomplished! 🐙 exact 
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
hnp 
h₁: HasType a Ty.nat
h₁ 
h₂: HasType b Ty.nat
h₂ (
typeCheck_correct: ∀ {e : Expr} {ty : Ty} {h : HasType e ty}, HasType e ty → e.typeCheck ≠ Maybe.unknown → e.typeCheck = Maybe.found ty h
typeCheck_correct 
h₁: HasType a Ty.nat
h₁ (
iha: a.typeCheck = Maybe.unknown → ¬HasType a Ty.nat
iha · 
h₁: HasType a Ty.nat
h₁)) (
typeCheck_correct: ∀ {e : Expr} {ty : Ty} {h : HasType e ty}, HasType e ty → e.typeCheck ≠ Maybe.unknown → e.typeCheck = Maybe.found ty h
typeCheck_correct 
h₂: HasType b Ty.nat
h₂ (
ihb: b.typeCheck = Maybe.unknown → ¬HasType b Ty.nat
ihb · 
h₂: HasType b Ty.nat
h₂))
Goals accomplished! 🐙
  | 
and: Expr → Expr → Expr
and 
a: Expr
a 
b: Expr
b 
iha: a.typeCheck = Maybe.unknown → ¬HasType a ty
iha 
ihb: b.typeCheck = Maybe.unknown → ¬HasType b ty
ihb =>
Goals accomplished! 🐙
    split
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₂✝
and.h_1
Maybe.found Ty.bool ⋯ = 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 }}
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_2
Maybe.unknown = Maybe.unknown → ¬HasType (a.and b) ty
    next =>
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₂✝
and.h_1
Maybe.found Ty.bool ⋯ = 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 }}
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_2
Maybe.unknown = Maybe.unknown → ¬HasType (a.and b) ty intros
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) ty; contradiction
Goals accomplished! 🐙
    next 
ra: {{ ty | HasType a ty }}
ra 
rb: {{ ty | HasType b ty }}
rb 
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
hnp =>
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_2
Maybe.unknown = Maybe.unknown → ¬HasType (a.and b) ty
      intro 
h: Maybe.unknown = Maybe.unknown
h 
ht: HasType (a.and b) ty
ht
ty: 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) ty
False
      cases 
ht: HasType (a.and b) ty
ht with
ty: 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) ty
False
      | 
and: ∀ {a b : Expr}, HasType a Ty.bool → HasType b Ty.bool → HasType (a.and b) Ty.bool
and 
h₁: HasType a✝ Ty.bool
h₁ 
h₂: HasType b✝ Ty.bool
h₂ =>
Goals accomplished! 🐙  exact 
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
hnp 
h₁: HasType a Ty.bool
h₁ 
h₂: HasType b Ty.bool
h₂ (
typeCheck_correct: ∀ {e : Expr} {ty : Ty} {h : HasType e ty}, HasType e ty → e.typeCheck ≠ Maybe.unknown → e.typeCheck = Maybe.found ty h
typeCheck_correct 
h₁: HasType a Ty.bool
h₁ (
iha: a.typeCheck = Maybe.unknown → ¬HasType a Ty.bool
iha · 
h₁: HasType a Ty.bool
h₁)) (
typeCheck_correct: ∀ {e : Expr} {ty : Ty} {h : HasType e ty}, HasType e ty → e.typeCheck ≠ Maybe.unknown → e.typeCheck = Maybe.found ty h
typeCheck_correct 
h₂: HasType b Ty.bool
h₂ (
ihb: b.typeCheck = Maybe.unknown → ¬HasType b Ty.bool
ihb · 
h₂: HasType b Ty.bool
h₂))
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': 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: {{ ty | HasType e ty }}
.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')