proposition: Lemma reachable_by_ind: forall (g: Gph) x y P, g |= x ~o~> y satisfying P -> x = y \/ exists z, g |= x ~> z /\ g |= z ~o~> y satisfying (fun n => P n /\ n <> x).
proof: Proof. intros. rewrite reachable_acyclic in H. destruct (equiv_dec x y). 1: left; auto. right. destruct H as [path [? [[? ?] [? ?]]]]. destruct path as [v p]. simpl in H0. subst v. destruct p. 1: simpl in H1; exfalso; auto. exists (dst g e). destruct H2. split. - subst x. assert (strong_evalid g e) by (simpl in H2; destruct p; intuition). destruct H0 as [? [? ?]]. do 2 (split; auto). rewrite step_spec. exists e. intuition. - exists (dst g e, p). split; split. + simpl; auto. + rewrite pfoot_cons in H1; auto. + apply valid_path_cons with x. split; auto. + clear H1. red in H3 |-* . simpl in H3 |-* . destruct H3. split. * subst x. apply NoDup_epath_to_vpath_edge with (e := e) in H; simpl; auto. rewrite Forall_forall in H3. split; auto. apply H3. left; easy. * rewrite Forall_forall in *. intros. specialize (H3 _ (in_cons e x0 p H4)). destruct H3. rewrite epath_to_vpath_cons_eq in H; auto. apply NoDup_cons_2 in H. rewrite in_path_eq_epath_to_vpath in H. 2: simpl in *; destruct p; [red in H2|]; intuition. split; split; auto; intro; apply H; unfold In_path; unfold fst, snd; right; exists x0; split; intuition. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec