proposition: Lemma ac_syntactic_aux : forall (l1 l2 l3 l4 : list A), permut0 eq_A (l1 ++ l2) (l3 ++ l4) -> (exists u1, exists u2, exists u3, exists u4, permut0 eq_A l1 (u1 ++ u2) /\ permut0 eq_A l2 (u3 ++ u4) /\ permut0 eq_A l3 (u1 ++ u3) /\ permut0 eq_A l4 (u2 ++ u4)).
proof: Proof. induction l1 as [ | a1 l1]; intros l2 l3 l4 P. exists (nil : list A); exists (nil : list A); exists l3; exists l4; simpl. repeat split. apply (permut0_refl eq_proof). intuition. apply (permut0_refl eq_proof). apply (permut0_refl eq_proof). simpl in P. assert (a1_in_l3l4 := @cons_permut0_mem _ _ eq_proof _ _ _ _ (@Equivalence_Reflexive _ _ eq_proof a1) P). rewrite <- mem_or_app in a1_in_l3l4; destruct a1_in_l3l4 as [a1_in_l3 | a1_in_l4]. generalize (mem_split_set _ _ eq_bool_ok _ _ a1_in_l3). intros [a1' [l3' [l3'' [a1_eq_a1' [H _]]]]]; simpl in a1_eq_a1'; simpl in H; subst l3. rewrite app_ass in P; rewrite <- app_comm_cons in P; rewrite <- permut0_cons_inside in P; trivial. rewrite <- app_ass in P; destruct (IHl1 l2 (l3' ++ l3'') l4 P) as [u1 [u2 [u3 [u4 [P1 [P2 [P3 P4]]]]]]]. exists (a1 :: u1); exists u2; exists u3; exists u4; repeat split; simpl; trivial. rewrite <- permut0_cons; trivial; reflexivity. apply (permut0_sym eq_proof). rewrite <- permut0_cons_inside; auto. apply (permut0_sym eq_proof). assumption. generalize (mem_split_set _ _ eq_bool_ok _ _ a1_in_l4). intros [a1' [l4' [l4'' [a1_eq_a1' [H _]]]]]; simpl in a1_eq_a1'; simpl in H; subst l4. rewrite <- app_ass in P; rewrite <- permut0_cons_inside in P; trivial. rewrite app_ass in P; destruct (IHl1 l2 l3 (l4' ++ l4'') P) as [u1 [u2 [u3 [u4 [P1 [P2 [P3 P4]]]]]]]; exists u1; exists (a1 :: u2); exists u3; exists u4; intuition; simpl; trivial. rewrite <- permut0_cons_inside; trivial. reflexivity. apply permut0_sym; [constructor;auto with typeclass_instances|]. rewrite <- permut0_cons_inside; trivial. apply permut0_sym; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)