proposition: Lemma list_same_diff: forall {A: Type} {EA: EqDec A eq} (l1 l2: list A), NoDup l1 -> NoDup l2 -> exists lsame ldiff, NoDup lsame /\ NoDup ldiff /\ Permutation (lsame++ldiff) l1 /\ incl lsame l2 /\ (forall e, In e ldiff -> ~ In e l2).
proof: Proof. induction l1; intros. + exists nil. exists nil. repeat split. apply NoDup_nil. apply NoDup_nil. rewrite app_nil_l. apply perm_nil. unfold incl; intros; contradiction. unfold not; intros; contradiction. + assert (NoDup l1). apply NoDup_cons_1 in H; auto. apply (IHl1 l2 H1) in H0. destruct H0 as [lsame [ldiff [? [? [? [? ?]]]]]]. destruct (in_dec EA a l2). exists (a::lsame). exists ldiff. repeat split. simpl. apply NoDup_cons. unfold not; intros. assert (In a l1). apply (Permutation_in (l:=(lsame++ldiff))); auto. apply in_or_app. left; auto. apply NoDup_cons_2 in H; auto. auto. auto. simpl; apply perm_skip; auto. unfold incl; intros. destruct H6. subst a; auto. auto. auto. exists lsame. exists (a::ldiff). repeat split. auto. apply NoDup_cons. unfold not; intros. assert (In a l1). apply (Permutation_in (l:=(lsame++ldiff))); auto. apply in_or_app. right; auto. apply NoDup_cons_2 in H. contradiction. auto. apply (Permutation_trans (l:=lsame ++ a :: ldiff) (l':=a::ldiff++lsame)). apply Permutation_app_comm. apply perm_skip. apply (Permutation_trans (l':=lsame ++ ldiff) (l:=ldiff++lsame)). apply Permutation_app_comm. apply H3. auto. intros. destruct H6. subst a. auto. auto. 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