proposition: Lemma iter_sepcon_ocon' (eq_dec: forall x y : B, {x = y} + {x <> y}): forall l l1 l2 p, NoDup l -> NoDup l1 -> NoDup l2 -> (forall x, precise (p x)) -> joinable p -> (forall x, In x l <-> In x l1 \/ In x l2) -> iter_sepcon l p = iter_sepcon l1 p ⊗ iter_sepcon l2 p.
proof: Proof. intros until p. intros NoDupl NoDupl1 NoDupl2 PRECISE EQUIV JOINABLE. assert (l ~= (l1 ++ l2)) by (apply eq_as_set_spec; intros; rewrite in_app_iff; auto). apply pred_ext. + destruct (tri_list_split eq_dec NoDupl NoDupl1 NoDupl2 H) as [i1 [i2 [i3 [? [? ?]]]]]. rewrite (iter_sepcon_permutation _ H0). rewrite (iter_sepcon_permutation _ H1). rewrite (iter_sepcon_permutation _ H2). rewrite !iter_sepcon_app_sepcon. rewrite <- sepcon_assoc. apply tri_sepcon_ocon. + destruct (double_list_split eq_dec NoDupl1 NoDupl2) as [i1 [i2 [i3 [? [? ?]]]]]. rewrite (iter_sepcon_permutation _ H0). rewrite (iter_sepcon_permutation _ H1). rewrite !iter_sepcon_app_sepcon. eapply derives_trans; [apply ocon_derives; apply sepcon_ocon |]. rewrite ocon_assoc. rewrite <- (ocon_assoc (iter_sepcon i2 p)). rewrite <- precise_ocon_self by (apply precise_iter_sepcon; auto). assert (Permutation l (i1 ++ i2 ++ i3)). 1: { apply NoDup_Permutation; auto. intros. rewrite JOINABLE. rewrite !in_app_iff. pose proof (Permutation_in x H0). pose proof (Permutation_in x H1). pose proof (Permutation_in x (Permutation_sym H0)). pose proof (Permutation_in x (Permutation_sym H1)). rewrite in_app_iff in *. tauto. } rewrite (iter_sepcon_permutation _ H3). rewrite !iter_sepcon_app_sepcon. eapply derives_trans; [ apply ocon_sepcon; apply disj_ocon_right | apply sepcon_derives; [auto | apply ocon_sepcon]]; apply iter_sepcon_app_joinable; auto; intros; apply NoDup_app_iff in H2; destruct H2 as [? [? ?]]; generalize (NoDup_app_not_in _ _ _ H5 x); intro; specialize (H6 x); auto; specialize (H6 H4); intro; apply H6; apply in_or_app; 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