proposition: Lemma spec_list_split: forall {A} (l: list A) P Q R, NoDup l -> (forall x, In x l <-> R x) -> Prop_join P Q R -> exists lp lq, NoDup lp /\ NoDup lq /\ (forall x, In x lp <-> P x) /\ (forall x, In x lq <-> Q x) /\ Permutation l (lp ++ lq).
proof: Proof. intros A l P Q R ? EQUIV [? ?]. assert (forall a, In a l <-> P a \/ Q a) by firstorder. clear EQUIV H0 R; rename H2 into H0. pose proof (spec_or_list_split l P Q H H0). destruct H2 as [lp [lq [? [? [? [? ?]]]]]]. exists lp, lq. split5; auto. + firstorder. cut (P x \/ Q x). 2: left; trivial. intros. rewrite <- H0, H6 in H8. destruct H8; [trivial | exfalso]. apply (H1 x); trivial. apply H5; trivial. + firstorder. cut (P x \/ Q x). 2: right; trivial. intros. rewrite <- H0, H6 in H8. destruct H8; [exfalso | trivial]. apply (H1 x); trivial. apply H4; trivial. + apply NoDup_Permutation; auto. - apply NoDup_app_inv; auto. firstorder. - intro; rewrite in_app_iff. apply H6. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver