proposition: Lemma compile_instr_complete : forall env env' i pg1 pg2 stk, exec env i env' -> exists ec, exec_asm ec (pg1 ++ compile_instr (map fst env) (length pg1) i ++ pg2) stk (env_to_mem env) (length pg1) = (stk, env_to_mem env', (length pg1 + length (compile_instr (map fst env) (length pg1) i))%nat).
proof: Proof. intros env env' i pg1 pg2 stk dyn; revert pg1 pg2 stk. induction dyn as [ | env env' x e v ev up | env env' env'' i1 i2 dyn1 Ih1 dyn2 Ih2| env env' env'' [e1 e2] i ev dyn1 Ih1 dyn2 Ih2 | env [e1 e2] i ev ]. intros pg1 pg2 stk. now exists 0%nat; simpl; rewrite Nat.add_0_r. intros pg1 pg2 stk. destruct (exec_aexp env e v pg1 (store (symbol_index (map fst env) x) :: pg2) stk) as [ec Pec]; auto. exists (ec + 1)%nat. simpl; rewrite <-!app_assoc; simpl; set (pg := pg1 ++ _). fold pg in Pec. assert (t1 := exec_asm_seq pg _ _ _ _ _ 1 _ _ Pec). rewrite t1; unfold pg; simpl; rewrite nth_error_app2; [ | lia]. rewrite minus_plus, <- (Nat.add_0_r (length _)). rewrite nth_error_app2;[ | lia]. rewrite minus_plus; simpl. assert (t2 := update_set_nth _ _ _ _ up). now rewrite t2, app_length, Nat.add_0_r, Nat.add_assoc. intros pg1 pg2 stk. destruct (Ih1 pg1 (compile_instr (map fst env) (length pg1 + length (compile_instr (map fst env) (length pg1) i1)) i2 ++ pg2) stk) as [ec1 Pec1]. revert Pec1; set (pg := (pg1 ++ _)); intros Pec1. destruct (Ih2 (pg1 ++ compile_instr (map fst env) (length pg1) i1) pg2 stk) as [ec2 Pec2]. revert Pec2; rewrite <-!app_assoc, app_length. rewrite <- (exec_fst_inv _ _ _ dyn1); fold pg; intros Pec2. simpl; rewrite <-!app_assoc, !app_length; fold pg. exists (ec1 + ec2)%nat. assert (t1 := exec_asm_seq pg _ _ _ _ _ ec2 _ _ Pec1). now rewrite t1, Pec2; rewrite !Nat.add_assoc. intros pg1 pg2 stk. cbn [compile_instr compile_bexp]. rewrite !app_length, !Nat.add_assoc, <-! app_assoc. repeat simpl (length [_]). set (middle_pc := (_ + 1 + 1)%nat). set (last_pc := (_ + 2)%nat). change (branch last_pc :: compile_instr (map fst env) middle_pc i ++ [goto (length pg1)]) with ([branch last_pc] ++ compile_instr (map fst env) middle_pc i ++ [goto (length pg1)]). rewrite <-!app_assoc. set (pg := pg1 ++ _). destruct (exec_bexp _ _ _ _ pg1 ([branch last_pc] ++ compile_instr (map fst env) (length pg1 + length (compile_bexp (map fst env) (blt e1 e2)) + 1) i ++ [goto (length pg1)] ++ pg2) stk ev) as [ec1 Pec1]. revert Pec1; cbn [compile_instr compile_bexp]. rewrite !app_length, !Nat.add_assoc, <- !app_assoc. simpl (length [ _ ]); fold middle_pc; fold pg; intros Pec1. destruct (Ih1 (pg1 ++ compile_bexp (map fst env) (blt e1 e2) ++ [branch last_pc]) ([goto (length pg1)] ++ pg2) stk) as [ec2 Pec2]. revert Pec2; cbn [compile_instr compile_bexp]. rewrite !app_length, !Nat.add_assoc, <- !app_assoc. simpl (length [cmp]); simpl (length [branch _]). fold middle_pc; fold pg; intros Pec2. destruct (Ih2 pg1 pg2 stk) as [ec3 Pec3]. revert Pec3; cbn [compile_instr compile_bexp]. rewrite !app_length, !Nat.add_assoc, <- !app_assoc. simpl (length [cmp]); simpl (length [branch _]). rewrite <- ! (exec_fst_inv _ _ _ dyn1). fold middle_pc; fold last_pc. change (branch last_pc :: compile_instr (map fst env) middle_pc i ++ [goto (length pg1)]) with ([branch last_pc] ++ compile_instr (map fst env) middle_pc i ++ [goto (length pg1)]). rewrite <- !app_assoc; fold pg; intros Pec3. exists (ec1 + (1 + (ec2 + (1 + ec3))))%nat. rewrite (exec_asm_seq pg _ (Z.b2z (negb true) :: stk) _ _ _ _ _ _ Pec1). rewrite (exec_asm_seq pg (Z.b2z (negb true) :: stk) stk (env_to_mem env) (env_to_mem env) 1 (ec2 + (1 + ec3)) (length pg1 + length (compile_aexp (map fst env) e1) + length (compile_aexp (map fst env) e2) + 1) middle_pc); cycle 1. simpl; unfold pg; rewrite <-!Nat.add_assoc. repeat (rewrite nth_error_app2, minus_plus; [ | lia]). now simpl; rewrite !Nat.add_assoc. rewrite (exec_asm_seq pg _ stk _ _ _ _ _ _ Pec2). rewrite (exec_asm_seq pg stk stk (env_to_mem env') (env_to_mem env') 1 ec3 _ (length pg1)); cycle 1. simpl; unfold pg, middle_pc; rewrite <-!Nat.add_assoc. repeat (rewrite nth_error_app2, minus_plus; [ | lia]). simpl. repeat (rewrite nth_error_app2, minus_plus; [ | lia]). simpl. set (L := length (compile_instr _ _ _)); rewrite <- (Nat.add_0_r L). unfold L. repeat (rewrite nth_error_app2, minus_plus; [ | lia]). easy. rewrite Pec3; unfold middle_pc; rewrite !app_length; simpl (length [_]). now rewrite !Nat.add_assoc. intros pg1 pg2 stk. cbn [compile_instr compile_bexp]. rewrite !app_length, !Nat.add_assoc, <-! app_assoc. repeat simpl (length [_]). set (middle_pc := (_ + 1 + 1)%nat). set (last_pc := (_ + 2)%nat). change (branch last_pc :: compile_instr (map fst env) middle_pc i ++ [goto (length pg1)]) with ([branch last_pc] ++ compile_instr (map fst env) middle_pc i ++ [goto (length pg1)]). rewrite <-!app_assoc. set (pg := pg1 ++ _). destruct (exec_bexp _ _ _ _ pg1 ([branch last_pc] ++ compile_instr (map fst env) (length pg1 + length (compile_bexp (map fst env) (blt e1 e2)) + 1) i ++ [goto (length pg1)] ++ pg2) stk ev) as [ec1 Pec1]. revert Pec1; cbn [compile_instr compile_bexp]. rewrite !app_length, !Nat.add_assoc, <- !app_assoc. simpl (length [ _ ]); fold middle_pc; fold pg; intros Pec1. exists (ec1 + 1)%nat. rewrite (exec_asm_seq _ _ (Z.b2z (negb false) :: stk) _ _ _ 1 _ _ Pec1). simpl. unfold pg; rewrite <-!Nat.add_assoc. repeat (rewrite nth_error_app2, minus_plus; [ | lia]). simpl. unfold last_pc, middle_pc. apply f_equal; lia. Qed.
imports: ZArith Arith List syntax little Lia