proposition: Lemma exec_avar : forall n env e v pg1 pg2 stk, aeval env e v -> e = avar n -> exec_asm 1 (pg1 ++ compile_aexp (map fst env) e ++ pg2) stk (env_to_mem env) (length pg1) = (v :: stk, env_to_mem env, (length pg1 + 1)%nat).
proof: Proof. intros n env e v pg1 pg2 stk dyn. induction dyn as [r v | r x v | r x y v v' xny dyn Ih | r e1 e2 v1 v2 dyn1 Ih1 dyn2 Ih2]. discriminate. intros [= xn]; simpl. destruct (S.string_dec x x) as [ _ | abs];[simpl | now case abs]. now rewrite nth_error_app2, Nat.sub_diag; simpl. intros [= xn]; simpl. destruct (S.string_dec x y) as [ abs | _];[now case xny | simpl]. rewrite nth_error_app2, Nat.sub_diag; simpl; auto with arith. revert Ih; rewrite xn; simpl. rewrite nth_error_app2, Nat.sub_diag; simpl; auto with arith. intros Ih; assert (Ih' := Ih eq_refl); injection Ih'. now intros v'q; rewrite v'q. discriminate. Qed.
imports: ZArith Arith List syntax little Lia