Theorem: Cpdt.Chapter5.Exp.typecheck_complete (Cpdt/Chapter5/Typechecker.lean)

State before:
case add
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
⊢ (match typecheck l, typecheck r with
      | Maybe.found Ty.nat lth, Maybe.found Ty.nat rth => Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat)
      | x, x_1 => Maybe.unknown) =
      Maybe.unknown →
    ∀ (t : Ty), ¬HasType (add l r) t
Tactic:
split
State after:
case add.h_1
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
lth✝ : HasType l Ty.nat
rth✝ : HasType r Ty.nat
heq✝¹ : typecheck l = Maybe.found Ty.nat lth✝
heq✝ : typecheck r = Maybe.found Ty.nat rth✝
⊢ Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t

case add.h_2
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝² : {{t|HasType l t}}
x✝¹ : {{t|HasType r t}}
x✝ :
  ∀ (lth : HasType l Ty.nat) (rth : HasType r Ty.nat),
    typecheck l = Maybe.found Ty.nat lth → typecheck r = Maybe.found Ty.nat rth → False
⊢ Maybe.unknown = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t

State before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.nat
htr : HasType r Ty.nat
rl : typecheck l = Maybe.found Ty.nat htl
rr : typecheck r = Maybe.found Ty.nat htr
⊢ Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t
Tactic:
case add.h_1 _ _ htl htr rl rr =>
  intros
  contradiction
State after:
no goals

State before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.nat
htr : HasType r Ty.nat
rl : typecheck l = Maybe.found Ty.nat htl
rr : typecheck r = Maybe.found Ty.nat htr
⊢ Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t
Tactic:
intros
State after:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.nat
htr : HasType r Ty.nat
rl : typecheck l = Maybe.found Ty.nat htl
rr : typecheck r = Maybe.found Ty.nat htr
a✝ : Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown
t✝ : Ty
⊢ ¬HasType (add l r) t✝

State before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.nat
htr : HasType r Ty.nat
rl : typecheck l = Maybe.found Ty.nat htl
rr : typecheck r = Maybe.found Ty.nat htr
a✝ : Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown
t✝ : Ty
⊢ ¬HasType (add l r) t✝
Tactic:
contradiction
State after:
no goals

State before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
hnp :
  ∀ (lth : HasType l Ty.nat) (rth : HasType r Ty.nat),
    typecheck l = Maybe.found Ty.nat lth → typecheck r = Maybe.found Ty.nat rth → False
⊢ Maybe.unknown = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t
Tactic:
intro h t ht
State after:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
hnp :
  ∀ (lth : HasType l Ty.nat) (rth : HasType r Ty.nat),
    typecheck l = Maybe.found Ty.nat lth → typecheck r = Maybe.found Ty.nat rth → False
h : Maybe.unknown = Maybe.unknown
t : Ty
ht : HasType (add l r) t
⊢ False

State before:
case and
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
⊢ (match typecheck l, typecheck r with
      | Maybe.found Ty.bool lth, Maybe.found Ty.bool rth => Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool)
      | x, x_1 => Maybe.unknown) =
      Maybe.unknown →
    ∀ (t : Ty), ¬HasType (and l r) t
Tactic:
split
State after:
case and.h_1
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
lth✝ : HasType l Ty.bool
rth✝ : HasType r Ty.bool
heq✝¹ : typecheck l = Maybe.found Ty.bool lth✝
heq✝ : typecheck r = Maybe.found Ty.bool rth✝
⊢ Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t

case and.h_2
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝² : {{t|HasType l t}}
x✝¹ : {{t|HasType r t}}
x✝ :
  ∀ (lth : HasType l Ty.bool) (rth : HasType r Ty.bool),
    typecheck l = Maybe.found Ty.bool lth → typecheck r = Maybe.found Ty.bool rth → False
⊢ Maybe.unknown = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t

State before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.bool
htr : HasType r Ty.bool
rl : typecheck l = Maybe.found Ty.bool htl
rr : typecheck r = Maybe.found Ty.bool htr
⊢ Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t
Tactic:
case and.h_1 _ _ htl htr rl rr =>
  intros
  contradiction
State after:
no goals

State before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.bool
htr : HasType r Ty.bool
rl : typecheck l = Maybe.found Ty.bool htl
rr : typecheck r = Maybe.found Ty.bool htr
⊢ Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t
Tactic:
intros
State after:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.bool
htr : HasType r Ty.bool
rl : typecheck l = Maybe.found Ty.bool htl
rr : typecheck r = Maybe.found Ty.bool htr
a✝ : Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown
t✝ : Ty
⊢ ¬HasType (and l r) t✝

State before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.bool
htr : HasType r Ty.bool
rl : typecheck l = Maybe.found Ty.bool htl
rr : typecheck r = Maybe.found Ty.bool htr
a✝ : Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown
t✝ : Ty
⊢ ¬HasType (and l r) t✝
Tactic:
contradiction
State after:
no goals

State before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
hnp :
  ∀ (lth : HasType l Ty.bool) (rth : HasType r Ty.bool),
    typecheck l = Maybe.found Ty.bool lth → typecheck r = Maybe.found Ty.bool rth → False
⊢ Maybe.unknown = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t
Tactic:
intro h t ht
State after:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
hnp :
  ∀ (lth : HasType l Ty.bool) (rth : HasType r Ty.bool),
    typecheck l = Maybe.found Ty.bool lth → typecheck r = Maybe.found Ty.bool rth → False
h : Maybe.unknown = Maybe.unknown
t : Ty
ht : HasType (and l r) t
⊢ False