proposition: Lemma FieldInDg_rac3_Correct: forall p ep st f dg , CorrectBacklinks p st -> (FieldInDg_rac2 p st@h ep (LocSet.singleton f) f dg <-> FieldInDg_rac3 p st@bl ep f dg = true).
proof: Proof. split;intros. unfold FieldInDg_rac3 in *. apply InDGTree_Correct. induction H0. elim ValidDGTree_exists with p st@bl ep (LocSetAll \ s) f; trivial. intro tree. intro. replace (BuildDGTree p st@bl ep f (LocSetAll \ s)) with tree . destruct tree. inversion H3. assert (In dg' f'list'). rewrite <- H6. apply in_or_app. right. apply StaticDGs_Correct; trivial. assert (In dg' f'list). clear H6. generalize f'list, H7, H11. clear f'list H7 H11 H8 H9. assert (LocSet.mem dg' (LocSetAll \ s) = true). rewrite LocSetPropEq.diff_mem. apply andb_true_iff. split. apply LocSet.mem_1. apply LocSetAll_def. apply negb_true_iff. apply LocSetPropEq.mem_3; trivial. induction f'list'. intros. inversion H11. intros. simpl in H11. destruct H11. subst. simpl. rewrite H6. simpl; left; trivial. simpl in H7. case_eq (LocSet.mem a (LocSetAll \ s)); intros; rewrite H9 in H7. destruct f'list. inversion H7. specialize IHf'list' with f'list. inversion H7. rewrite H13. apply IHf'list' in H13. auto with *. trivial. apply IHf'list'. trivial. trivial. apply in_nth with (d:=f) in H12. destruct H12 as [n H12]. destruct H12. inversion H4. set (tree' := nth n dgs0 (DGNode f [])). specialize H9 with n f dg' tree'. case_eq (LocDec.eq_dec dg f); intros. unfold LocDec.eq in e. apply InDG_base with dgs0. rewrite e; trivial. apply InDG_step with dgs0 f tree'; trivial. unfold tree'. apply nth_In. rewrite H8; trivial. assert (BuildDGTree p st@bl ep dg' (LocSetAll \ (LocSet.add dg' s)) = tree'). rewrite <- BuildDGTree_def. apply ValidDGTree_EqualSets with (n := LocSet.cardinal ((LocSetAll \ s) \ {dg'})) (s1 := (LocSetAll \ s) \ {dg'}); trivial. apply LocSet_diff_remove_diff_add. apply H9; trivial. rewrite H8; trivial. rewrite <- H17. trivial. symmetry . apply BuildDGTree_def; trivial. elim ValidDGTree_exists with p st@bl ep (LocSetAll \ s) f; trivial. intro tree. intro. replace (BuildDGTree p st@bl ep f (LocSetAll \ s)) with tree . destruct tree. inversion H4. assert (In dg' f'list'). rewrite <- H7. apply in_or_app. left. unfold CorrectBacklinks in H. unfold CorrectBacklink in H. unfold get_backlinks in H6. rewrite H in H0. destruct H0 as [amd H0]. destruct H0. rewrite <- In_InA. apply LocSet.elements_1. apply fold_right_union. elim LocDict_get_some with st@bl f pivot amd;trivial. intros. rewrite H13 in H6. rewrite <- H6. exists amd. split;trivial. apply LocDict.filter_1. exists pivot. unfold get_backlinks in H0. rewrite H13 in H0. tauto. assert (In dg' f'list). clear H7. generalize f'list, H8, H12. clear f'list H8 H12 H9 H10. assert (LocSet.mem dg' (LocSetAll \ s) = true). rewrite LocSetPropEq.diff_mem. apply andb_true_iff. split. apply LocSet.mem_1. apply LocSetAll_def. apply negb_true_iff. apply LocSetPropEq.mem_3; trivial. induction f'list'. intros. inversion H12. intros. simpl in H12. destruct H12. subst. simpl. rewrite H7. simpl; left; trivial. simpl in H8. case_eq (LocSet.mem a (LocSetAll \ s)); intros; rewrite H10 in H8. destruct f'list. inversion H8. specialize IHf'list' with f'list. inversion H8. rewrite H14. apply IHf'list' in H14. auto with *. trivial. apply IHf'list'. trivial. trivial. apply in_nth with (d := f) in H13. destruct H13 as [n H13]. destruct H13. inversion H4. set (tree' := nth n dgs0 (DGNode f [])). specialize H10 with n f dg' tree'. case_eq (LocDec.eq_dec dg f); intros. unfold LocDec.eq in e. apply InDG_base with dgs0. rewrite e; trivial. apply InDG_step with dgs0 f tree'; trivial. unfold tree'. apply nth_In. rewrite H9; trivial. assert (BuildDGTree p st@bl ep dg' (LocSetAll \ (LocSet.add dg' s)) = tree'). rewrite <- BuildDGTree_def. apply ValidDGTree_EqualSets with (n := LocSet.cardinal ((LocSetAll \ s) \ {dg'})) (s1 := (LocSetAll \ s) \ {dg'}); trivial. apply LocSet_diff_remove_diff_add. apply H10; trivial. rewrite H9; trivial. rewrite <- H23. trivial. symmetry . apply BuildDGTree_def; trivial. assert(exists tree, BuildDGTree p st@bl ep f (LocSetAll \s) = tree). exists (BuildDGTree p st@bl ep f (LocSetAll \s)). trivial. destruct H1 as [tree H1]. apply BuildDGTree_def in H1. replace (BuildDGTree p st@bl ep f (LocSetAll \s)) with tree. inversion H1. apply InDG_base with dgs. rewrite <- H0. trivial. symmetry. apply BuildDGTree_def;trivial. apply FieldInDg_rac2_EqualSet with (LocSetAll \ (LocSetAll \ (LocSet.singleton f))). unfold FieldInDg_rac3 in *. apply InDGTree_Correct in H0. assert (exists tree, BuildDGTree p st@bl ep f (LocSetAll \ LocSet.singleton f) = tree). exists (BuildDGTree p st@bl ep f (LocSetAll \ LocSet.singleton f)). trivial. destruct H1 as (tree, H1). rewrite H1 in H0. apply BuildDGTree_def in H1. induction H1. destruct H0. rewrite H0 in H1. inversion H1. apply FieldInDg_rac2_base. trivial. rewrite H0 in H1. inversion H1. apply in_nth with (d := DGNode f []) in H9. destruct H9 as (n, H9). destruct H9. set (f' := nth n f'list f). assert (In f' f'list). apply nth_In. rewrite <- H5. rewrite <- H13; trivial. assert (LocSet.In f' m). clear H3. generalize f'list, H4, f', H14. clear f'list H4 f' H14 H5 H6 H7. induction f'list'. intros. simpl in H4. rewrite <- H4 in H14. inversion H14. intros. simpl in H4. case_eq (LocSet.mem a m); intros; rewrite H3 in H4. destruct f'list. inversion H4. simpl in H14. destruct H14. rewrite <- H5. inversion H4. rewrite <- H7. apply LocSet.mem_2; trivial. apply IHf'list' with f'list. inversion H4; trivial. trivial. apply IHf'list' with f'list; trivial. specialize H6 with n f f' tree'. specialize H7 with n f f' tree'. assert (In f' f'list'). rewrite <- H4 in H14. rewrite filter_In in H14. destruct H14; trivial. rewrite <- H3 in H16. apply in_app_or in H16. destruct H16. unfold CorrectBacklinks in H. unfold CorrectBacklink in H. apply In_InA in H16. apply LocSet.elements_2 in H16. apply fold_right_union in H16. destruct H16 as (ams, H16). rewrite LocDict.filter_1 in H16. destruct H16. destruct H16 as (pivot, H16). destruct H16. apply FieldInDg_rac2_dynamic with pivot f'; trivial. rewrite H. exists ams. split;trivial. rewrite H2;trivial. intro. apply LocSet.diff_2 in H19. elim H19;trivial. apply FieldInDg_rac2_EqualSet with (LocSetAll \ (m \ {f'})). rewrite <- H13 in H7. apply H7; trivial. apply LocSet_remove_diff_remove_add. apply LocSetAll_def. apply StaticDGs_Correct in H16. apply FieldInDg_rac2_static with f'; trivial. intro. apply LocSet.diff_2 in H17. elim H17; trivial. apply FieldInDg_rac2_EqualSet with (LocSetAll \ (m \ {f'})). rewrite <- H13 in H7. apply H7; trivial. apply LocSet_remove_diff_remove_add. apply LocSetAll_def. split; intros. apply LocSet.diff_2 in H1. assert (LocSet.In a LocSetAll). apply LocSetAll_def. assert (~ LocSet.In a (LocSetAll \ {f})). intro; elim H1. apply remove_diff_singleton; trivial. apply LocSet.singleton_2. unfold LocSet.E.eq. case_eq (MP.FM.eq_dec f a); intros. auto. elim H3. apply LocSet.remove_2. trivial. trivial. apply LocSet.diff_3. apply LocSetAll_def. intro. apply LocSet.diff_2 in H2. elim H2; 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)