proposition: Lemma new_object_field_not_ref: forall h p lt obj fsig loc h' r, Heap.new h p lt = Some (obj, h') -> loc = Heap.InstanceField obj fsig -> Heap.get h' loc <> Some (Ref r).
proof: Proof. intros. destruct lt. elim classic with (defined_field p c fsig). intros. destruct H1 as (f, H1). generalize Heap.new_defined_object_field. intro. specialize H2 with h p c u fsig f obj h'. rewrite H0. rewrite H2; trivial. intro. inversion H3. elim init_field_value_not_ref with f r; trivial. intro. generalize Heap.new_undefined_object_field. intro. specialize H2 with h p c u fsig obj h'. rewrite H0. rewrite H2; trivial. intro. discriminate H3. intro. generalize Heap.get_uncompat. intro. specialize H2 with h' loc. rewrite H2 in H1. discriminate H1. clear H2. intro. destruct H2. discriminate H0. inversion H0. subst. generalize Heap.new_typeof. intro. apply H3 in H. rewrite H in H2. inversion H2. discriminate H0. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)