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](http://adam.chlipala.net/cpdt/) by Adam Chlipala.

inductive
 
Expr: Type
Expr
 
where

  | 
nat: Nat → _root_.Expr
nat
  : 
Nat: Type
Nat
 → 
Expr: Sort _tmp_ind_univ_param
Expr

  | 
plus: _root_.Expr → _root_.Expr → _root_.Expr
plus
 : 
Expr: Sort _tmp_ind_univ_param
Expr
 → 
Expr: Sort _tmp_ind_univ_param
Expr
 → 
Expr: Sort _tmp_ind_univ_param
Expr

  | 
bool: Bool → _root_.Expr
bool
 : 
Bool: Type
Bool
 → 
Expr: Sort _tmp_ind_univ_param
Expr

  | 
and: _root_.Expr → _root_.Expr → _root_.Expr
and
  : 
Expr: Sort _tmp_ind_univ_param
Expr
 → 
Expr: Sort _tmp_ind_univ_param
Expr
 → 
Expr: Sort _tmp_ind_univ_param
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: _root_.Ty
nat

  | 
bool: _root_.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}, _root_.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}, _root_.HasType a Ty.nat → _root_.HasType b Ty.nat → _root_.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}, _root_.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}, _root_.HasType a Ty.bool → _root_.HasType b Ty.bool → _root_.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₂
 := 
by
e: Expr
t₁, t₂: Ty
h₁: HasType e t₁
h₂: HasType e t₂
t₁ = t₂

  
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
h₂: HasType (Expr.plus a✝² 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
h₂: HasType (Expr.and a✝² b✝) t₂
and
Ty.bool = t₂
 
<;>
e: Expr
t₁, t₂: Ty
h₁: HasType e t₁
h₂: HasType e t₂
t₁ = t₂
 
cases
 
h₂: HasType (Expr.nat v✝) t₂
h₂
bool.bool
Ty.bool = Ty.bool
 
<;>
t₂: Ty
a✝², b✝: Expr
h₂: HasType (Expr.plus a✝² b✝) t₂
plus
Ty.nat = t₂
 
rfl
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 → _root_.Maybe p
found
 : (
a: α
a
 : 
α: Sort u_1
α
) → 
p: α → Prop
p
 
a: α
a
 → 
Maybe: {α : Sort u_1} → (α → Prop) → Sort _tmp_ind_univ_param
Maybe
 
p: α → Prop
p

  | 
unknown: {α : Sort u_1} → {p : α → Prop} → _root_.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) → Maybe fun 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) → Maybe fun ty => HasType e ty
typeCheck
, 
b: Expr
b
.
typeCheck: (e : Expr) → Maybe fun 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 (plus a b) Ty.nat
.plus
 
h₁: HasType a Ty.nat
h₁
 
h₂: HasType b Ty.nat
h₂
)
    | 
_: Maybe fun ty => HasType a ty
_
, 
_: Maybe fun ty => HasType b ty
_
 => 
.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) → Maybe fun ty => HasType e ty
typeCheck
, 
b: Expr
b
.
typeCheck: (e : Expr) → Maybe fun 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 (and a b) Ty.bool
.and
 
h₁: HasType a Ty.bool
h₁
 
h₂: HasType b Ty.bool
h₂
)
    | 
_: Maybe fun ty => HasType a ty
_
, 
_: Maybe fun ty => HasType b ty
_
 => 
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.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: ∀ {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) → Maybe fun ty => HasType e ty
typeCheck
 = 
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown
 → ¬ 
HasType: Expr → Ty → Prop
HasType
 
e: Expr
e
 
ty: Ty
ty
 := 
by
ty: Ty
e: Expr
typeCheck e = Maybe.unknown → ¬HasType e ty

  
induction
 
e: Expr
e
 
with
ty: Ty
e: Expr
typeCheck e = Maybe.unknown → ¬HasType e ty
 
simp
 [
typeCheck: (e : Expr) → Maybe fun ty => HasType e ty
typeCheck
]
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

  
| plus a b iha ihb =>
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

    
revert
 
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
iha
 
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ihb
ty: Ty
a, b: Expr
plus
(typeCheck a = Maybe.unknown → ¬HasType a ty) →
  (typeCheck b = Maybe.unknown → ¬HasType b ty) →
    (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

    
cases
 
typeCheck: (e : Expr) → Maybe fun ty => HasType e ty
typeCheck
 
a: Expr
a
ty: Ty
a, b: Expr
a✝¹: Ty
a✝: HasType a a✝¹
plus.found
(Maybe.found a✝¹ a✝ = Maybe.unknown → ¬HasType a ty) →
  (typeCheck b = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.found a✝¹ 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
plus.unknown
(Maybe.unknown = Maybe.unknown → ¬HasType a ty) →
  (typeCheck b = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.unknown, 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
plus
(typeCheck a = Maybe.unknown → ¬HasType a ty) →
  (typeCheck b = Maybe.unknown → ¬HasType b ty) →
    (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
 
cases
 
typeCheck: (e : Expr) → Maybe fun ty => HasType e ty
typeCheck
 
b: Expr
b
ty: Ty
a, b: Expr
a✝¹: Ty
a✝: HasType b a✝¹
plus.unknown.found
(Maybe.unknown = Maybe.unknown → ¬HasType a ty) →
  (Maybe.found a✝¹ a✝ = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.unknown, Maybe.found a✝¹ a✝ 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
plus.unknown.unknown
(Maybe.unknown = Maybe.unknown → ¬HasType a ty) →
  (Maybe.unknown = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.unknown, Maybe.unknown 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
a✝¹: Ty
a✝: HasType a a✝¹
plus.found
(Maybe.found a✝¹ a✝ = Maybe.unknown → ¬HasType a ty) →
  (typeCheck b = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.found a✝¹ 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
 
simp
ty: Ty
a, b: Expr
a✝¹: Ty
a✝: HasType b a✝¹
plus.unknown.found
¬HasType a ty → ¬HasType (plus a b) ty
 
<;>
ty: Ty
a, b: Expr
a✝¹: Ty
a✝: HasType a a✝¹
plus.found.unknown
(Maybe.found a✝¹ a✝ = Maybe.unknown → ¬HasType a ty) →
  (Maybe.unknown = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.found a✝¹ a✝, Maybe.unknown 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
 
intros
ty: Ty
a, b: Expr
plus.unknown.unknown
¬HasType (plus a b) ty
 
<;>
ty: Ty
a, b: Expr
a✝³: Ty
a✝²: HasType a a✝³
a✝¹: Ty
a✝: HasType b a✝¹
plus.found.found
(match Maybe.found a✝³ a✝², Maybe.found a✝¹ a✝ 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
 
intro
 
h: HasType (plus a b) ty
h
ty: Ty
a, b: Expr
a✝¹: Ty
a✝: HasType b a✝¹
h: HasType (plus a b) ty
plus.unknown.found
False
 
<;>
ty: Ty
a, b: Expr
plus.unknown.unknown
¬HasType (plus a b) ty
 
cases
 
h: HasType (plus a b) ty
h
a, b: Expr
a✝³: Ty
a✝²: HasType b a✝³
plus.unknown.found.plus
False
 
<;>
ty: Ty
a, b: Expr
a✝²: Ty
a✝¹: HasType a a✝²
a✝: (match Maybe.found a✝² a✝¹, Maybe.unknown 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
h: HasType (plus a b) ty
plus.found.unknown
False
 
try
a, b: Expr
plus.unknown.unknown.plus
False
 
contradiction
Goals accomplished! 🐙

    
rename_i
 ty₁ _ ty₂ _ h _ _
a, b: Expr
ty₁: Ty
a✝³: HasType a ty₁
ty₂: Ty
a✝²: HasType b ty₂
h: (match Maybe.found ty₁ a✝³, Maybe.found ty₂ a✝² 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
plus.found.found.plus
False

    
cases
 
ty₁: Ty
ty₁
a, b: Expr
ty₂: Ty
a✝³: HasType b ty₂
a✝: HasType a Ty.nat
h: (match Maybe.found Ty.nat a✝, Maybe.found ty₂ a✝³ 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
plus.found.found.plus.nat
False
a, b: Expr
ty₂: Ty
a✝³: HasType b ty₂
a✝: HasType a Ty.bool
h: (match Maybe.found Ty.bool a✝, Maybe.found ty₂ a✝³ 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
plus.found.found.plus.bool
False
 
<;>
a, b: Expr
ty₁: Ty
a✝³: HasType a ty₁
ty₂: Ty
a✝²: HasType b ty₂
h: (match Maybe.found ty₁ a✝³, Maybe.found ty₂ a✝² 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
plus.found.found.plus
False
 
cases
 
ty₂: Ty
ty₂
a, b: Expr
a✝¹: HasType a Ty.nat
a✝: HasType b Ty.nat
h: (match Maybe.found Ty.nat a✝¹, Maybe.found Ty.nat a✝ 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
plus.found.found.plus.nat.nat
False
a, b: Expr
a✝¹: HasType a Ty.nat
a✝: HasType b Ty.bool
h: (match Maybe.found Ty.nat a✝¹, Maybe.found Ty.bool a✝ 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
plus.found.found.plus.nat.bool
False
 
<;>
a, b: Expr
ty₂: Ty
a✝³: HasType b ty₂
a✝: HasType a Ty.nat
h: (match Maybe.found Ty.nat a✝, Maybe.found ty₂ a✝³ 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
plus.found.found.plus.nat
False
 
simp
 
at
 
h: (match Maybe.found Ty.nat a✝¹, Maybe.found Ty.bool a✝ 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
h
a, b: Expr
h: True
plus.found.found.plus.nat.bool
False

    
.
a, b: Expr
h: True
plus.found.found.plus.nat.bool
False
 
have
 := 
HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det
 ‹HasType b Ty.bool› ‹HasType b Ty.nat›
a, b: Expr
h: True
this: Ty.bool = Ty.nat
plus.found.found.plus.nat.bool
False
; 
contradiction
Goals accomplished! 🐙

    
.
a, b: Expr
h: True
plus.found.found.plus.bool.nat
False
 
have
 := 
HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det
 ‹HasType a Ty.bool› ‹HasType a Ty.nat›
a, b: Expr
h: True
this: Ty.bool = Ty.nat
plus.found.found.plus.bool.nat
False
; 
contradiction
Goals accomplished! 🐙

    
.
a, b: Expr
h: True
plus.found.found.plus.bool.bool
False
 
have
 := 
HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det
 ‹HasType a Ty.bool› ‹HasType a Ty.nat›
a, b: Expr
h: True
this: Ty.bool = Ty.nat
plus.found.found.plus.bool.bool
False
; 
contradiction
Goals accomplished! 🐙

  
| and a b iha ihb =>
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

    
revert
 
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
iha
 
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ihb
ty: Ty
a, b: Expr
and
(typeCheck a = Maybe.unknown → ¬HasType a ty) →
  (typeCheck b = Maybe.unknown → ¬HasType b ty) →
    (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

    
cases
 
typeCheck: (e : Expr) → Maybe fun ty => HasType e ty
typeCheck
 
a: Expr
a
ty: Ty
a, b: Expr
a✝¹: Ty
a✝: HasType a a✝¹
and.found
(Maybe.found a✝¹ a✝ = Maybe.unknown → ¬HasType a ty) →
  (typeCheck b = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.found a✝¹ 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
and.unknown
(Maybe.unknown = Maybe.unknown → ¬HasType a ty) →
  (typeCheck b = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.unknown, 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
and
(typeCheck a = Maybe.unknown → ¬HasType a ty) →
  (typeCheck b = Maybe.unknown → ¬HasType b ty) →
    (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
 
cases
 
typeCheck: (e : Expr) → Maybe fun ty => HasType e ty
typeCheck
 
b: Expr
b
ty: Ty
a, b: Expr
a✝¹: Ty
a✝: HasType b a✝¹
and.unknown.found
(Maybe.unknown = Maybe.unknown → ¬HasType a ty) →
  (Maybe.found a✝¹ a✝ = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.unknown, Maybe.found a✝¹ a✝ 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
and.unknown.unknown
(Maybe.unknown = Maybe.unknown → ¬HasType a ty) →
  (Maybe.unknown = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.unknown, Maybe.unknown 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
a✝¹: Ty
a✝: HasType a a✝¹
and.found
(Maybe.found a✝¹ a✝ = Maybe.unknown → ¬HasType a ty) →
  (typeCheck b = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.found a✝¹ 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
 
simp
ty: Ty
a, b: Expr
a✝¹: Ty
a✝: HasType b a✝¹
and.unknown.found
¬HasType a ty → ¬HasType (and a b) ty
 
<;>
ty: Ty
a, b: Expr
a✝¹: Ty
a✝: HasType a a✝¹
and.found.unknown
(Maybe.found a✝¹ a✝ = Maybe.unknown → ¬HasType a ty) →
  (Maybe.unknown = Maybe.unknown → ¬HasType b ty) →
    (match Maybe.found a✝¹ a✝, Maybe.unknown 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
 
intros
ty: Ty
a, b: Expr
and.unknown.unknown
¬HasType (and a b) ty
 
<;>
ty: Ty
a, b: Expr
a✝¹: Ty
a✝: HasType b a✝¹
and.unknown.found
¬HasType a ty → ¬HasType (and a b) ty
 
intro
 
h: HasType (and a b) ty
h
ty: Ty
a, b: Expr
h: HasType (and a b) ty
and.unknown.unknown
False
 
<;>
ty: Ty
a, b: Expr
and.unknown.unknown
¬HasType (and a b) ty
 
cases
 
h: HasType (and a b) ty
h
a, b: Expr
and.unknown.unknown.and
False
 
<;>
ty: Ty
a, b: Expr
a✝²: Ty
a✝¹: HasType a a✝²
a✝: (match Maybe.found a✝² a✝¹, Maybe.unknown 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
h: HasType (and a b) ty
and.found.unknown
False
 
try
a, b: Expr
a✝³: Ty
a✝²: HasType b a✝³
and.unknown.found.and
False
 
contradiction
Goals accomplished! 🐙

    
rename_i
 ty₁ _ ty₂ _ h _ _
a, b: Expr
ty₁: Ty
a✝³: HasType a ty₁
ty₂: Ty
a✝²: HasType b ty₂
h: (match Maybe.found ty₁ a✝³, Maybe.found ty₂ a✝² 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
and.found.found.and
False

    
cases
 
ty₁: Ty
ty₁
a, b: Expr
ty₂: Ty
a✝³: HasType b ty₂
a✝: HasType a Ty.nat
h: (match Maybe.found Ty.nat a✝, Maybe.found ty₂ a✝³ 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
and.found.found.and.nat
False
a, b: Expr
ty₂: Ty
a✝³: HasType b ty₂
a✝: HasType a Ty.bool
h: (match Maybe.found Ty.bool a✝, Maybe.found ty₂ a✝³ 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
and.found.found.and.bool
False
 
<;>
a, b: Expr
ty₁: Ty
a✝³: HasType a ty₁
ty₂: Ty
a✝²: HasType b ty₂
h: (match Maybe.found ty₁ a✝³, Maybe.found ty₂ a✝² 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
and.found.found.and
False
 
cases
 
ty₂: Ty
ty₂
a, b: Expr
a✝¹: HasType a Ty.bool
a✝: HasType b Ty.nat
h: (match Maybe.found Ty.bool a✝¹, Maybe.found Ty.nat a✝ 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
and.found.found.and.bool.nat
False
a, b: Expr
a✝¹: HasType a Ty.bool
a✝: HasType b Ty.bool
h: (match Maybe.found Ty.bool a✝¹, Maybe.found Ty.bool a✝ 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
and.found.found.and.bool.bool
False
 
<;>
a, b: Expr
ty₂: Ty
a✝³: HasType b ty₂
a✝: HasType a Ty.bool
h: (match Maybe.found Ty.bool a✝, Maybe.found ty₂ a✝³ 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
and.found.found.and.bool
False
 
simp
 
at
 
h: (match Maybe.found Ty.bool a✝¹, Maybe.found Ty.bool a✝ 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
h
Goals accomplished! 🐙

    
.
a, b: Expr
h: True
and.found.found.and.nat.nat
False
 
have
 := 
HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det
 ‹HasType b Ty.bool› ‹HasType b Ty.nat›
a, b: Expr
h: True
this: Ty.bool = Ty.nat
and.found.found.and.nat.nat
False
; 
contradiction
Goals accomplished! 🐙

    
.
a, b: Expr
h: True
and.found.found.and.nat.bool
False
 
have
 := 
HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det
 ‹HasType a Ty.bool› ‹HasType a Ty.nat›
a, b: Expr
h: True
this: Ty.bool = Ty.nat
and.found.found.and.nat.bool
False
; 
contradiction
Goals accomplished! 🐙

    
.
a, b: Expr
h: True
and.found.found.and.bool.nat
False
 
have
 := 
HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det
 ‹HasType b Ty.bool› ‹HasType b Ty.nat›
a, b: Expr
h: True
this: Ty.bool = Ty.nat
and.found.found.and.bool.nat
False
; 
contradiction
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) → Maybe fun 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}, Expr.typeCheck e = Maybe.unknown → ¬HasType e ty
Expr.typeCheck_complete
 
h': Expr.typeCheck e = Maybe.unknown
h'
)