proposition: Lemma pred_sepcon_prop_true_weak: forall (P Q: B -> Prop) (qdec: forall x, Decidable (Q x)) p, (forall x, Q x -> P x) -> pred_sepcon P p |-- pred_sepcon Q p * TT.
proof: Proof. intros. unfold pred_sepcon. normalize. apply (exp_right (filter (fun x => if (qdec x) then true else false) l)). rewrite <- prop_and, sepcon_andp_prop'. remember (filter (fun x0 : B => if qdec x0 then true else false) l) as l'. assert (forall x : B, In x l' <-> Q x). { intros. subst l'. rewrite filter_In. destruct (qdec x); split; intros; auto. - split; auto. apply H in H2. rewrite H0. auto. - destruct H2; inversion H3. - exfalso; auto. } assert (NoDup l') by (subst l'; apply NoDup_filter; auto). apply andp_right. - apply prop_right. split; auto. - apply iter_sepcon_incl_true; auto. intro. rewrite H0, H2. apply H. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.List_ext VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.Morphisms CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize