proposition: Lemma spec_or_list_split: forall {A} (l: list A) P Q, NoDup l -> (forall x, In x l <-> P x \/ Q x) -> exists lp lq, NoDup lp /\ NoDup lq /\ (forall x, In x lp -> P x) /\ (forall x, In x lq -> Q x) /\ (forall x, In x l <-> In x lp \/ In x lq).
proof: Proof. intros. pose proof (fun x => proj1 (H0 x)). clear H0. induction l. + exists nil, nil. split5; [constructor | constructor |..]; intro x; simpl; tauto. + spec IHl; [inversion H; auto |]. spec IHl; [intros; apply H1; simpl; auto |]. destruct IHl as [lp [lq [? [? [? [? ?]]]]]]. destruct (H1 a (or_introl eq_refl)); [exists (a :: lp), lq | exists lp, (a :: lq)]; split5; intros; auto. - constructor; auto. inversion H; subst. firstorder. - destruct H7; [subst |]; auto. - simpl; specialize (H5 x); tauto. - constructor; auto. inversion H; subst. firstorder. - destruct H7; [subst |]; auto. - simpl; specialize (H5 x); tauto. 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