proposition: Lemma pred_sepcon_ocon: forall (P Q R: B -> Prop) p (eq_dec : forall x y : B, {x = y} + {x <> y}), (forall x, Decidable (P x)) -> (forall x, Decidable (Q x)) -> (forall a, P a \/ Q a <-> R a) -> (forall x : B, precise (p x)) -> joinable p -> pred_sepcon P p ⊗ pred_sepcon Q p = pred_sepcon R p.
proof: Proof. intros. unfold pred_sepcon. apply pred_ext. + normalize_overlap; intro lP. do 2 normalize_overlap. rename x into lQ. apply (exp_right (nodup eq_dec (lP ++ lQ))). rewrite (iter_sepcon_ocon eq_dec); auto. rewrite <- prop_and. apply andp_right; auto. apply prop_right. split; intros. 2: apply NoDup_nodup. split; intros. - rewrite nodup_In in H6. rewrite <- H. rewrite in_app_iff in H6. rewrite H2 in H6. rewrite H4 in H6. auto. - rewrite nodup_In. rewrite <- H in H6. rewrite in_app_iff. rewrite H2. rewrite H4. auto. + normalize. intro lR; intros. normalize. normalize_overlap. assert (forall a, In a lR <-> P a \/ Q a) by (clear -H H2; firstorder). destruct (or_dec_prop_list_split _ _ _ H3 X X0 H4) as [lP [lQ [? [? [? [? ?]]]]]]. apply (exp_right lP). normalize_overlap. apply (exp_right lQ). rewrite <- prop_and. normalize_overlap. apply andp_right. - apply prop_right. intuition. - rewrite <- iter_sepcon_ocon' with (l := lR); auto. 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