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

State before:
e : Exp
t : Ty
h : HasType e t
⊢ HasType e t → typecheck e ≠ Maybe.unknown → typecheck e = Maybe.found t h
Tactic:
intro ht1
State after:
e : Exp
t : Ty
h ht1 : HasType e t
⊢ typecheck e ≠ Maybe.unknown → typecheck e = Maybe.found t h

State before:
e : Exp
t : Ty
h ht1 : HasType e t
⊢ typecheck e ≠ Maybe.unknown → typecheck e = Maybe.found t h
Tactic:
cases typecheck e with
| found t2 ht2 =>
  intros
  have h : t = t2 := HasType_det ht1 ht2
  simp [h]
| unknown =>
  intros
  contradiction
State after:
no goals

State before:
case found
e : Exp
t : Ty
h ht1 : HasType e t
t2 : Ty
ht2 : HasType e t2
⊢ Maybe.found t2 ht2 ≠ Maybe.unknown → Maybe.found t2 ht2 = Maybe.found t h
Tactic:
intros
State after:
case found
e : Exp
t : Ty
h ht1 : HasType e t
t2 : Ty
ht2 : HasType e t2
a✝ : Maybe.found t2 ht2 ≠ Maybe.unknown
⊢ Maybe.found t2 ht2 = Maybe.found t h

State before:
case found
e : Exp
t : Ty
h ht1 : HasType e t
t2 : Ty
ht2 : HasType e t2
a✝ : Maybe.found t2 ht2 ≠ Maybe.unknown
⊢ Maybe.found t2 ht2 = Maybe.found t h
Tactic:
have h : t = t2 := HasType_det ht1 ht2
State after:
case found
e : Exp
t : Ty
h✝ ht1 : HasType e t
t2 : Ty
ht2 : HasType e t2
a✝ : Maybe.found t2 ht2 ≠ Maybe.unknown
h : t = t2
⊢ Maybe.found t2 ht2 = Maybe.found t h✝

State before:
case found
e : Exp
t : Ty
h✝ ht1 : HasType e t
t2 : Ty
ht2 : HasType e t2
a✝ : Maybe.found t2 ht2 ≠ Maybe.unknown
h : t = t2
⊢ Maybe.found t2 ht2 = Maybe.found t h✝
Tactic:
simp [h]
State after:
no goals

State before:
case unknown
e : Exp
t : Ty
h ht1 : HasType e t
⊢ Maybe.unknown ≠ Maybe.unknown → Maybe.unknown = Maybe.found t h
Tactic:
intros
State after:
case unknown
e : Exp
t : Ty
h ht1 : HasType e t
a✝ : Maybe.unknown ≠ Maybe.unknown
⊢ Maybe.unknown = Maybe.found t h

State before:
case unknown
e : Exp
t : Ty
h ht1 : HasType e t
a✝ : Maybe.unknown ≠ Maybe.unknown
⊢ Maybe.unknown = Maybe.found t h
Tactic:
contradiction
State after:
no goals