Theorem: Cpdt.Chapter2.compile_correct (Cpdt/Chapter2/Lang.lean)

State before:
⊢ ∀ (e : Exp), Prog.denote (Exp.compile e) [] = some [Exp.denote e]
Tactic:
intro e
State after:
e : Exp
⊢ Prog.denote (Exp.compile e) [] = some [Exp.denote e]

State before:
e : Exp
⊢ Prog.denote (Exp.compile e) [] = some [Exp.denote e]
Tactic:
rw [←List.append_nil (Exp.compile e)]
State after:
e : Exp
⊢ Prog.denote (Exp.compile e ++ []) [] = some [Exp.denote e]

State before:
e : Exp
⊢ Prog.denote (Exp.compile e ++ []) [] = some [Exp.denote e]
Tactic:
rw [compile_correct_help]
State after:
e : Exp
⊢ Prog.denote [] [Exp.denote e] = some [Exp.denote e]

State before:
e : Exp
⊢ Prog.denote [] [Exp.denote e] = some [Exp.denote e]
Tactic:
rw [Prog.denote_nil]
State after:
no goals