proposition: Lemma SetRemoveBacklinks_Correct: forall p loc st st' f dg pivot v cn um loc_obj loc_fsig, PivotField p loc -> loc = Heap.InstanceField loc_obj loc_fsig -> Heap.typeof st@h loc_obj = Some (Heap.ObjectObject cn um) -> defined_field p cn loc_fsig -> assign_compatible p st@h v (FIELDSIGNATURE.type (snd loc_fsig)) -> st' = st[h := (Heap.update st@h loc v)] [bl := (SetBacklinks p loc v (RemoveBacklinks p loc st))] -> CorrectBacklink p st f dg pivot -> CorrectBacklink p st' f dg pivot.
proof: Proof. unfold CorrectBacklink. intros. rewrite H4. simpl. clear H4. rename H5 into H4. split; intros. inversion H5. case_eq (LocSet.E.eq_dec pivot_loc loc); intros. intros. rewrite e in H18. rewrite H18 in H5. rewrite H18 in H9. set (h' := Heap.update (State.h st) pivot v). assert (Heap.Compat (State.h st) pivot). rewrite H18 in H0. rewrite H0. apply Heap.CompatObject with cn um; trivial. generalize H9; intros. rewrite Heap.get_update_same in H21; trivial. inversion H21. fold h' in H5. fold h' in H9. rewrite H18. exists (list2LocSet (DynamicDGs p field_fsig pivot)). generalize H9; intro. apply PivotTargets_Correct with (p := p) (f_fsig := field_fsig) in H9. destruct H9. rewrite <- H7 in H24. assert (ex (fun dg => direct_FieldInDg_dynamic p h' f dg pivot)). exists dg; trivial. unfold SetBacklinks. apply H24 in H25. clear H9 H24. rewrite H7. induction (PivotTargets p pivot). inversion H25. split. case_eq (FsigDec.eq_dec a field_fsig); intros. simpl in H25. destruct H25. clear IHl. rewrite H24. simpl. unfold set_backlink at 1. simpl. destruct Backlinks.get. unfold get_backlinks. rewrite Backlinks.get_update_same. rewrite LocDict.get_update_same. trivial. unfold get_backlinks. rewrite Backlinks.get_update_same. unfold LocDict.singleton. rewrite LocDict.get_update_same. trivial. rewrite e0. simpl. unfold set_backlink at 1. simpl. destruct Backlinks.get. unfold get_backlinks. rewrite Backlinks.get_update_same. rewrite LocDict.get_update_same. trivial. unfold get_backlinks. rewrite Backlinks.get_update_same. unfold LocDict.singleton. rewrite LocDict.get_update_same. trivial. simpl in H25. destruct H25. elim n; trivial. simpl. unfold set_backlink at 1. destruct Backlinks.get. unfold get_backlinks. rewrite Backlinks.get_update_old. apply IHl. trivial. intro. inversion H25. elim n; trivial. unfold get_backlinks. rewrite Backlinks.get_update_old. apply IHl. trivial. intro. inversion H25. elim n; trivial. apply list2LocSet_1. rewrite DynamicDGs_Correct with (h := h') (f_obj := field_obj); trivial. rewrite <- H7; trivial. rewrite Heap.get_update_old in H9. destruct H4. elim H4. intros. exists x. split; trivial. clear H4 H20. destruct H21. apply get_remove_old with (p := p) (loc := loc) in H4. apply get_set_old with (p := p) (loc := loc) (v := v) in H4; trivial. rewrite <- H18; trivial. rewrite <- H18; trivial. tauto. split with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg0; trivial. rewrite <- H18; auto. case_eq (LocSet.E.eq_dec pivot loc); intros. rewrite <- e in H5. rewrite <- e. rewrite <- e in H0. rewrite <- e in H. clear loc e H6. destruct f. rewrite <- get_set_old_f_uncompat in H5. rewrite <- get_remove_old_f_uncompat in H5. apply H4 in H5. inversion H5. inversion H7. intros; intro; inversion H6. intros; intro; inversion H6. unfold SetBacklinks in H5. inversion H3. rewrite <- H6 in H5. elim get_remove_none with p st o f pivot dg; trivial. rewrite <- H8 in H5. case_eq (ObjDec.eq_dec o obj). intros. rewrite e. rewrite e in H5. repeat rewrite e in H4. clear o e H10. elim classic with (In f (PivotTargets p pivot)). intros. induction (PivotTargets p pivot). inversion H10. simpl in H10. destruct H10. clear IHl. rewrite H10 in H5. simpl in H5. unfold set_backlink at 1 in H5. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField obj f) pivot (list2LocSet (DynamicDGs p f pivot))) (RemoveBacklinks p pivot st) l) (Heap.InstanceField obj f)); intros; rewrite H11 in H5. simpl. unfold get_backlinks in H5. rewrite Backlinks.get_update_same in H5. rewrite LocDict.get_update_same in H5. destruct H5. destruct H5. inversion H5. rewrite <- H14 in H12. apply list2LocSet_1 in H12. rewrite DynamicDGs_Correct with (h := Heap.update (State.h st) pivot (Ref obj)) (f_obj := obj) in H12. trivial. apply Heap.get_update_same. rewrite H0. apply Heap.CompatObject with cn um; trivial. unfold LocDict.singleton in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_same in H5. rewrite LocDict.get_update_same in H5. destruct H5. destruct H5. inversion H5. rewrite <- H14 in H12. apply list2LocSet_1 in H12. rewrite DynamicDGs_Correct with (h := Heap.update (State.h st) pivot (Ref obj)) (f_obj := obj) in H12. trivial. apply Heap.get_update_same. rewrite H0. apply Heap.CompatObject with cn um; trivial. case_eq (FsigDec.eq_dec a f). intros. rewrite e in H5. clear IHl. clear a e H11. simpl in H5. unfold set_backlink at 1 in H5. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField obj f) pivot (list2LocSet (DynamicDGs p f pivot))) (RemoveBacklinks p pivot st) l) (Heap.InstanceField obj f)); intros; rewrite H11 in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_same in H5. rewrite LocDict.get_update_same in H5. destruct H5. destruct H5. inversion H5. rewrite <- H14 in H12. apply list2LocSet_1 in H12. rewrite DynamicDGs_Correct with (h := Heap.update (State.h st) pivot (Ref obj)) (f_obj := obj) in H12. trivial. apply Heap.get_update_same. rewrite H0. apply Heap.CompatObject with cn um; trivial. unfold LocDict.singleton in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_same in H5. rewrite LocDict.get_update_same in H5. destruct H5. destruct H5. inversion H5. rewrite <- H14 in H12. apply list2LocSet_1 in H12. rewrite DynamicDGs_Correct with (h := Heap.update (State.h st) pivot (Ref obj)) (f_obj := obj) in H12. trivial. apply Heap.get_update_same. rewrite H0. apply Heap.CompatObject with cn um; trivial. intros. simpl in H5. unfold set_backlink at 1 in H5. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField obj f) pivot (list2LocSet (DynamicDGs p f pivot))) (RemoveBacklinks p pivot st) l) (Heap.InstanceField obj a)); intros; rewrite H12 in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro. inversion H13. elim n; trivial. unfold LocDict.singleton in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro. inversion H13. elim n; trivial. intros. induction (PivotTargets p pivot). simpl in H5. intros. elim get_remove_none with p st obj f pivot dg; trivial. simpl in H5. unfold set_backlink at 1 in H5. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField obj f) pivot (list2LocSet (DynamicDGs p f pivot))) (RemoveBacklinks p pivot st) l) (Heap.InstanceField obj a)); intros; rewrite H11 in H5. simpl in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro; elim H10; auto with *. intro; elim H10. inversion H12. auto with *. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro; elim H10; auto with *. intro; elim H10. inversion H12. auto with *. intros. induction (PivotTargets p pivot). simpl in H5. elim get_remove_none with p st o f pivot dg; trivial. simpl in H5. unfold set_backlink at 1 in H5. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField obj f) pivot (list2LocSet (DynamicDGs p f pivot))) (RemoveBacklinks p pivot st) l) (Heap.InstanceField obj a)); intros; rewrite H11 in H5. simpl in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro; elim n. inversion H12; trivial. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro; elim n. inversion H12; trivial. rewrite <- H8 in H5. case_eq (ObjDec.eq_dec o obj). intros. rewrite e. rewrite e in H5. repeat rewrite e in H4. clear o e H10. elim classic with (In f (PivotTargets p pivot)). intros. induction (PivotTargets p pivot). inversion H10. simpl in H10. destruct H10. clear IHl. rewrite H10 in H5. simpl in H5. unfold set_backlink at 1 in H5. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField obj f) pivot (list2LocSet (DynamicDGs p f pivot))) (RemoveBacklinks p pivot st) l) (Heap.InstanceField obj f)); intros; rewrite H11 in H5. simpl. unfold get_backlinks in H5. rewrite Backlinks.get_update_same in H5. rewrite LocDict.get_update_same in H5. destruct H5. destruct H5. inversion H5. rewrite <- H14 in H12. apply list2LocSet_1 in H12. rewrite DynamicDGs_Correct with (h := Heap.update (State.h st) pivot (Ref obj)) (f_obj := obj) in H12. trivial. apply Heap.get_update_same. rewrite H0. apply Heap.CompatObject with cn um; trivial. unfold LocDict.singleton in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_same in H5. rewrite LocDict.get_update_same in H5. destruct H5. destruct H5. inversion H5. rewrite <- H14 in H12. apply list2LocSet_1 in H12. rewrite DynamicDGs_Correct with (h := Heap.update (State.h st) pivot (Ref obj)) (f_obj := obj) in H12. trivial. apply Heap.get_update_same. rewrite H0. apply Heap.CompatObject with cn um; trivial. case_eq (FsigDec.eq_dec a f). intros. rewrite e in H5. clear IHl. clear a e H11. simpl in H5. unfold set_backlink at 1 in H5. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField obj f) pivot (list2LocSet (DynamicDGs p f pivot))) (RemoveBacklinks p pivot st) l) (Heap.InstanceField obj f)); intros; rewrite H11 in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_same in H5. rewrite LocDict.get_update_same in H5. destruct H5. destruct H5. inversion H5. rewrite <- H14 in H12. apply list2LocSet_1 in H12. rewrite DynamicDGs_Correct with (h := Heap.update (State.h st) pivot (Ref obj)) (f_obj := obj) in H12. trivial. apply Heap.get_update_same. rewrite H0. apply Heap.CompatObject with cn um; trivial. unfold LocDict.singleton in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_same in H5. rewrite LocDict.get_update_same in H5. destruct H5. destruct H5. inversion H5. rewrite <- H14 in H12. apply list2LocSet_1 in H12. rewrite DynamicDGs_Correct with (h := Heap.update (State.h st) pivot (Ref obj)) (f_obj := obj) in H12. trivial. apply Heap.get_update_same. rewrite H0. apply Heap.CompatObject with cn um; trivial. intros. simpl in H5. unfold set_backlink at 1 in H5. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField obj f) pivot (list2LocSet (DynamicDGs p f pivot))) (RemoveBacklinks p pivot st) l) (Heap.InstanceField obj a)); intros; rewrite H12 in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro. inversion H13. elim n; trivial. unfold LocDict.singleton in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro. inversion H13. elim n; trivial. intros. induction (PivotTargets p pivot). simpl in H5. intros. elim get_remove_none with p st obj f pivot dg; trivial. simpl in H5. unfold set_backlink at 1 in H5. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField obj f) pivot (list2LocSet (DynamicDGs p f pivot))) (RemoveBacklinks p pivot st) l) (Heap.InstanceField obj a)); intros; rewrite H11 in H5. simpl in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro; elim H10; auto with *. intro; elim H10. inversion H12. auto with *. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro; elim H10; auto with *. intro; elim H10. inversion H12. auto with *. intros. induction (PivotTargets p pivot). simpl in H5. elim get_remove_none with p st o f pivot dg; trivial. simpl in H5. unfold set_backlink at 1 in H5. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField obj f) pivot (list2LocSet (DynamicDGs p f pivot))) (RemoveBacklinks p pivot st) l) (Heap.InstanceField obj a)); intros; rewrite H11 in H5. simpl in H5. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro; elim n. inversion H12; trivial. unfold get_backlinks in H5. rewrite Backlinks.get_update_old in H5. apply IHl; trivial. intro; elim n. inversion H12; trivial. rewrite <- H7 in H5. elim get_remove_none with p st o f pivot dg; trivial. rewrite <- get_set_old_f_uncompat in H5. rewrite <- get_remove_old_f_uncompat in H5. apply H4 in H5. inversion H5. inversion H7. intros; intro; inversion H6. intros; intro; inversion H6. destruct H5. destruct H5. apply get_set_old in H5. apply get_remove_old in H5. destruct H4. assert (ex (fun ams => and (eq (LocDict.get (get_backlinks (Adds.backlinks (State.adds st)) f) pivot) (Some ams)) (LocSet.In dg ams))). exists x; auto. apply H8 in H9. inversion H9. split with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg0; trivial. rewrite Heap.get_update_old. trivial. auto. 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)