proposition: Theorem rac2_rac1_correct: forall p, (forall e st_rac2 st'_rac2 r, OpRac2.ExpressionStep p e st_rac2 st'_rac2 r -> forall st_rac1, CorrespondingState p st_rac1 st_rac2 -> exists st'_rac1, CorrespondingState p st'_rac1 st'_rac2 /\ OpRac1.ExpressionStep p e st_rac1 st'_rac1 r) /\ (forall l st_rac2 st'_rac2 r, OpRac2.ListSteps p l st_rac2 st'_rac2 r -> forall st_rac1, CorrespondingState p st_rac1 st_rac2 -> exists st'_rac1, CorrespondingState p st'_rac1 st'_rac2 /\ OpRac1.ListSteps p l st_rac1 st'_rac1 r) /\ (forall m b st_rac2 st'_rac2 r, OpRac2.StatementStep p m b st_rac2 st'_rac2 r -> forall st_rac1, CorrespondingState p st_rac1 st_rac2 -> exists st'_rac1, CorrespondingState p st'_rac1 st'_rac2 /\ OpRac1.StatementStep p m b st_rac1 st'_rac1 r) /\ (forall m b st_rac2 st'_rac2 r, OpRac2.BlockStep p m b st_rac2 st'_rac2 r -> forall st_rac1, CorrespondingState p st_rac1 st_rac2-> exists st'_rac1, CorrespondingState p st'_rac1 st'_rac2 /\ OpRac1.BlockStep p m b st_rac1 st'_rac1 r).
proof: Proof. intro p. apply OpRac2.mutual_ind; intros; simpl in *. apply H2 in H11. destruct H11 as[st1_rac1 H11]. destruct H11. destruct H5 with st1_rac1 as [st2_rac1 H13];trivial. destruct H13. set (st'_rac1 := Rac1.Assignables.FieldUpdateAction p loc v st2_rac1). exists ((st'_rac1[h := Heap.update st2_rac1@h loc v])%rac1). split. rewrite H10. apply FieldUpdateAction_Correct;trivial. inversion H13. apply (OpRac1.assignment_instance_field_ok p e v obj fsig expr target st_rac1 st1_rac1 st2_rac1 st2_rac1[h := Heap.update st2_rac1@h loc v]%rac1 st2_rac1 loc cn um); trivial. apply (FieldUpdateCheck_Correct loc p st1_rac1 st1); trivial. rewrite H23;trivial. rewrite H23;trivial. destruct H1 with st_rac1 as (st1_rac1, Htmp); trivial. destruct Htmp. clear H1. destruct H6 with st1_rac1 as (st2_rac1, Htmp); trivial. destruct Htmp. clear H6. set (fr_c1_rac1 := Rac1.NewFrame m' (lv2params m' (Ref this0 :: psv)) st2_rac1) in |- *. set (st3_rac1 := st2_rac1[fr := fr_c1_rac1]%rac1) in |- *. set (st_c_rac1 := Rac1.Assignables.MethodCallAction p c' m' st3_rac1) in |- *. destruct H15 with st_c_rac1 as (st_c'_rac1, Htmp). assert (CorrespondingState p st3_rac1 st3). unfold st3_rac1 in |- *. rewrite H10 in |- *. apply NewFrame_Correct with (m := m') (param := lv2params m' (Ref this0 :: psv)) (st_rac1 := st2_rac1) (st_rac2 := st2); trivial. unfold st_c_rac1 in |- *. rewrite <- H11. apply MethodCallAction_Correct with (c := c') (m := m') (st_rac1 := st3_rac1) (st_rac2 := st3); trivial. destruct Htmp. set (st'_rac1 := Rac1.Assignables.MethodReturnAction p st_c'_rac1 st2_rac1) in |- *. exists st'_rac1. split. unfold st'_rac1 in |- *. rewrite <- H17 in |- *. generalize rac2_length_assignables_correct. intros. specialize H23 with p. destruct H23. destruct H24. destruct H25. apply MethodReturnAction_Correct with st2_rac1 st_c'_rac1 st2 st_c'; trivial. assert (EquivAssignables p st2 st_c). unfold NewFrame in H9. unfold MethodCallAction in H11. unfold EquivAssignables. rewrite H9 in H10. rewrite H10 in H11. simpl in H11. rewrite <- H11. simpl. unfold level. simpl. rewrite nat_compare_n_Sn. rewrite truncate_same. apply EquivAssignables_ind_refl. apply EquivAssignables_trans with st_c; trivial. generalize rac2_equiv_assignables_correct. intros. specialize H28 with p. destruct H28. destruct H29. destruct H30. apply H31 in H14. trivial. apply H26 in H14. rewrite H14. apply Nat.le_min_r. apply H26 in H14. rewrite <- H14. rewrite <- H11. rewrite H10. rewrite H9. simpl. trivial. apply (OpRac1.method_vcall_ok p e st_rac1 st1_rac1 st2_rac1 st3_rac1 st_c_rac1 st_c'_rac1 st'_rac1 fr_c1_rac1 msig o cn um this0 ps psnv psv v cn' m' c' b body); trivial. destruct H19. rewrite H30;trivial. destruct H6. rewrite H25. trivial. set (st1_rac1 := Rac1.Assignables.NewObjectAction p o st_rac1) in |- *. exists st1_rac1[h := h']%rac1. split. rewrite H2 in |- *. assert (CorrespondingState p st1_rac1 st1). unfold st1_rac1 in |- *. rewrite <- H1 in |- *. apply NewObjectAction_Correct with o st_rac1 st; trivial. destruct H4. split;simpl;trivial. destruct H11. split. trivial. intros. generalize UnfoldDatagroups_rac_intersect_new. intros. specialize H11 with p st_rac2@h (Heap.ObjectObject cn um) st_rac2@fr o h' n. replace st@h with st_rac2@h in H0. apply H11 in H0. generalize H0. specialize e1 with n. generalize e1. apply LocSet.eq_trans. rewrite <- H1. simpl. trivial. apply OpRac1.new_object_ok with (st1 := st1_rac1) (h' := h') (cn := cn) (um := um); trivial. destruct H3. rewrite H11; trivial. exists st_rac1. rewrite <- H in |- *. split; trivial. apply OpRac1.ListSteps_nil; trivial. destruct H1 with st_rac1 as (st1_rac1, Htmp); trivial. destruct Htmp. destruct H3 with st1_rac1 as (st'_rac1, Htmp); trivial. destruct Htmp. exists st'_rac1. split; trivial. apply OpRac1.ListSteps_cons_ok with (e := e) (le := le) (st1 := st1_rac1); trivial. destruct H1 with st_rac1 as (st'_rac1, Htmp); trivial. destruct Htmp. exists st'_rac1. split; trivial. apply OpRac1.expr_stmt_ok with (v := v) (e := e); trivial. destruct H2. destruct H5. rewrite H6 in |- *; trivial. destruct H1 with st_rac1 as (st1_rac1, Htmp); trivial. destruct Htmp. set (fr2_rac1 := Rac1.State.Frame.set_pc st1_rac1@fr%rac1 pc') in |- *. destruct H4 with st1_rac1[fr := fr2_rac1]%rac1 as (st'_rac1, Htmp); trivial. destruct H6. rewrite H2 in |- *. unfold fr2_rac1 in |- *. split; trivial. destruct Htmp. exists st'_rac1. split; trivial. apply OpRac1.BlockStep_ok_next with (pc' := pc') (st1 := st1_rac1) (fr2 := fr2_rac1); trivial. destruct H5. rewrite H11 in |- *. trivial. destruct H1 with st_rac1 as (st'_rac1, Htmp); trivial. destruct Htmp. exists st'_rac1. split; trivial. apply OpRac1.BlockStep_ok_last; trivial. destruct H2. rewrite H6 in |- *; trivial. Qed.
imports: Coq(List)