proposition: Lemma get_set_old: forall p loc pivot bl x f v, pivot <> loc -> (LocDict.get (get_backlinks bl f) pivot = Some x <-> LocDict.get (get_backlinks (SetBacklinks p loc v bl) f) pivot = Some x).
proof: Proof. split; intros. unfold SetBacklinks. destruct v; trivial. induction (PivotTargets p loc). simpl; trivial. simpl. unfold set_backlink at 1. case_eq (Backlinks.get (fold_right (fun (f0 : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField o f0) loc (list2LocSet (DynamicDGs p f0 loc))) bl l) (Heap.InstanceField o a)); intros. simpl. unfold get_backlinks. case_eq (eq_dec (Heap.InstanceField o a) f); intros. rewrite <- e. rewrite Backlinks.get_update_same. unfold get_backlinks in IHl. rewrite e in H1. rewrite H1 in IHl. rewrite LocDict.get_update_old; auto. rewrite Backlinks.get_update_old; trivial. case_eq (eq_dec (Heap.InstanceField o a) f); intros. rewrite e in H1. unfold get_backlinks in IHl. rewrite H1 in IHl. rewrite LocDict.get_empty in IHl. inversion IHl. unfold LocDict.singleton. unfold get_backlinks. rewrite Backlinks.get_update_old; trivial. unfold SetBacklinks in H0. destruct v; trivial. induction (PivotTargets p loc). simpl; trivial. simpl in H0. unfold set_backlink at 1 in H0. case_eq (Backlinks.get (fold_right (fun (f : FieldSignature) (bl' : Backlinks.t) => set_backlink bl' (Heap.InstanceField o f) loc (list2LocSet (DynamicDGs p f loc))) bl l) (Heap.InstanceField o a)); intros. rewrite H1 in H0. simpl in H0. unfold get_backlinks in H0. case_eq (eq_dec (Heap.InstanceField o a) f); intros. rewrite <- e in H0. rewrite Backlinks.get_update_same in H0. unfold get_backlinks in IHl. rewrite e in H1. rewrite H1 in IHl. rewrite LocDict.get_update_old in H0; auto. rewrite Backlinks.get_update_old in H0; trivial. apply IHl. trivial. rewrite H1 in H0. unfold get_backlinks in H0. case_eq (eq_dec (Heap.InstanceField o a) f); intros. rewrite e in H0. rewrite Backlinks.get_update_same in H0. unfold LocDict.singleton in H0. rewrite LocDict.get_update_old in H0. rewrite LocDict.get_empty in H0. inversion H0. auto. rewrite Backlinks.get_update_old in H0. apply IHl. 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)