proposition: Lemma get_remove_none: forall p st obj f pivot dg, CorrectBacklink p st (Heap.InstanceField obj f) dg pivot -> PivotField p pivot -> ~ (exists locs, LocDict.get (get_backlinks (RemoveBacklinks p pivot st) (Heap.InstanceField obj f)) pivot = Some locs /\ (LocSet.In dg locs)).
proof: Proof. unfold CorrectBacklink. intros. unfold RemoveBacklinks. case_eq (Heap.get st@h pivot);intros. destruct v. intro. rewrite <- H in H2. inversion H2. rewrite H6 in H1. inversion H1. intro. rewrite <- H in H2. inversion H2. rewrite H6 in H1. inversion H1. case_eq (ObjDec.eq_dec o obj). intros. rewrite e. rewrite e in H1. clear o e H2. elim classic with (exists dg, direct_FieldInDg_dynamic p st @h (Heap.InstanceField obj f) dg pivot). intros. generalize H2; intro. rewrite <- PivotTargets_Correct in H3; trivial. induction (PivotTargets p pivot). inversion H3. simpl in H3. destruct H3. clear IHl. rewrite H3. clear a H3. simpl. unfold get_backlinks. unfold remove_backlink at 1. case_eq (Backlinks.get (fold_right (fun (f0 : FieldSignature) (bl : Backlinks.t) => remove_backlink bl (Heap.InstanceField obj f0) pivot) st @bl l) (Heap.InstanceField obj f)). intros. simpl. rewrite Backlinks.get_update_same. rewrite LocDict.get_remove_none. intro. destruct H4. destruct H4. inversion H4. intros. rewrite H3. intro. rewrite LocDict.get_empty in H4. destruct H4. destruct H4. inversion H4. simpl. case_eq (FsigDec.eq_dec a f). intros. rewrite e. unfold get_backlinks. unfold remove_backlink at 1. case_eq (Backlinks.get (fold_right (fun (f0 : FieldSignature) (bl : Backlinks.t) => remove_backlink bl (Heap.InstanceField obj f0) pivot) st @bl l) (Heap.InstanceField obj f)). simpl. intros. rewrite Backlinks.get_update_same. rewrite LocDict.get_remove_none. intro. destruct H6. destruct H6. inversion H6. intro. rewrite H5. intro. rewrite LocDict.get_empty in H6. destruct H6. destruct H6. inversion H6. intros. unfold get_backlinks. unfold remove_backlink at 1. case_eq (Backlinks.get (fold_right (fun (f0 : FieldSignature) (bl : Backlinks.t) => remove_backlink bl (Heap.InstanceField obj f0) pivot) st @bl l) (Heap.InstanceField obj a)). intros. simpl. rewrite Backlinks.get_update_old. apply IHl. trivial. intro. elim n. inversion H6; trivial. intro. apply IHl. trivial. intros. intro. elim H2. exists dg. apply H. rewrite <- PivotTargets_Correct in H2. induction (PivotTargets p pivot). simpl. intros. destruct H3 as [ams H3]. exists ams. trivial. intros. simpl in H3. unfold remove_backlink at 1 in H3. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl : Backlinks.t) => remove_backlink bl (Heap.InstanceField obj f) pivot) st @bl l) (Heap.InstanceField obj a)); intros; rewrite H4 in H3. simpl in H3. simpl in H2. assert (a <> f). intro. elim H2. left; trivial. unfold get_backlinks in H3. rewrite Backlinks.get_update_old in H3. apply IHl. intro. elim H2. right. trivial. trivial. intro. elim H5. inversion H6. trivial. apply IHl. intro. elim H2. right; trivial. trivial. trivial. intros. assert (~ direct_FieldInDg_dynamic p st @h (Heap.InstanceField obj f) dg pivot). intro. inversion H3. inversion H5. rewrite H7 in H1. inversion H1. rewrite <- H18 in H20. elim n. symmetry. trivial. rewrite H in H3. intro. elim H3. induction (PivotTargets p pivot). simpl in H4. trivial. apply IHl. clear IHl. simpl in H4. unfold remove_backlink at 1 in H4. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl : Backlinks.t) => remove_backlink bl (Heap.InstanceField o f) pivot) st @bl l) (Heap.InstanceField o a)); intros; rewrite H5 in H4. simpl. unfold get_backlinks in H4. rewrite Backlinks.get_update_old in H4. trivial. intro. elim n. inversion H6; trivial. trivial. intro. rewrite <- H in H2. inversion H2. rewrite H6 in H1. inversion H1. intro. rewrite <- H in H2. inversion H2. rewrite H6 in H1. inversion H1. 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)