proposition: Lemma spanning_list_trans': forall P g1 g2 g3 l1 l2, Forall (evalid g1) (l1 ++ l2) -> spanning_list' P g1 l1 g2 -> spanning_list' (fun x => P x /\ ~ reachable_by_through_set g1 (map (dst g1) l1) P x) g2 l2 g3 -> spanning_list' P g1 (l1 ++ l2) g3.
proof: Proof. intros. remember (fun x : V => P x /\ ~ reachable_by_through_set g1 (map (dst g1) l1) P x) as P0. induction H1. + rewrite app_nil_r. induction H0. - apply spanning_list_nil'. rewrite H0. auto. - apply spanning_list_cons' with g0; auto. rewrite <- si_edge_spanning_tree'. apply H2. apply H1. + assert (Forall (evalid g1) (l1 ++ es)). { rewrite Forall_forall in H |-* . intros. apply H. rewrite app_assoc. apply in_or_app. left; auto. } specialize (IHspanning_list' H3 H0 HeqP0). rewrite app_assoc. apply spanning_list_cons' with g2; auto. rewrite (edge_spanning_tree_equiv _ (fun x : V => P0 x /\ ~ reachable_by_through_set g0 (map (dst g0) es) P0 x)); auto. intros. subst P0. split; intros. - destruct H4. split; [split|]; auto. * intro. apply H5. destruct H6 as [s [? ?]]. exists s. split; auto. rewrite Coqlib.list_append_map. apply in_or_app. left; auto. * clear H1 H2 IHspanning_list' H. induction H0. 1: { rewrite app_nil_l in *. simpl. intro. apply H5. clear H5. assert (map (dst g0) es = map (dst g1) es). { clear H0. induction es; simpl; auto. f_equal. + destruct H as [? [? [? ?]]]. rewrite Forall_forall in H3. assert (evalid g1 a) by (apply H3, in_eq). assert (evalid g0 a) by (rewrite <- H0; auto). symmetry. apply H2; auto. + apply IHes. rewrite Forall_forall in H3 |-* . intros. apply H3. apply in_cons; auto. } rewrite H1 in H0. rewrite (si_reachable_by_through_set g1 g0 _ _ (fun x0 : V => P x0 /\ ~ reachable_by_through_set g1 nil P x0)); auto. hnf. intros. simpl. rewrite reachable_by_through_nil. intuition. } 1: { assert (Forall (evalid g1) (es0 ++ es)). { rewrite Forall_forall in H3 |-* . intros. apply H3. apply in_app_or in H1. apply in_or_app. destruct H1; [left | right]; auto. apply in_or_app. left; auto. } specialize (IHspanning_list' H1 H4). assert (~ reachable_by_through_set g1 (map (dst g1) (es0 ++ es)) P x). { intro. apply H5. destruct H2 as [s [? ?]]. exists s. split; auto. rewrite Coqlib.list_append_map in H2 |-* . apply in_app_or in H2. apply in_or_app. destruct H2; [left | right]; auto. rewrite Coqlib.list_append_map. apply in_or_app. left; auto. } specialize (IHspanning_list' H2). Abort. Inductive spanning_list : (V -> Prop) -> Graph -> list E -> Graph -> Prop := | spanning_list_nil: forall P g1 g2, g1 ~=~ g2 -> spanning_list P g1 nil g2 | spanning_list_cons: forall P g1 g2 g3 e es, edge_spanning_tree g1 e P g2 -> spanning_list (fun x => P x /\ ~ g1 |= (dst g1 e) ~o~> x satisfying P) g2 es g3 -> spanning_list P g1 (e :: es) g3. Lemma spanning_list_eq: forall P g1 g2 es, Forall (evalid g1) es -> (spanning_list P g1 es g2 <-> spanning_list' P g1 es g2). Proof. intros. split; intros; induction H0. + apply spanning_list_nil'; auto. + pose proof (app_cons_assoc nil es e). do 2 rewrite app_nil_l in H2. rewrite H2. Abort. Lemma spanning_list_derive: forall (P1 P2: V -> Prop) (g1 g2 : Graph) e, (forall x, P1 x <-> P2 x) -> spanning_list P1 g1 e g2 -> spanning_list P2 g1 e g2. Proof. intros. revert P1 P2 g1 H H0. induction e; intros. + constructor. inversion H0. auto. + inversion H0. subst. apply spanning_list_cons with g3. - rewrite <- (edge_spanning_tree_equiv P1 P2); auto. - apply (IHe (fun x : V => P1 x /\ ~ g1 |= dst g1 a ~o~> x satisfying P1) (fun x : V => P2 x /\ ~ g1 |= dst g1 a ~o~> x satisfying P2)); auto. intros; split; intros; destruct H1; split. * rewrite <- H; auto. * rewrite <- (reachable_by_eq _ _ _ P1 P2); auto. * rewrite H; auto. * 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