proposition: Lemma reachable_toEdgeList: forall root len x r (X: EnumCovered Vertex (reachable g root)), is_list g root -> length (proj1_sig X) <= len -> reachable g root x -> NoDup (listVertices' Vertex Edge r) -> (forall v, reachable g root v -> v <> root -> reachable g x v \/ In v (listVertices' Vertex Edge r)) -> (forall v, In v (listVertices' Vertex Edge r) -> reachable g root v) -> (forall v, reachable g x v -> x <> v -> ~ In v (listVertices' Vertex Edge r)) -> (x <> root -> In x (listVertices' Vertex Edge r)) -> forall v, reachable g root v -> v <> root -> In v (listVertices' Vertex Edge (toEdgeList (len, x, r))).
proof: Proof. intros root len x r ? ?. remember (lengthInput (len, x, r)) as n. assert (lengthInput (len, x, r) <= n) by lia. clear Heqn. revert len x r H0. induction n; intros; simpl; unfold lengthInput in H0; rewrite toEdgeList_unfold; destruct (Compare_dec.le_dec len (length r)); [apply (listVertices'_In_length_reachable _ _ _ _ len _ X) | simpl; exfalso; intuition | apply (listVertices'_In_length_reachable _ _ _ _ len _ X)| ]; auto. assert (HS: Forall (evalid g) (edge_func g x)) by (rewrite Forall_forall; intros; rewrite edge_func_spec in H10; destruct H10; auto). simpl. destruct (filterE (edge_func g x)) eqn:? . + specialize (H4 _ H8 H9). destruct H4; auto. clear IHn. apply reachable_by_ind in H4. destruct H4. 1: subst x; apply H7; auto. exfalso. destruct H4 as [z [[? [? ?]] ?]]. rewrite step_spec in H11. destruct H11 as [e [? [? ?]]]. assert (vvalid g (dst g e) /\ In e (edge_func g x)) by (split; [rewrite H14 | rewrite edge_func_spec; split]; auto). rewrite <- filter_valid in H15; auto. rewrite Heql in H15. simpl in H15; auto. + specialize (IHn len (dst g e) ((e, dst g e) :: r)). assert (S: len - length ((e, dst g e) :: r) <= n) by (simpl; clear -H0; intuition). specialize (IHn S H1); clear S. assert (g |= x ~> (dst g e)). { assert (In e (e :: l)) by (simpl; left; auto). rewrite <- Heql in H10. rewrite filter_valid in H10; auto. rewrite edge_func_spec in H10. hnf. rewrite step_spec. destruct H10 as [? [? ?]]. apply reachable_foot_valid in H2. split; [|split; [|exists e]]; auto. } assert (vvalid g root) by (apply reachable_head_valid in H2; auto). apply IHn; auto; clear IHn. * apply reachable_edge with x; auto. * simpl. apply NoDup_cons; auto. apply H6. 1: apply reachable_edge with x; auto; apply reachable_refl; apply reachable_foot_valid in H2; auto. intro. subst x. apply (is_list_no_self_edge g root) in H10; auto. * intros. specialize (H4 _ H12 H13). simpl. destruct H4. 2: right; right; auto. apply reachable_by_ind in H4. destruct H4. 1: right; right; subst x; apply H7; auto. destruct H4 as [z [? ?]]. pose proof (is_list_edge_dst_the_same _ _ _ _ _ H H2 H4 H10). subst z. apply reachable_by_is_reachable in H14. left; auto. * simpl; intros. destruct H12. 2: apply H5; auto. subst v0. apply reachable_edge with x; auto. * intros. simpl. intro. destruct H14; auto. revert H14. apply H6. 1: apply edge_reachable with (dst g e); auto. intro. subst v0. apply (is_list_no_edge_loop g root x (dst g e)); auto. * simpl; intros; left; auto. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph