proposition: Lemma tri_list_split {A : Type} (eq_dec : forall x y : A, {x = y} + {x <> y}): forall (l l1 l2 : list A), NoDup l -> NoDup l1 -> NoDup l2 -> l ~= (l1 ++ l2) -> exists i1 i2 i3, Permutation l1 (i1 ++ i2) /\ Permutation l2 (i2 ++ i3) /\ Permutation l (i1 ++ i2 ++ i3).
proof: Proof. intros. remember (intersect eq_dec l1 l2) as j2. remember (subtract eq_dec l1 j2) as j1. remember (subtract eq_dec l2 j2) as j3. exists j1, j2, j3. assert (Permutation l1 (j1 ++ j2)). rewrite Heqj1. apply subtract_permutation. auto. rewrite Heqj2. apply intersect_nodup. auto. intro y; intros. rewrite Heqj2 in H3. rewrite <- intersect_property in H3. intuition. split. auto. assert (Permutation l2 (j2 ++ j3)). rewrite Heqj3. apply Permutation_trans with (subtract eq_dec l2 j2 ++ j2). apply subtract_permutation. auto. rewrite Heqj2. apply intersect_nodup. auto. intro y; intros. rewrite Heqj2 in H4. rewrite <- intersect_property in H4. intuition. apply Permutation_app_comm. split; auto. remember (subtract eq_dec l l2) as j4. apply Permutation_trans with (j4 ++ l2). rewrite Heqj4. apply subtract_permutation; auto. destruct H2. repeat intro. apply (H5 a). apply in_or_app; right; auto. apply Permutation_app. apply NoDup_Permutation. rewrite Heqj4. apply subtract_nodup; auto. rewrite Heqj1. apply subtract_nodup; auto. rewrite Heqj1, Heqj4. destruct H2. hnf in H2, H5. intro x; split; intros; rewrite <- subtract_property in H6; destruct H6; rewrite <- subtract_property; split. apply H2 in H6. apply in_app_or in H6. destruct H6; intuition. rewrite Heqj2. intro; apply H7. rewrite <- intersect_property in H8. destruct H8; auto. apply H5. apply in_or_app; left; auto. intro; apply H7. rewrite Heqj2. rewrite <- intersect_property. split; 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