proposition: Lemma mark_list_proper_strong: forall (g g': PreGraph V E) m1 l m2 (R_DEC: forall x, In x l -> ReachDecidable g x (negateP m1)) (V_DEC: forall x, In x l -> Decidable (vvalid g x)) (R_DEC': forall x, In x l -> ReachDecidable g' x (negateP m1)) (V_DEC': forall x, In x l -> Decidable (vvalid g' x)), ((predicate_partialgraph g (reachable_by_through_set g l (negateP m1))) ~=~ (predicate_partialgraph g' (reachable_by_through_set g' l (negateP m1)))) -> (mark_list g m1 l m2 <-> mark_list g' m1 l m2).
proof: Proof. intros. assert (forall (g: PreGraph V E) m1 l m2 (R_DEC: forall x, In x l -> ReachDecidable g x (negateP m1)) (V_DEC: forall x, In x l -> Decidable (vvalid g x)), mark_list g m1 l m2 -> forall (g': PreGraph V E), ((predicate_partialgraph g (reachable_by_through_set g l (negateP m1))) ~=~ (predicate_partialgraph g' (reachable_by_through_set g' l (negateP m1)))) -> mark_list g' m1 l m2). 2: intros; split; intros; eapply H0; eauto; symmetry; eauto; reflexivity. intro. apply (ind_RV_DEC g0 (fun m l m' => forall g'0 : PreGraph V E, (predicate_partialgraph g0 (reachable_by_through_set g0 l (negateP m))) ~=~ (predicate_partialgraph g'0 (reachable_by_through_set g'0 l (negateP m))) -> mark_list g'0 m l m')); intros. + constructor. auto. + econstructor. - pose proof mark_proper_strong g0 g'0 m v m'. spec H4; [| rewrite <- H4; auto]. eapply si_stronger_partialgraph with (p := (reachable_by g0 v (negateP m))); [| | exact H3]; intros. * assert (g0 |= v ~o~> v0 satisfying (negateP m) -> reachable_by_through_set g0 (v :: l0) (negateP m) v0); [intro | tauto]. exists v; split; [simpl |]; auto. * pose proof reachable_by_partialgraph_reachable_by_equiv g0 (reachable_by_through_set g0 (v :: l0) (negateP m)) (negateP m) v. spec H5; [intro; intros; exists v; split; [simpl |]; auto |]. pose proof reachable_by_partialgraph_reachable_by_equiv g'0 (reachable_by_through_set g'0 (v :: l0) (negateP m)) (negateP m) v. spec H6; [intro; intros; exists v; split; [simpl |]; auto |]. rewrite H3 in H5. rewrite <- H5 in H6. clear H5. rewrite Same_set_spec in H6. specialize (H6 v0). assert (g'0 |= v ~o~> v0 satisfying (negateP m) -> reachable_by_through_set g'0 (v :: l0) (negateP m) v0); [intro | tauto]. exists v; split; [simpl |]; auto. - apply H0. eapply si_stronger_partialgraph with (p := (reachable_by_through_set g0 l0 (negateP m'))); [| | eauto]; intros. * assert (reachable_by_through_set g0 l0 (negateP m') v0 -> reachable_by_through_set g0 (v :: l0) (negateP m) v0); [intro | tauto]. destruct H4 as [vv [? ?]]; exists vv; split; [simpl |]; auto. eapply reachable_by_weaken; [| eauto]. apply Complement_Included_rev; intro; eapply mark_markeds; [eauto |]. apply R_DEC0; simpl; auto. * assert (reachable_by_through_set g'0 l0 (negateP m') v0 <-> reachable_by_through_set g0 l0 (negateP m') v0). 1: { apply ex_iff; intro. apply and_iff_compat_l_weak; intro. pose proof reachable_by_partialgraph_reachable_by_equiv g0 (reachable_by_through_set g0 (v :: l0) (negateP m)) (negateP m') x. spec H5. 1: { intro; intros; exists x. split; [simpl; auto |]. eapply reachable_by_weaken; eauto. apply Complement_Included_rev; intro; eapply mark_markeds; [eauto |]. apply R_DEC0; simpl; auto. } pose proof reachable_by_partialgraph_reachable_by_equiv g'0 (reachable_by_through_set g'0 (v :: l0) (negateP m)) (negateP m') x. spec H6. 1: { intro; intros; exists x. split; [simpl; auto |]. eapply reachable_by_weaken; eauto. apply Complement_Included_rev; intro; eapply mark_markeds; [eauto |]. apply R_DEC0; simpl; auto. } rewrite H3 in H5. rewrite <- H5 in H6. rewrite Same_set_spec in H6. clear H5; apply H6. } assert (reachable_by_through_set g'0 l0 (negateP m') v0 -> reachable_by_through_set g'0 (v :: l0) (negateP m) v0); [clear H4; intro | tauto]. destruct H4 as [vv [? ?]]; exists vv; split; [simpl |]; auto. eapply reachable_by_weaken; [| eauto]. apply Complement_Included_rev; intro; eapply mark_markeds; [eauto |]. apply R_DEC0; simpl; auto. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2