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