proposition: Lemma spanning_tree_equiv: forall (P1 P2: V -> Prop) (g1: Graph) (v: V) (g2: Graph), (forall x, P1 x <-> P2 x) -> (spanning_tree g1 v P1 g2 <-> spanning_tree g1 v P2 g2).
proof: Proof. cut (forall P1 P2 g1 v g2, (forall x, P1 x <-> P2 x) -> spanning_tree g1 v P1 g2 -> spanning_tree g1 v P2 g2); intros. + split; intros; [apply (H P1 P2) | apply (H P2 P1)]; firstorder. + destruct H0 as [? [? [? ?]]]. split; [|split; [|split]]; intros. - apply (si_stronger_partialgraph _ _ (fun n : V => ~ g1 |= v ~o~> n satisfying P1) (fun n : V => ~ g1 |= v ~o~> n satisfying P1) _ _ (fun _ => True)); auto; intros; pose proof (reachable_by_eq g1 v v0 P1 P2 H); rewrite H4; intuition. - rewrite <- H in H4. specialize (H1 H4). assert ((predicate_partialgraph g2 (reachable_by g1 v P1)) ~=~ (predicate_partialgraph g2 (reachable_by g1 v P2))). { apply partialgraph_proper. reflexivity. apply reachable_by_proper'; try reflexivity. rewrite Same_set_spec; hnf; auto. } apply (is_tree_proper _ _ H5 v v); auto. - apply H2. rewrite (reachable_by_eq _ _ _ P1 P2); auto. - apply H3; rewrite (reachable_by_eq _ _ _ P1 P2); auto. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind Coq.Logic.Classical