proposition: Lemma exec_aexp : forall env e v pg1 pg2 stk, aeval env e v -> exists ec, exec_asm ec (pg1 ++ compile_aexp (map fst env) e ++ pg2) stk (env_to_mem env) (length pg1) = (v :: stk, env_to_mem env, (length pg1 + length (compile_aexp (map fst env) e))%nat).
proof: Proof. intros env e v pg1 pg2 stk dyn; revert pg1 pg2 stk. induction dyn as [r n | r x v | r x y v v' xny dyn Ih| r e1 e2 v1 v2 dyn1 Ih1 dyn2 Ih2]. intros pg1 pg2 stk; exists 1%nat; simpl. now rewrite nth_error_app2, Nat.sub_diag; simpl. intros pg1 pg2 stk; exists 1%nat. apply (exec_avar x). constructor. easy. intros pg1 pg2 stk; exists 1%nat. apply (exec_avar x). now constructor. easy. intros pg1 pg2 stk. destruct (Ih1 pg1 (compile_aexp (map fst r) e2 ++ [add] ++ pg2) stk) as [ec1 Pec1]. destruct (Ih2 (pg1 ++ (compile_aexp (map fst r) e1)) (add :: pg2) (v1 :: stk)) as [ec2 Pec2]. exists (ec1 + ec2 + 1)%nat. simpl. revert Pec1 Pec2; rewrite <-!app_assoc; simpl. rewrite app_length. set (pg := pg1 ++ _); intros Pec1 Pec2. assert (both_exp : exec_asm (ec1 + ec2) pg stk (env_to_mem r) (length pg1) = (v2 :: v1 :: stk, env_to_mem r, (length pg1 + length (compile_aexp (map fst r) e1) + length (compile_aexp (map fst r) e2)))%nat). rewrite (exec_asm_seq pg _ (v1 :: stk) _ (env_to_mem r) _ _ _ (length pg1 + length (compile_aexp (map fst r) e1))%nat Pec1). easy. rewrite app_length. rewrite (exec_asm_seq _ _ (v2 :: v1 :: stk) _ (env_to_mem r) _ _ _ _ both_exp). unfold pg; simpl. rewrite 2!app_assoc. rewrite nth_error_app2;[ | now rewrite !app_length; auto with arith]. rewrite !app_length, Nat.sub_diag; simpl. now rewrite (Z.add_comm v2 v1), !Nat.add_assoc. Qed.
imports: ZArith Arith List syntax little Lia