proposition: Lemma FieldInDg_rac_2: forall p h h' lt obj pivots a dg, Heap.new h p lt = Some (obj, h') -> (FieldInDg_rac p h pivots a dg <-> FieldInDg_rac p h' pivots a dg).
proof: Proof. split; intros. induction H0. apply FieldInDg_rac_step with dg'; trivial. apply FieldInDg_rac_static; trivial. apply FieldInDg_rac_dynamic with pivot; trivial. destruct H0. split with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg; trivial. rewrite <- H4. destruct lt. apply Heap.new_object_no_change with p c u obj; trivial. intro. intro. rewrite H3 in H11. inversion H11. subst. generalize Heap.new_fresh_location. intro. apply H0 in H. clear H0. generalize Heap.get_uncompat. intro. assert (~Heap.Compat h (Heap.InstanceField obj fs)). intro. inversion H2. subst. rewrite H in H10. discriminate H10. apply H0 in H2. rewrite H4 in H2. discriminate H2. apply Heap.new_array_no_change with p t s u obj; trivial. intros. rewrite H3. intro. discriminate H11. subst. apply FieldInDg_rac_same. trivial. induction H0. apply FieldInDg_rac_step with dg'; trivial. apply FieldInDg_rac_static; trivial. apply FieldInDg_rac_dynamic with pivot; trivial. destruct H0. split with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg; trivial. elim classic with (obj = pivot_obj); intro. generalize new_object_field_not_ref. intro. specialize H12 with h p lt obj pivot_fsig pivot_loc h' field_obj. apply H12 in H. elim H; trivial. rewrite H11; trivial. rewrite <- H4. symmetry . destruct lt. apply Heap.new_object_no_change with p c u obj; trivial. intros. rewrite H3. intro. elim H11. inversion H12. trivial. apply Heap.new_array_no_change with p t s u obj; trivial. intros. rewrite H3. intro. discriminate H12. subst. apply FieldInDg_rac_same. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)