proposition: Lemma ValidDGTree_exists: forall p bl ep m, forall f, exists dg, ValidDGTree p bl ep f m dg.
proof: Proof. intros p bl ep m. assert (exists n , n = LocSet.cardinal m). exists (LocSet.cardinal m);trivial. destruct H as [n H]. generalize n m H. clear m n H. induction n. intros. set (ad := get_backlinks bl f). set (f'list' := (LocSet.elements (fold_right (LocSet.union) LocSet.empty (LocDict.filter ad (fun f'' => ~ LocSet.In f'' ep)))) +++ (StaticDGs p f)). exists (DGNode f nil). apply ValidDGTree_def with (dgs := nil) (ad := ad) (f'list' := f'list') (f'list := nil); trivial. induction f'list'. simpl; trivial. simpl. symmetry in H. rewrite <- LocSetProp.cardinal_Empty in H. replace (LocSet.mem a m) with false . trivial. case_eq (LocSet.mem a m); intro; trivial. apply LocSet.mem_2 in H0. unfold LocSet.Empty in H. destruct H with a; trivial. intros. simpl in H0. inversion H0. intros. set (ad := get_backlinks bl f). set (f'list' := (LocSet.elements (fold_right (LocSet.union) LocSet.empty (LocDict.filter ad (fun f'' => ~ LocSet.In f'' ep)))) +++ (StaticDGs p f)). set (f'list := filter (fun f'' => LocSet.mem f'' m) f'list'). set (dgsEx := (exists dgs, length dgs = length f'list /\ forall n f'' f' dgs', n < length dgs -> nth n f'list f'' = f' -> nth n dgs (DGNode f'' []) = dgs' -> ValidDGTree p bl ep f' (LocSet.remove f' m) dgs')). unfold ad in f'list'. elim classic with dgsEx; intros. destruct H0 as (dgs, H0). clear dgsEx. destruct H0. exists (DGNode f dgs). apply ValidDGTree_def with (dgs := dgs) (ad := ad) (f'list' := f'list') (f'list := f'list); trivial. elim H0. unfold dgsEx. apply not_all_not_ex. intro. clear H0 dgsEx. induction f'list'. specialize H1 with (nil (A:=DGTree)). destruct H1. split. trivial. intros. inversion H0. apply IHf'list'. clear IHf'list'. intro. intro. case_eq (LocSet.mem a m); intro. specialize IHn with (m := LocSet.remove a m). destruct IHn with a. apply eq_add_S. rewrite H. symmetry . apply LocSetProp.remove_cardinal_1. apply LocSet.mem_2; trivial. apply H1 with (cons x n0). split. unfold f'list. simpl. rewrite H2. simpl. lia. destruct H0. intros. unfold f'list in H6. simpl in H6. rewrite H2 in H6. case_eq n1; intros. simpl in H7. rewrite H8 in H7. simpl in H6. rewrite H8 in H6. rewrite <- H6. rewrite <- H7. trivial. simpl in H7. apply H4 with n2 f''. rewrite H8 in H5. simpl in H5. auto with *. rewrite H8 in H6. simpl in H6. trivial. rewrite H8 in H7. trivial. apply H1 with n0. unfold f'list. simpl. rewrite 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)