proposition: Lemma construct_reachable_unfold: forall i, construct_reachable i = match i with | (_, nil, r) => r | (len, g :: l, r) => if le_dec len (length r) then r else let newL := new_working_list l (map (dst G) (edge_func G g)) (g :: r) in construct_reachable (len, newL, g :: r) end.
proof: Proof. intros. destruct i as [[n pr] rslt]. unfold construct_reachable at 1; rewrite Fix_eq. destruct pr; simpl. auto. destruct (le_dec n (length rslt)). auto. unfold construct_reachable; auto. intros; assert (f = g) by (extensionality y; extensionality p; auto); subst; 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