proposition: Lemma finite_reachable_computable': forall x (X: EnumCovered V (reachable G x)) l', vvalid G x -> l' = construct_reachable (length (proj1_sig X), x :: nil, @nil V) -> reachable_list G x l' /\ NoDup l'.
proof: Proof. intros. subst l'. destruct X as [l [? ?H]]. simpl. clear n. set (i := (length l, x :: nil, @nil V)). unfold Ensembles.In in *. pose proof sound_by_invariance' (fun i => reachable_bounded x i /\ Forall_reachable x i /\ input_nodup i /\ reachable_covered x i /\ edge_closed i) (fun l => res_reachable_sound x l /\ res_nodup l /\ res_reachable_covered x l /\ res_reachable_closed l) i as MainTheorem. spec MainTheorem; [| spec MainTheorem; [| spec MainTheorem; [| spec MainTheorem]]]; [clear MainTheorem .. |]. + subst i; repeat split; simpl. - unfold reachable_bounded; simpl. intros. rewrite Forall_forall in H2. assert (incl l0 l). unfold incl. exact (fun a H => H0 a (H2 a H)). apply NoDup_incl_length; auto. - unfold Forall_reachable; simpl. repeat constructor. apply reachable_refl; auto. - constructor. - intros; auto. - unfold reachable_covered; simpl. intros. exists x. repeat split; auto. apply reachable_refl; auto. - unfold edge_closed; simpl. intros; auto. + intros ? [? [? [? _]]]. unfold reachable_bounded, Forall_reachable, input_nodup, rch1_is_bound in *. intros. rewrite Forall_app_iff in H2. destruct H2. destruct H3. specialize (H1 (nodup equiv_dec (rch2 i0) ++ rch3 i0)). spec H1. 1: { apply NoDup_app_inv. + apply NoDup_nodup. + auto. + intros; intro. rewrite nodup_In in H7. eapply H6; eauto. } spec H1. 1: { apply Forall_app_iff; split; auto. rewrite Forall_forall in H2 |- *; intros. rewrite nodup_In in H7. apply H2; auto. } rewrite app_length in H1. assert (length (nodup equiv_dec (rch2 i0)) = 0) by lia. clear - H7. remember (rch2 i0). clear Heql. induction l; auto. simpl in H7. destruct (in_dec equiv_dec a l). * specialize (IHl H7). subst. inversion i. * simpl in H7. inversion H7. + apply invariant_and; [apply Invariance0 |]. apply invariant_and; [apply Invariance1 |]. apply invariant_and; [apply Invariance2 |]. apply invariant_and; [apply Invariance3 | apply Invariance4]. + apply sound1_and; [eapply sound1_strengthen; [| apply sound1_inv1]; intros; tauto |]. apply sound1_and; [eapply sound1_strengthen; [| apply sound1_inv2]; intros; tauto |]. apply sound1_and; [eapply sound1_strengthen; [| apply sound1_inv3]; intros; tauto |]. eapply sound1_strengthen; [| apply sound1_inv4]; intros; tauto. + unfold res_reachable_sound, res_nodup, res_reachable_covered, res_reachable_closed, reachable_list in *. destruct MainTheorem as [? [? [? ?]]]; split; [intro; split; intro |]. - clear - H1 H5. rewrite Forall_forall in H1; apply H1; auto. - destruct (H3 _ H5) as [z [? ?]]. apply H4 with z; auto. - auto. Qed.
imports: Coq.Sets.Finite_sets Coq.Arith.Arith Coq.Logic.ProofIrrelevance Coq.Logic.FunctionalExtensionality Coq.Sorting.Permutation Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles Coq.Lists.List VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph