proposition: Lemma DynamicDGs_Correct: forall p h f_obj f_fsig pivot dg, Heap.get h pivot = Some (Ref f_obj) -> (In dg (DynamicDGs p f_fsig pivot) <-> direct_FieldInDg_dynamic p h (Heap.InstanceField f_obj f_fsig) dg pivot).
proof: Proof. intuition. unfold DynamicDGs 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. rename f into pivot_f. apply in_map_iff in H0. destruct H0 as (dg_fsig, H0). destruct H0. apply in_flat_map in H3. destruct H3 as (dgt, H3). destruct H3. apply filter_In in H3. destruct H3. apply filter_In in H3. destruct H3. case_eq (DATA_GROUP.pivotTarget dgt); intros; rewrite H7 in H5. case_eq d; intros. rewrite H8 in H5. rewrite H8 in H7. clear d H8. case_eq (FsigDec.eq_dec fsig f_fsig); intros. unfold FsigDec.eq in e. rewrite e in H7. clear H5 H8. clear fsig e. split with pivot_obj dg_fsig f_obj f_fsig pivot_obj pivot_fsig pivot_f dgt; trivial. auto. rewrite <- H1; trivial. rewrite H8 in H5; inversion H5. inversion H5. inversion H0. unfold DynamicDGs. rewrite H3. rewrite H5. inversion H2. rewrite <- H16. apply in_map_iff. exists dg_fsig. split. rewrite <- H10; auto. apply in_flat_map. exists dg0. rewrite filter_In. split. split. rewrite filter_In. split. trivial. trivial. rewrite H8. destruct FsigDec.eq_dec. trivial. elim n. auto. 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)