proposition: Lemma FieldUpdateAction_Correct: forall p loc st_rac2 v st_rac2' st_rac3 st_rac3' cn um loc_obj loc_fsig, loc = Heap.InstanceField loc_obj loc_fsig -> Heap.typeof st_rac3@h loc_obj = Some (Heap.ObjectObject cn um) -> defined_field p cn loc_fsig -> assign_compatible p st_rac3@h v (FIELDSIGNATURE.type (snd loc_fsig)) -> CorrespondingState p st_rac2 st_rac3 -> FieldUpdateAction p loc v st_rac3 = st_rac3' -> Rac2.Assignables.FieldUpdateAction p loc v st_rac2 = st_rac2' -> CorrespondingState p st_rac2'[h:=Heap.update st_rac2@h loc v]%rac2 st_rac3'[h:=Heap.update st_rac3@h loc v].
proof: Proof. intuition. unfold FieldUpdateAction in H4. unfold Rac2.Assignables.FieldUpdateAction in H5. case_eq (isPivot p loc); intros; rewrite H6 in H5;rewrite H6 in H4. inversion H3. subst. split; simpl. inversion H7. subst. split; simpl; trivial. destruct H14. split. repeat rewrite map_length. trivial. intros. case_eq (Nat.compare n (length st_rac3 @fr @assignables )). intros. rewrite nat_compare_Eq in H14. repeat rewrite nth_overflow. auto with *. rewrite map_length. lia. rewrite map_length. lia. intros. apply nat_compare_lt in H14. generalize H14; intros. rewrite <- e in H15. repeat rewrite (nth_indep (map (Rac2.SavePreState p st_rac2 @h%rac2 (Heap.InstanceField loc_obj loc_fsig)) st_rac2 @fr%rac2 @assignables) a0 (Rac2.SavePreState p st_rac2 @h%rac2 (Heap.InstanceField loc_obj loc_fsig) a0)). repeat rewrite (nth_indep (map (SavePreState p st_rac3 @bl (Heap.InstanceField loc_obj loc_fsig)) st_rac3 @fr @assignables) a0 (SavePreState p st_rac3 @bl (Heap.InstanceField loc_obj loc_fsig) a0)). rewrite map_nth. rewrite map_nth. destruct a with n a0. repeat rewrite H8. apply SavePreState_same; trivial. rewrite map_length; trivial. rewrite map_length; trivial. intros. rewrite <- nat_compare_gt in H14. repeat rewrite nth_overflow. auto with *. rewrite map_length. lia. rewrite map_length. lia. rewrite H8. trivial. unfold CorrectBacklinks in H9 |- *. unfold CorrectBacklink in H9 |- *. intros. simpl. set (st' := st_rac3[h :=(Heap.update st_rac3 @h (Heap.InstanceField loc_obj loc_fsig) v)] [bl := (SetBacklinks p (Heap.InstanceField loc_obj loc_fsig) v (RemoveBacklinks p (Heap.InstanceField loc_obj loc_fsig) st_rac3))]). replace (Heap.update st_rac3 @h (Heap.InstanceField loc_obj loc_fsig) v) with st'@h. replace ((SetBacklinks p (Heap.InstanceField loc_obj loc_fsig) v (RemoveBacklinks p (Heap.InstanceField loc_obj loc_fsig) st_rac3))) with st'@bl. apply SetRemoveBacklinks_Correct with (Heap.InstanceField loc_obj loc_fsig) st_rac3 v cn um loc_obj loc_fsig ;trivial. apply isPivot_PivotField;trivial. unfold CorrectBacklink. trivial. trivial. trivial. split; simpl. destruct H. subst; trivial. destruct H3. trivial. destruct H3. rewrite H7. trivial. destruct H3. destruct H3. unfold CorrectBacklinks in H8 |- *. unfold CorrectBacklink in H8 |- *. simpl. rewrite <- H4. intros. rewrite <- not_isPivot_direct_FieldInDg. trivial. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)