proposition: Lemma CorrectBacklinks_new: forall st p cn um obj h' , Heap.new st@h p (Heap.ObjectObject cn um) = Some (obj, h') -> (CorrectBacklinks p st <-> CorrectBacklinks p st [h := h']).
proof: Proof. intuition. intros. unfold CorrectBacklinks. unfold CorrectBacklink. intros. destruct H0 with f dg pivot. simpl in *. intuition. apply H1. clear H1 H2. inversion H3. split with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg0; trivial. assert (pivot_obj <> obj). intro. rewrite H15 in H4. apply Rac2.new_object_field_not_ref with (fsig := pivot_fsig) (loc := pivot) (r := field_obj) in H; trivial. elim H; trivial. rewrite <- H5. symmetry . apply Heap.new_object_no_change with p cn um obj; trivial. intros. rewrite H4. intro. inversion H16. elim H15; trivial. clear H3 H2. inversion H4. split with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg0; trivial. assert (pivot_obj <> obj). intro. rewrite H15 in H3. apply Heap.new_fresh_location in H. assert (~Heap.Compat st @h pivot). intro. destruct H16. inversion H3. inversion H3. rewrite H18 in H16. rewrite H in H16. inversion H16. inversion H3. apply Heap.get_uncompat in H16. rewrite H5 in H16. inversion H16. rewrite <- H5. apply Heap.new_object_no_change with p cn um obj; trivial. intros. rewrite H3. intro. inversion H16. elim H15; trivial. unfold CorrectBacklinks. unfold CorrectBacklink. intros. destruct H0 with f dg pivot. simpl in *. intuition. apply H1. clear H1 H2. inversion H3. split with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg0; trivial. assert (pivot_obj <> obj). intro. rewrite H15 in H4. apply Heap.new_fresh_location in H. assert (~Heap.Compat st @h pivot). intro. destruct H16. inversion H4. inversion H4. rewrite H18 in H16. rewrite H in H16. inversion H16. inversion H4. apply Heap.get_uncompat in H16. rewrite H5 in H16. inversion H16. rewrite <- H5. apply Heap.new_object_no_change with p cn um obj; trivial. intros. rewrite H4. intro. inversion H16. elim H15; trivial. clear H3 H2. inversion H4. split with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg0; trivial. assert (pivot_obj <> obj). intro. rewrite H15 in H3. apply Rac2.new_object_field_not_ref with (fsig := pivot_fsig) (loc := pivot) (r := field_obj) in H; trivial. elim H; trivial. rewrite <- H5. symmetry . apply Heap.new_object_no_change with p cn um obj; trivial. intros. rewrite H3. intro. inversion H16. elim H15; 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)