proposition: Lemma PivotTargets_Correct: forall p h f_fsig f_obj pivot, Heap.get h pivot = Some (Ref f_obj) -> (In f_fsig (PivotTargets p pivot) <-> exists dg, direct_FieldInDg_dynamic p h (Heap.InstanceField f_obj f_fsig) dg pivot).
proof: Proof. intuition. unfold PivotTargets in H0. case_eq pivot; intros; rewrite H1 in H0; try inversion H0. rename o into pivot_obj. rename f into pivot_fsig. case_eq (findField p pivot_fsig); intros; rewrite H2 in H0; try inversion H0. apply some_list_list in H0. apply in_map_iff in H0. destruct H0 as (dg, H0). destruct H0. case_eq (DATA_GROUP.pivotTarget dg); intros; rewrite H4 in H0. case_eq d; intros; rewrite H5 in H0. apply filter_In in H3. destruct H3. generalize DATA_GROUP.dataGroups_not_nil. intro. specialize H7 with dg. case_eq (DATA_GROUP.dataGroups dg); intros. elim H7; trivial. exists (Heap.InstanceField pivot_obj f0). split with pivot_obj f0 f_obj f_fsig pivot_obj pivot_fsig f dg; trivial. rewrite <- H1; trivial. inversion H0. rewrite H10 in H5. rewrite <- H5. trivial. rewrite H8. auto with *. inversion H0. destruct H0 as (dg, H0). inversion H0. unfold PivotTargets. rewrite H3. rewrite H5. apply some_list_list. apply in_map_iff. exists dg0. rewrite H8. inversion H2. split;auto. apply filter_In. split. 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)