gistfile1.coq

Lemma lemma1 : forall (st : state) (st1 st2 st3: list nat) (ins1 ins2 : list sinstr),
  s_execute st st1 ins1 = st2 ->
  s_execute st st2 ins2 = st3 ->
  s_execute st st1 (ins1 ++ ins2) = st3.
Proof.
  intros st st1 st2 st3 ins1.
  generalize dependent st1. generalize dependent st2.
  generalize dependent st3.
  induction ins1.
    intros. rewrite app_nil_l. simpl in H. subst. reflexivity.
    intros. destruct a;
      try (simpl in *; apply IHins1 with (st2:=st2); assumption);
      try (simpl; destruct st1;
        [simpl in *; apply IHins1 with (st2:=st2); assumption
        | destruct st1; try (simpl in *; apply IHins1 with (st2:=st2); assumption)]).
Qed.

Lemma s_compile_correct_gen : forall (st : state) (e : aexp) (s : list nat),
  s_execute st s (s_compile e) = [aeval st e] ++ s.
Proof.
  intros st e. generalize dependent st.
  induction e; intros; simpl; try reflexivity.  
  apply lemma1 with (st2 := [aeval st e1]++s).
  apply IHe1. apply lemma1 with (st2:=[aeval st e2]++[aeval st e1]++s).
  apply IHe2. reflexivity.

  apply lemma1 with (st2 := [aeval st e1]++s).
  apply IHe1. apply lemma1 with (st2:=[aeval st e2]++[aeval st e1]++s).
  apply IHe2. reflexivity.

  apply lemma1 with (st2 := [aeval st e1]++s).
  apply IHe1. apply lemma1 with (st2:=[aeval st e2]++[aeval st e1]++s).
  apply IHe2. reflexivity.
Qed.

Theorem s_compile_correct : forall (st : state) (e : aexp),
  s_execute st [] (s_compile e) = [ aeval st e ].
Proof.
  intros.
  apply s_compile_correct_gen.
Qed.