proposition: Lemma NewObjectAction_Correct: forall p l st_rac st_rac' st_sem st_sem', CorrespondingState p st_rac st_sem -> NewObjectAction p l st_rac = st_rac' -> Sem.Assignables.NewObjectAction p l st_sem = st_sem' -> CorrespondingState p st_rac' st_sem'.
proof: Proof. intuition. subst. inversion H. split; trivial. inversion H1. split; trivial. subst. unfold Sem.Assignables.NewObjectAction. unfold NewObjectAction. simpl in *. destruct st_rac @fr @fresh. simpl. destruct H10; trivial. simpl. simpl in H8. unfold ObjSet.Equal in *. split; intros. case_eq (ObjDec.eq_dec l a); intros. apply ObjSet.add_1; trivial. apply ObjSet.add_2; trivial. apply ObjSet.add_3 in H11; trivial. rewrite <- H8; trivial. case_eq (ObjDec.eq_dec l a); intros. apply ObjSet.add_1; trivial. apply ObjSet.add_2; trivial. apply ObjSet.add_3 in H11; trivial. rewrite H8; trivial. unfold Sem.Assignables.NewObjectAction. unfold NewObjectAction. simpl in *. split; intuition. destruct H9 with loc. clear H16. apply H15 in H13. destruct H13. destruct H13 as (fset, H13). left. destruct st_rac @fr @fresh. elim H10; trivial. simpl. rename fset into m0. exists m0. destruct m0. simpl in *. split. tauto. destruct H13. rewrite ObjSet2LocSet_def in H16 |- *. unfold LocInObjSet in H16 |- *. destruct loc. inversion H16. apply ObjSet.mem_1. apply ObjSet.add_2. apply ObjSet.mem_2 in H16; trivial. apply ObjSet.mem_1. apply ObjSet.add_2. apply ObjSet.mem_2 in H16; trivial. destruct H13. split; trivial. right; trivial. left; trivial. left. destruct st_rac @fr @fresh. elim H10; trivial. simpl in *. exists 0%nat. split. lia. rewrite ObjSet2LocSet_def. unfold ObjSet.Equal in *. unfold LocInObjSet in H14 |- *. destruct loc. inversion H14. apply ObjSet.mem_2 in H14. apply ObjSet.mem_1. case_eq (ObjDec.eq_dec l o); intros. apply ObjSet.add_1; trivial. apply ObjSet.add_2; trivial. apply ObjSet.add_3 in H14; trivial. rewrite <- H8; trivial. apply ObjSet.mem_2 in H14. apply ObjSet.mem_1. case_eq (ObjDec.eq_dec l o); intros. apply ObjSet.add_1; trivial. apply ObjSet.add_2; trivial. apply ObjSet.add_3 in H14; trivial. rewrite <- H8; trivial. case_eq (LocInObj loc l); intros. right. apply LocInObj_ObjSet with (obj := l); trivial. apply ObjSet.add_1; trivial. destruct H9 with loc. clear H15. destruct H16. intros. apply H13 in H15. destruct H15. destruct H15 as (m0, H15). left. destruct st_rac @fr @fresh. elim H10; trivial. simpl in H15. exists m0. destruct m0. simpl in *. split. tauto. destruct H15. rewrite ObjSet2LocSet_def in H16 |- *. unfold LocInObjSet in H16 |- *. unfold LocInObj in H14. destruct loc. inversion H16. case_eq (ObjDec.eq_dec o l); intros. rewrite H17 in H14. inversion H14. apply ObjSet.mem_2 in H16. apply ObjSet.add_3 in H16. apply ObjSet.mem_1; trivial. auto. case_eq (ObjDec.eq_dec o l); intros. rewrite H17 in H14. inversion H14. apply ObjSet.mem_2 in H16. apply ObjSet.add_3 in H16. apply ObjSet.mem_1; trivial. auto. destruct H15. split; trivial. right; trivial. left; trivial. right. unfold LocInObjSet in H15 |- *. destruct loc. inversion H15. apply ObjSet.mem_2 in H15. apply ObjSet.mem_1. apply ObjSet.add_2; trivial. apply ObjSet.mem_2 in H15. apply ObjSet.mem_1. apply ObjSet.add_2; trivial. unfold NewObjectAction. simpl. destruct st_rac @fr @fresh. elim H10; trivial. simpl. auto with *. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Lia)