s_compile_correct.v

Theorem s_concat_program :
  forall (st : state) (prog1 prog2 : list sinstr) (l : list nat),
    s_execute st l (prog1 ++ prog2) = s_execute st (s_execute st l prog1)  prog2.
Proof.
  intros st. induction prog1.
  auto.
  simpl. intros.
  destruct (s_eval st l a); apply IHprog1.
Qed.


Theorem s_compile_correct : forall (st : state) (e : aexp),
  s_execute st [] (s_compile e) = [ aeval st e ].
Proof.
  intros st. induction e.
  auto. auto. simpl.
  try ( repeat (rewrite s_concat_program)).
  rewrite IHe1. 


  st : state
  e1, e2 : aexp
  IHe1 : s_execute st [] (s_compile e1) = [aeval st e1]
  IHe2 : s_execute st [] (s_compile e2) = [aeval st e2]
  ============================
  s_execute st (s_execute st [aeval st e1] (s_compile e2)) [SPlus] = [aeval st e1 + aeval st e2]

subgoal 2 (ID 176) is:
 s_execute st [] (s_compile (AMinus e1 e2)) = [aeval st (AMinus e1 e2)]
subgoal 3 (ID 181) is:
 s_execute st [] (s_compile (AMult e1 e2)) = [aeval st (AMult e1 e2)]

https://github.com/mukeshtiwari/Coq/blob/master/software-foundation-8.5/Imp.v