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

State before:
⊢ ∀ (e : Exp) (p : Prog) (s : Stack), Prog.denote (Exp.compile e ++ p) s = Prog.denote p (Exp.denote e :: s)
Tactic:
intro e p s
State after:
e : Exp
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile e ++ p) s = Prog.denote p (Exp.denote e :: s)

State before:
e : Exp
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile e ++ p) s = Prog.denote p (Exp.denote e :: s)
Tactic:
induction e generalizing p s with
| const n =>
  rw [Exp.compile_const]
  rw [Exp.denote_const]
  simp
  rw [Prog.denote_iConst]
| binop b l r lih rih =>
  rw [Exp.compile_binop]
  rw [Exp.denote_binop]
  rw [List.append_assoc (Exp.compile r)]
  rw [List.append_assoc (Exp.compile r)]
  rw [rih]
  rw [List.append_assoc]
  rw [lih]
  simp
  rw [Prog.denote_iBinop_2args]
State after:
no goals

State before:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile (Exp.const n) ++ p) s = Prog.denote p (Exp.denote (Exp.const n) :: s)
Tactic:
rw [Exp.compile_const]
State after:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iConst n] ++ p) s = Prog.denote p (Exp.denote (Exp.const n) :: s)

State before:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iConst n] ++ p) s = Prog.denote p (Exp.denote (Exp.const n) :: s)
Tactic:
rw [Exp.denote_const]
State after:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iConst n] ++ p) s = Prog.denote p (n :: s)

State before:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iConst n] ++ p) s = Prog.denote p (n :: s)
Tactic:
simp
State after:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote (Instr.iConst n :: p) s = Prog.denote p (n :: s)

State before:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote (Instr.iConst n :: p) s = Prog.denote p (n :: s)
Tactic:
rw [Prog.denote_iConst]
State after:
no goals

State before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile (Exp.binop b l r) ++ p) s = Prog.denote p (Exp.denote (Exp.binop b l r) :: s)
Tactic:
rw [Exp.compile_binop]
State after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ Exp.compile l ++ [Instr.iBinop b] ++ p) s =
    Prog.denote p (Exp.denote (Exp.binop b l r) :: s)

State before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ Exp.compile l ++ [Instr.iBinop b] ++ p) s =
    Prog.denote p (Exp.denote (Exp.binop b l r) :: s)
Tactic:
rw [Exp.denote_binop]
State after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ Exp.compile l ++ [Instr.iBinop b] ++ p) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)

State before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ Exp.compile l ++ [Instr.iBinop b] ++ p) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [List.append_assoc (Exp.compile r)]
State after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ (Exp.compile l ++ [Instr.iBinop b]) ++ p) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)

State before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ (Exp.compile l ++ [Instr.iBinop b]) ++ p) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [List.append_assoc (Exp.compile r)]
State after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ (Exp.compile l ++ [Instr.iBinop b] ++ p)) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)

State before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ (Exp.compile l ++ [Instr.iBinop b] ++ p)) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [rih]
State after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile l ++ [Instr.iBinop b] ++ p) (Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)

State before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile l ++ [Instr.iBinop b] ++ p) (Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [List.append_assoc]
State after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile l ++ ([Instr.iBinop b] ++ p)) (Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)

State before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile l ++ ([Instr.iBinop b] ++ p)) (Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [lih]
State after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iBinop b] ++ p) (Exp.denote l :: Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)

State before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iBinop b] ++ p) (Exp.denote l :: Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
simp
State after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Instr.iBinop b :: p) (Exp.denote l :: Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)

State before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Instr.iBinop b :: p) (Exp.denote l :: Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [Prog.denote_iBinop_2args]
State after:
no goals