proposition: Lemma exec_bexp : forall env e1 e2 v pg1 pg2 stk, beval env (blt e1 e2) v -> exists ec, exec_asm ec (pg1 ++ compile_bexp (map fst env) (blt e1 e2) ++ pg2) stk (env_to_mem env) (length pg1) = (Z.b2z (negb v) :: stk, env_to_mem env, (length pg1 + length (compile_bexp (map fst env) (blt e1 e2)))%nat).
proof: Proof. intros env e1 e2 v pg1 pg2 stk dyn. inversion dyn as [r e1' e2' v1 v2 ev1 ev2 cmp1| r e1' e2' v1 v2 ev1 ev2 cmp2]. destruct (exec_aexp env e1 v1 pg1 (compile_aexp (map fst env) e2 ++ [cmp] ++ pg2) stk ev1) as [ec1 Pec1]. destruct (exec_aexp env e2 v2 (pg1 ++ compile_aexp (map fst env) e1) ([cmp] ++ pg2) (v1 :: stk) ev2) as [ec2 Pec2]. revert Pec1 Pec2; simpl; rewrite <-!app_assoc; simpl; set (pg := pg1 ++ _). rewrite app_length. intros Pec1 Pec2; exists (ec1 + ec2 + 1)%nat. assert (both_exp : exec_asm (ec1 + ec2) pg stk (env_to_mem env) (length pg1) = (v2 :: v1 :: stk, env_to_mem env, (length pg1 + length (compile_aexp (map fst env) e1) + length (compile_aexp (map fst env) e2)))%nat). rewrite (exec_asm_seq pg _ (v1 :: stk) _ (env_to_mem env) _ _ _ (length pg1 + length (compile_aexp (map fst env) e1))%nat Pec1). easy. rewrite (exec_asm_seq _ _ (v2 :: v1 :: stk) _ (env_to_mem env) _ _ _ _ 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. assert (cmpv : v2 <=? v1 = false) by now rewrite Z.leb_gt. now rewrite cmpv, !Nat.add_assoc. destruct (exec_aexp env e1 v1 pg1 (compile_aexp (map fst env) e2 ++ [cmp] ++ pg2) stk ev1) as [ec1 Pec1]. destruct (exec_aexp env e2 v2 (pg1 ++ compile_aexp (map fst env) e1) ([cmp] ++ pg2) (v1 :: stk) ev2) as [ec2 Pec2]. revert Pec1 Pec2; simpl; rewrite <-!app_assoc; simpl; set (pg := pg1 ++ _). rewrite app_length. intros Pec1 Pec2; exists (ec1 + ec2 + 1)%nat. assert (both_exp : exec_asm (ec1 + ec2) pg stk (env_to_mem env) (length pg1) = (v2 :: v1 :: stk, env_to_mem env, (length pg1 + length (compile_aexp (map fst env) e1) + length (compile_aexp (map fst env) e2)))%nat). rewrite (exec_asm_seq pg _ (v1 :: stk) _ (env_to_mem env) _ _ _ (length pg1 + length (compile_aexp (map fst env) e1))%nat Pec1). easy. rewrite (exec_asm_seq _ _ (v2 :: v1 :: stk) _ (env_to_mem env) _ _ _ _ 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. assert (cmpv : v2 <=? v1 = true) by now rewrite Z.leb_le. now rewrite cmpv, !Nat.add_assoc. Qed.
imports: ZArith Arith List syntax little Lia