# Library list_extensions.list_permut

``` Add LoadPath "basis". ```

# Permutation over lists, and finite multisets.

``` Set Implicit Arguments. Require Import decidable_set. Require Import List. Require Import more_list. Require Import equiv_list. Require Import Relations. Require Import Arith. Require Import Setoid. Inductive permut (A B : Set) (R : A -> B -> Prop) : (list A -> list B -> Prop) :=   | Pnil : permut R nil nil   | Pcons : forall a b l l1 l2, R a b -> permut R l (l1 ++ l2) ->                    permut R (a :: l) (l1 ++ b :: l2). Lemma permut_nil :   forall (A B : Set) (R : A -> B -> Prop) l, permut R l nil -> l = nil. Proof. intros A B R l P; inversion P as [ | a b l' l1 l2 a_R_b P']; trivial. destruct l1; discriminate. Qed. Lemma permut_impl :   forall (A B : Set) (R R' : A -> B -> Prop) l1 l2,   (forall a b, R a b -> R' a b) -> permut R l1 l2 -> permut R' l1 l2. Proof. intros A B R R' l1; induction l1 as [ | a1 l1]; intros l2 Compat P; inversion P as [ | a b k k1 k2 a_R_b Q]; subst. apply Pnil. apply Pcons. apply Compat; trivial. apply IHl1; trivial. Qed. Lemma permut_strong :   forall (A B : Set) (R : A -> B -> Prop) a1 a2 l1 k1 l2 k2,   R a1 a2 -> permut R (l1 ++ k1) (l2 ++ k2) ->   permut R (l1 ++ a1 :: k1) (l2 ++ a2 :: k2). Proof. intros A B R a1 a2 l1; induction l1 as [ | u1 l1]; intros k1 l2 k2 a1_R_a2 P. apply (@Pcons _ _ R a1 a2 k1 l2 k2); trivial. inversion P as [ | b1 b2 l k k' b1_R_b2 Q]; clear P; subst. destruct (split_list _ _ _ _ H) as [H' | H']; clear H. destruct H' as [l [H1 H2]]; subst; simpl. assert (Q' := @Pcons _ _ R u1 b2 (l1 ++ a1 :: k1) (l2 ++ a2 :: l) k' b1_R_b2). do 2 rewrite <- ass_app in Q'; simpl in Q'; apply Q'. apply IHl1; trivial. rewrite ass_app; trivial. destruct H' as [l [H1 H2]]; subst; simpl. destruct l as [ | u l]. simpl in H2; subst k2; rewrite <- app_nil_end. assert (Q' := @Pcons _ _ R u1 b2 (l1 ++ a1 :: k1) (k ++ a2 :: nil) k' b1_R_b2). do 2 rewrite <- ass_app in Q'; simpl in Q'; apply Q'. apply IHl1; trivial. simpl in H2; injection H2; clear H2; intros H2 b2_eq_u; subst u k'. assert (Q' := @Pcons _ _ R u1 b2 (l1 ++ a1 :: k1) k (l ++ a2 :: k2) b1_R_b2). rewrite <- ass_app; simpl; apply Q'. rewrite ass_app; apply IHl1; trivial. rewrite <- ass_app; trivial. Qed. Lemma permut_inv_left_strong :   forall (A B : Set) (R : A -> B -> Prop) a l1' l1'' l2,   permut R (l1' ++ a :: l1'') l2 -> exists b, exists l2', exists l2'',    (R a b /\ l2 = l2' ++ b :: l2'' /\ permut R (l1' ++ l1'') (l2' ++ l2'')). Proof. intros A B R a l1'; generalize a; clear a; induction l1' as [ | a1 l1']; intros a l1'' l2 P. inversion P as [ | a' b l' l2' l2'' a_R_b Q H]; clear P; subst. exists b; exists l2'; exists l2''; repeat split; trivial. inversion P as [ | a1' b l' l2' l2'' a1_R_b Q H]; clear P; subst. destruct (IHl1' _ _ _ Q) as [b' [k2' [k2'' [a_R_b' [H Q']]]]]; clear Q. destruct (split_list _ _ _ _ H) as [H' | H']; clear H. destruct H' as [[ | b'' l] [H1 H2]]; simpl in *; subst. exists b'; exists (k2' ++ b :: nil); exists k2''; repeat split; trivial. rewrite <- app_nil_end; rewrite <- ass_app; simpl; trivial. rewrite <- ass_app; simpl; apply Pcons; trivial. injection H2; clear H2; intros; subst. exists b''; exists k2'; exists (l ++ b :: l2''); repeat split; trivial. rewrite <- ass_app; simpl; trivial. rewrite ass_app; apply Pcons; trivial; rewrite <- ass_app; trivial. destruct H' as [l [H1 H2]]; subst. exists b'; exists (l2' ++ b :: l); exists k2''; repeat split; trivial. rewrite <- ass_app; simpl; trivial. rewrite <- ass_app. do 2 rewrite <- app_comm_cons; apply Pcons; trivial; rewrite ass_app; trivial. Qed. Lemma permut_inv_right :   forall (A : Set) (R : relation A) b l1 l2,   permut R l1 (b :: l2) -> exists a, exists l1', exists l1'',    (R a b /\ l1 = l1' ++ a :: l1'' /\ permut R (l1' ++ l1'') l2). Proof. intros A R b l1; generalize b; clear b; induction l1 as [ | a1 l1]; intros b l2 P; inversion P as [ | a b' l' l1' l2' a_R_b' Q H]; subst. destruct l1' as [ | a1' l1']; injection H2; clear H2; intros; subst. exists a1; exists (@nil A); exists l1; repeat split; trivial. simpl in Q; destruct (IHl1 _ _ Q) as [a [k1' [k1'' [a_R_b [H Q']]]]]; subst. exists a; exists (a1 :: k1'); exists k1''; repeat split; trivial. simpl; apply (@Pcons _ _ R a1 b' (k1' ++ k1'') l1' l2'); trivial. Qed. Lemma permut_inv_right_strong :   forall (A B : Set) (R : A -> B -> Prop) b l1 l2' l2'',   permut R l1 (l2' ++ b :: l2'') -> exists a, exists l1', exists l1'',    (R a b /\ l1 = l1' ++ a :: l1'' /\ permut R (l1' ++ l1'') (l2' ++ l2'')). Proof. intros A B R b l1; generalize b; clear b; induction l1 as [ | a1 l1]; intros b l2' l2'' P; inversion P as [ | a b' l' l1' k2 a_R_b' Q H]; subst. destruct l2'; discriminate. destruct (in_in_split_set _ _ _ _ _ _ H2) as [[H2' | H2'] | H2']; clear H2. destruct H2' as [l [H2 H3]]; subst. rewrite <- ass_app in Q; simpl in Q; destruct (IHl1 b _ _ Q) as [a [l1' [l1'' [a_R_b [H Q']]]]]; subst. exists a; exists (a1 :: l1'); exists l1''; repeat split; trivial. simpl; rewrite ass_app; apply Pcons; trivial. rewrite <- ass_app; trivial. destruct H2' as [l [H2 H3]]; subst. rewrite ass_app in Q. destruct (IHl1 b _ _ Q) as [a [k1' [k1'' [a_R_b [H Q']]]]]; subst. exists a; exists (a1 :: k1'); exists k1''; repeat split; trivial. rewrite <- ass_app; simpl; apply Pcons; trivial. rewrite ass_app; trivial. destruct H2' as [b'_eq_b [H2 H3]]; subst. exists a1; exists (@nil A); exists l1; repeat split; trivial. Qed. Lemma permut_rev :   forall (A B : Set) (R : A -> B -> Prop) l1 l2, permut R l1 l2 ->   permut (fun b a => R a b) l2 l1. Proof. intros A B R l1; induction l1 as [ | a1 l1]; intros l2 P; inversion P as [ | a b l1' l2' l2'' a_R_b Q]; subst. apply Pnil. apply (@permut_strong B A (fun b a => R a b) b a1 l2' l2'' (@nil _) l1); trivial. simpl; apply IHl1; trivial. Qed. ```
Permutation is compatible with length.
``` Lemma permut_length :   forall (A : Set) (R : relation A) l1 l2, permut R l1 l2 -> length l1 = length l2. Proof. intros A R l; induction l as [ | a l]; intros l' P; inversion P; trivial. subst. rewrite length_app; simpl; rewrite plus_comm; simpl; rewrite plus_comm. rewrite <- length_app; rewrite (IHl (l1 ++ l2)); trivial. Qed. Lemma permut_refl :    forall (A : Set) (R : relation A) l,   (forall a, In a l -> R a a) -> permut R l l. Proof. intros A R l refl_R; induction l as [ | a l]. apply Pnil. apply (@Pcons _ _ R a a l nil l). apply refl_R; left; trivial. simpl; apply IHl; intros; apply refl_R; right; trivial. Qed. Lemma permut_sym :   forall (A : Set) (R : relation A) l1 l2,    (forall a b, In a l1 -> In b l2 -> R a b -> R b a) ->    permut R l1 l2 -> permut R l2 l1. Proof. intros A R l1; induction l1 as [ | a1 l1]; intros l2 sym_R P; inversion P as [ | a b l1' l2' l2'' a_R_b Q]; subst. apply Pnil. apply (permut_strong (R := R) b a1 l2' l2'' (@nil A) l1). apply sym_R; trivial; [left | apply in_or_app; right; left]; trivial. simpl; apply IHl1; trivial. intros; apply sym_R; trivial; [right | apply in_insert]; trivial. Qed. Lemma permut_trans :   forall (A : Set) (R : relation A) l1 l2 l3,    (forall a b c, In a l1 -> In b l2 -> In c l3 -> R a b -> R b c -> R a c) ->    permut R l1 l2 -> permut R l2 l3 -> permut R l1 l3. Proof. intros A R l1 l2; generalize l1; clear l1; induction l2 as [ | a2 l2]; intros l1 l3 trans_R P1 P2. inversion_clear P2; trivial. destruct (permut_inv_right P1) as [a1 [l1' [l1'' [a1_R_a2 [H Q1]]]]]; subst l1. inversion P2 as [ | a2' a3 l2' l3' l3'' a2_R_a3 Q2]; subst. apply permut_strong. apply trans_R with a2; trivial. apply in_or_app; right; left; trivial. left; trivial. apply in_or_app; right; left; trivial. apply IHl2; trivial. intros a b c; intros; apply trans_R with b; trivial. apply in_insert; trivial. right; trivial. apply in_insert; trivial. Qed. Lemma permut_cons_inside :   forall (A B : Set) (R : A -> B -> Prop) a b l l1 l2,   (forall a1 b1 a2 b2, In a1 (a :: l) -> In b1 (l1 ++ b :: l2) ->                    In a2 (a :: l) -> In b2 (l1 ++ b :: l2) ->                    R a1 b1 -> R a2 b1 -> R a2 b2 -> R a1 b2) ->   R a b -> permut R (a :: l) (l1 ++ b :: l2) -> permut R l (l1 ++ l2). Proof. intros A B R a b l l1 l2 trans_R a_R_b P; destruct (permut_inv_right_strong (R := R) _ _ _ P) as [a' [l1' [l1'' [a'_R_b [H P']]]]]. destruct l1' as [ | a1' l1']; injection H; clear H; intros; subst; trivial. inversion P' as [ | a'' b' l' k1' k2' a''_R_b' P'']; subst. apply permut_strong; trivial. apply trans_R with b a1'; trivial. right; apply in_or_app; right; left; trivial. apply in_or_app; right; left; trivial. left; trivial. apply in_insert; rewrite <- H; apply in_or_app; right; left; trivial. Qed. Lemma permut_add_inside :    forall (A B : Set) (R : A -> B -> Prop) a b l1 l1' l2 l2',   (forall a1 b1 a2 b2, In a1 (l1 ++ a :: l1') -> In b1 (l2 ++ b :: l2') ->                    In a2 (l1 ++ a :: l1') -> In b2 (l2 ++ b :: l2') ->                    R a1 b1 -> R a2 b1 -> R a2 b2 -> R a1 b2) ->   R a b -> permut R (l1 ++ a :: l1') (l2 ++ b :: l2') -> permut R (l1 ++ l1') (l2 ++ l2'). Proof. intros A B R a b l1 l1' l2 l2' trans_R a_R_b P. destruct (permut_inv_left_strong (R := R) _ _ _ P) as [b' [k2 [k2' [a_R_b' [H P']]]]]. destruct (in_in_split_set _ _ _ _ _ _ H) as [[H' | H'] | H']; clear H. destruct H' as [l [H1 H2]]; subst. rewrite ass_app in P'. destruct (permut_inv_right_strong (R := R) _ _ _ P') as [a' [k1' [k1'' [a'_R_b' [H P'']]]]]. rewrite H; rewrite <- ass_app; simpl; apply permut_strong. apply trans_R with b a; trivial. apply in_insert; rewrite H; apply in_or_app; right; left; trivial. apply in_or_app; right; left; trivial. apply in_or_app; right; left; trivial. apply in_or_app; left; apply in_or_app; right; left; trivial. rewrite ass_app; trivial. destruct H' as [l [H1 H2]]; subst. rewrite <- ass_app in P'; simpl in P'. destruct (permut_inv_right_strong (R := R) _ _ _ P') as [a' [k1' [k1'' [a'_R_b' [H P'']]]]]. rewrite H; rewrite ass_app; simpl; apply permut_strong. apply trans_R with b a; trivial. apply in_insert; rewrite H; apply in_or_app; right; left; trivial. apply in_or_app; right; left; trivial. apply in_or_app; right; left; trivial. apply in_or_app; right; right; apply in_or_app; right; left; trivial. rewrite <- ass_app; trivial. destruct H' as [H1 [H2 H3]]; subst; trivial. Qed. Lemma exists_dec :   forall (A : Set) (P : A -> Prop) (l : list A),   (forall a, In a l -> {P a}+{~P a}) ->   {a | In a l /\ P a}+{~exists a, In a l /\ P a}. Proof. intros A P l P_dec; induction l as [ | a l]. right; intros [a [a_in_nil _]]; absurd (In a nil); auto. destruct (P_dec a) as [Pa | not_Pa]. left; trivial. left; exists a; split; trivial; left; trivial. destruct IHl as [Ok | Ko]. intros; apply P_dec; right; trivial. destruct Ok as [b [b_in_l P_b]]. left; exists b; split; trivial; right; trivial. right; intros [b [[b_eq_a | b_in_l] Pb]]. subst; apply not_Pa; trivial. apply Ko; exists b; split; trivial. Defined. Fixpoint split_all (A : Set) (l : list A) : list (A * (list A * list A)) :=   match l with   | nil => @nil _   | a :: l =>     (a,(@nil _, l)) ::     (map (fun bl' => match bl' with (b,(l',l'')) => (b, (a :: l',l'')) end) (split_all l))     end. Lemma split_all_is_sound :   forall (A : Set) (l : list A) b l' l'', In (b,(l',l'')) (split_all l) <-> l = l' ++ b :: l''. Proof. intros A l; induction l as [ | a l]; intros b l' l''. split; intro H. contradiction. destruct l'; discriminate. simpl; split; intro H. setoid_rewrite in_map_iff in H; destruct H as [ H | H ]. injection H; intros; subst; trivial. destruct H as [[c [k' k'']] [H H']]. injection H; intros; subst. simpl; apply (f_equal (fun l => a :: l)). setoid_rewrite <- (IHl b k' l''); trivial. setoid_rewrite in_map_iff; destruct l' as [ | a' l']; simpl in H; injection H; intros; subst. left; trivial. right; exists (b,(l',l'')); split; trivial. setoid_rewrite (IHl b l' l''); trivial. Qed. Lemma permut_dec :   forall (A B : Set) (R : A -> B -> Prop),           forall l1 l2, (forall a1 a2, In a1 l1 -> In a2 l2 -> {R a1 a2}+{~R a1 a2}) ->          {permut R l1 l2}+{~permut R l1 l2}. Proof. intros A B R l1; induction l1 as [ | a1 l1]; intros l2 R_dec. destruct l2 as [ | a2 l2]. left; apply Pnil. right; intro P; inversion P. assert (P_dec : forall a : B * (list B * list B),   In a (split_all l2) ->   {(fun bll' : B * (list B * list B) =>     let (b, y) := bll' in let (l, l') := y in R a1 b /\ permut R l1 (l ++ l'))      a} +   {~    (fun bll' : B * (list B * list B) =>     let (b, y) := bll' in let (l, l') := y in R a1 b /\ permut R l1 (l ++ l'))      a}). intros [b [l l']] H; setoid_rewrite split_all_is_sound in H. destruct (R_dec a1 b) as [a1_R_b | not_a1_R_b]. left; trivial. subst l2; apply in_or_app; right; left; trivial. destruct (IHl1 (l ++ l')) as [P | not_P]. intros; apply R_dec. right; trivial. subst l2; apply in_insert; trivial. left; split; trivial. right; intros [_ P]; apply not_P; trivial. right; intros [a1_R_b _]; apply not_a1_R_b; trivial. assert (H := list_exists_rest_is_sound                        (fun bll' =>                            match bll' with                            | (b,(l,l')) => R a1 b /\ permut R l1 (l ++ l')                            end) (split_all l2) P_dec). destruct (list_exists_rest       (fun bll' : B * (list B * list B) =>        let (b, y) := bll' in        let (l, l') := y in R a1 b /\ permut R l1 (l ++ l')) (split_all l2) P_dec). left. destruct ((proj1 H) (refl_equal _)) as [[b [l l']] [H' [a1_R_b P]]]. setoid_rewrite split_all_is_sound in H'; subst l2; apply Pcons; trivial. right; intro P; inversion P; subst. assert (false = true). setoid_rewrite H; exists (b,(l0,l3)); split; trivial. setoid_rewrite split_all_is_sound; trivial. split; trivial. discriminate. Defined. Lemma permut_map :   forall (A B A' B': Set) (R : A -> B -> Prop) (R' : A' -> B' -> Prop) (f1 : A -> A') (f2 : B -> B')   l1 l2, (forall a b, In a l1 -> In b l2 -> R a b -> R' (f1 a) (f2 b)) ->   permut R l1 l2 -> permut R' (map f1 l1) (map f2 l2). Proof. intros A B A' B' R R' f1 f2 l1; induction l1 as [ | a1 l1]; intros l2 Compat P; inversion P as [ | a' b l1' l2' l2'' a_R_b P' H]; subst. simpl; apply Pnil. rewrite map_app; simpl; apply Pcons. apply Compat; trivial. left; trivial. apply in_or_app; right; left; trivial. rewrite <- map_app; apply IHl1; trivial. intros a b' a_in_l1 b'_in_l2; apply Compat. right; trivial. apply in_insert; trivial. Qed. Lemma permut_length_1:   forall (A B : Set) (R : A -> B -> Prop) a b, permut R (a :: nil) (b :: nil) -> R a b. Proof. intros A B R a b P; inversion P as [ | a' b' l' l1' l2' a_R_b' P' H1 H']; subst. destruct l1' as [ | a1' [ | b1' l1']]. injection H'; intros; subst; trivial. discriminate. discriminate. Qed. Lemma permut_length_2 :  forall (A B : Set) (R : A -> B -> Prop) a1 b1 a2 b2,     permut R (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->     (R a1 a2 /\ R b1 b2) \/ (R a1 b2 /\ R b1 a2). Proof. intros A B R a1 b1 a2 b2 P; inversion P as [ | a b l l1 l2 a_R_b P' H1 H']; subst. destruct l1 as [ | c1 l1]. destruct l2 as [ | c2 [ | d2 l2]]. discriminate. injection H'; intros; subst. left; split; trivial. apply (permut_length_1 P'). discriminate. destruct l1 as [ | d1 l1]. destruct l2 as [ | c2 l2]. injection H'; intros; subst. right; split; trivial. apply (permut_length_1 P'). discriminate. destruct l1; discriminate. Qed. Lemma permut_size :   forall (A B : Set) (R : A -> B -> Prop) size size' l1 l2,   (forall a a', In a l1 -> In a' l2 -> R a a' -> size a = size' a') ->   permut R l1 l2 -> list_size size l1 = list_size size' l2. Proof. intros A B R size size' l1; induction l1 as [ | a1 l1 ]; intros l2 E P; inversion P as [ | a b l1' l2' l2'' a_R_b P']; subst; trivial. rewrite list_size_app; simpl. rewrite (E a1 b); trivial. rewrite (IHl1 (l2' ++ l2'')); trivial. rewrite list_size_app; simpl. rewrite plus_comm. rewrite <- plus_assoc. apply (f_equal (fun n => list_size size' l2' + n)). apply plus_comm. intros a a' a_in_la a_in_l'; apply E; trivial. right; trivial. apply in_insert; trivial. left; trivial. apply in_or_app; right; left; trivial. Qed. Lemma in_permut_in :    forall (A : Set) l1 l2, permut (@eq A) l1 l2 -> (forall a, In a l1 <-> In a l2). Proof. assert (H : forall (A : Set) l1 l2, permut (@eq A) l1 l2 -> forall a, In a l2 -> In a l1). intros A l1 l2 P a a_in_l2; destruct (In_split _ _ a_in_l2) as [l2' [l2'' H]]; subst. destruct (permut_inv_right_strong (R := @eq A) _ _ _ P)   as [a' [l1' [l1'' [a_eq_a' [H _]]]]]; subst. apply in_or_app; right; left; trivial. intros A l1 l2 P a; split; apply H; trivial. apply permut_sym; trivial; intros; subst; trivial. Qed. ```
Permutation is compatible with append.
``` Lemma permut_app :   forall (A B : Set) (R : A -> B -> Prop) l1 l1' l2 l2',    permut R l1 l2 -> permut R l1' l2' -> permut R (l1 ++ l1') (l2 ++ l2'). Proof. intros A B R l1; induction l1 as [ | a1 l1]; intros l1' l2 l2' P P'. inversion_clear P; trivial. inversion P as [ | a b l1'' l2'' l2''' a_R_b Q]; subst. simpl; rewrite <- ass_app; simpl; apply Pcons; trivial. rewrite ass_app; apply IHl1; trivial. Qed. Lemma permut_swapp :   forall (A B : Set) (R : A -> B -> Prop) l1 l1' l2 l2',    permut R l1 l2 -> permut R l1' l2' -> permut R (l1 ++ l1') (l2' ++ l2). Proof. intros A B R l1; induction l1 as [ | a1 l1]; intros l1' l2 l2' P P'. inversion_clear P; rewrite <- app_nil_end; trivial. inversion P as [ | a b l1'' l2'' l2''' a_R_b Q]; subst. simpl; rewrite ass_app; apply Pcons; trivial. rewrite <- ass_app; apply IHl1; trivial. Qed. Lemma permut_app1 :   forall (A : Set) (R : relation A), equivalence _ R ->   forall l l1 l2, permut R l1 l2 <-> permut R (l ++ l1) (l ++ l2). Proof. intros A R E l l1 l2; split; intro P. induction l as [ | u l]; trivial. simpl; apply (@Pcons _ _ R u u (l ++ l1) (@nil A) (l ++ l2)); trivial. apply (equiv_refl _ _ E). induction l as [ | u l]; trivial. apply IHl. apply (@permut_cons_inside A A R u u (l ++ l1) (@nil _) (l ++ l2)); trivial. intros a1 b1 a2 b2 _ _ _ _ a1_R_b1 a2_R_b1 a2_R_b2; apply (equiv_trans _ _ E) with b1; trivial. apply (equiv_trans _ _ E) with a2; trivial. apply (equiv_sym _ _ E); trivial. apply (equiv_refl _ _ E). Qed. Lemma permut_app2 :   forall (A : Set) (R : relation A), equivalence _ R ->   forall l l1 l2, permut R l1 l2 <-> permut R (l1 ++ l) (l2 ++ l). Proof. intros A R E l l1 l2; split; intro P. induction l as [ | u l]. do 2 rewrite <- app_nil_end; trivial. apply permut_strong; trivial. apply (equiv_refl _ _ E). induction l as [ | u l]. do 2 rewrite <- app_nil_end in P; trivial. apply IHl. apply (@permut_add_inside A A R u u); trivial. intros a1 b1 a2 b2 _ _ _ _ a1_R_b1 a2_R_b1 a2_R_b2; apply (equiv_trans _ _ E) with b1; trivial. apply (equiv_trans _ _ E) with a2; trivial. apply (equiv_sym _ _ E); trivial. apply (equiv_refl _ _ E). Qed. Lemma permut_list_exists :   forall (A B : Set) (R : A -> B -> Prop) f f', (forall t t', R t t' -> f t = f' t') ->   forall l l', permut R l l' -> list_exists f l = list_exists f' l'. Proof. intros A B R f f' E l; induction l as [ | a l]; simpl; intros l' P; inversion P as [ | a' b l1 l2' l2'' a_R_b Q]; subst; simpl; trivial. rewrite list_exists_app; simpl. rewrite (E _ _ a_R_b). destruct (f' b); simpl. destruct (list_exists f' l2'); simpl; trivial. rewrite <- list_exists_app; apply IHl; trivial. Qed. Lemma permut_list_forall_exists :   forall (A B A' B': Set) (R : A -> B -> Prop) (R' : A' -> B' -> Prop) f f',   (forall ta ta' tb tb', R ta tb -> R' ta' tb' -> f ta ta' = f' tb tb') ->   forall la la' lb lb', permut R la lb -> permut R' la' lb' ->   list_forall (fun t1 => list_exists (fun t2 => f t1 t2) la') la =   list_forall (fun t1 => list_exists (fun t2 => f' t1 t2) lb') lb. Proof. intros A B A' B' R R' f f' E la; induction la as [ | a la]; intros la' lb lb' P P'; inversion P as [ | a' b k1 k2' k2'' a_R_b Q]; subst; simpl; trivial. rewrite list_forall_app; simpl. rewrite (IHla la' (k2' ++ k2'') lb' Q P'). rewrite list_forall_app; simpl. assert (E' : forall (t : A') (t' : B'), R' t t' -> f a t = f' b t'). intros; apply E; trivial. rewrite (@permut_list_exists _ _ R' (fun t2 : A' => f a t2) (fun t2 : B' => f' b t2) E' _ _ P'). destruct (list_exists (fun t2 : B' => f' b t2) lb'); simpl; trivial. destruct (list_forall (fun t1 : B => list_exists (fun t2 : B' => f' t1 t2) lb') k2'); simpl; trivial. Qed. Module Type S.   Declare Module Import EDS : decidable_set.ES.   Notation permut := (permut eq_A). Fixpoint mem (e : A) (l : list A) {struct l} : Prop :=    match l with    | nil => False    | e' :: l => (eq_A e e') \/ mem e l    end.  Axiom permut_refl :     forall (l : list A), permut l l.  Axiom permut_sym :     forall l1 l2 : list A, permut l1 l2 -> permut l2 l1.   Axiom permut_trans :     forall l1 l2 l3 : list A, permut l1 l2 -> permut l2 l3 -> permut l1 l3.   Hint Immediate permut_refl.   Hint Resolve permut_sym. Function remove_equiv (l1 l2 : list A) {struct l1} : (list A) * (list A) :=   match l1 with     | nil => (l1, l2)     | x1 :: l1' =>         match remove _ eq_dec x1 l2 with         | Some l2' => remove_equiv l1' l2'         | None =>               match remove_equiv l1' l2 with               | (l1'', l2'') => ((x1 :: l1'') , l2'')               end           end      end. Axiom in_impl_mem : forall e l, In e l -> mem e l. Axiom mem_dec : forall a l, {mem a l}+{~ mem a l}. Axiom mem_split_set :    forall a l, mem a l -> {a' : A & {l' : list A & {l'' | eq_A a a' /\ l = l' ++ a' :: l''}}}. Axiom mem_or_app :   forall l m a, mem a l \/ mem a m <-> mem a (l ++ m). Axiom mem_insert :   forall l1 l2 e a, mem a (l1 ++ l2) -> mem a (l1 ++ e :: l2). Axiom diff_mem_remove :   forall l1 l2 e a, ~eq_A a e -> mem a (l1 ++ e :: l2) -> mem a (l1 ++ l2).  Axiom mem_permut_mem :     forall l1 l2 e, permut l1 l2 -> (mem e l1 <-> mem e l2).    Axiom cons_permut_mem :     forall l1 l2 e1 e2, eq_A e1 e2 -> permut (e1 :: l1) l2 -> mem e2 l2.   Axiom permut_cons :     forall e1 e2 l1 l2, eq_A e1 e2 ->       (permut l1 l2 <-> permut (e1 :: l1) (e2 :: l2)).    Axiom permut_add_inside :     forall e1 e2 l1 l2 l3 l4, eq_A e1 e2 ->       (permut (l1 ++ l2) (l3 ++ l4) <->       permut (l1 ++ e1 :: l2) (l3 ++ e2 :: l4)).   Axiom permut_cons_inside :     forall e1 e2 l l1 l2, eq_A e1 e2 ->       (permut l (l1 ++ l2) <-> permut (e1 :: l) (l1 ++ e2 :: l2)).  Axiom permut_app1 :   forall l l1 l2, permut l1 l2 <-> permut (l ++ l1) (l ++ l2). Axiom permut_app2 :   forall l l1 l2, permut l1 l2 <-> permut (l1 ++ l) (l2 ++ l).  Axiom list_permut_app_app :  forall l1 l2, permut (l1 ++ l2) (l2 ++ l1).  Axiom ac_syntactic :  forall (l1 l2 l3 l4 : list A),  permut (l2 ++ l1) (l4 ++ l3) ->  (exists u1, exists u2, exists u3, exists u4,  permut l1 (u1 ++ u2) /\  permut l2 (u3 ++ u4) /\  permut l3 (u1 ++ u3) /\  permut l4 (u2 ++ u4)).  Axiom permut_dec :   forall (l1 l2 : list A), {permut l1 l2}+{~permut l1 l2}. Axiom remove_is_sound :   forall x l, match remove _ eq_dec x l with                 | None => ~mem x l                 | Some l' => permut l (x :: l')                 end. Axiom remove_equiv_is_sound:   forall l1 l2, match remove_equiv l1 l2 with   | (l1', l2') => exists l, permut l1 (l ++ l1') /\ permut l2 (l ++ l2') /\                         (forall x, mem x l1' -> mem x l2' -> False)   end.   Add Relation (list A) permut   reflexivity proved by permut_refl     symmetry proved by permut_sym       transitivity proved by permut_trans as LP.    Add Morphism mem         with signature eq_A ==> permut ==> iff         as mem_morph.  Add Morphism (List.app (A:=A))         with signature permut ==> permut ==> permut         as app_morph.  Add Morphism (List.cons (A:=A))         with signature eq_A ==> permut ==> permut         as add_A_morph. End S. ```

## Definition of permutation over lists.

``` Module Make (EDS1 : decidable_set.ES) : S with Module EDS:= EDS1.   Module Import EDS <: decidable_set.ES := EDS1.   Notation permut := (permut eq_A). Fixpoint mem (e : A) (l : list A) {struct l} : Prop :=    match l with    | nil => False    | e' :: l => (eq_A e e') \/ mem e l    end. ```

## Permutation is a equivalence relation.

Reflexivity.
```   Theorem permut_refl :     forall (l : list A), permut l l.   Proof.   intro l; apply permut_refl.   intros a _; reflexivity.   Qed. ```
Symetry.
```   Theorem permut_sym :     forall l1 l2 : list A, permut l1 l2 -> permut l2 l1.   Proof.   intros l1 l2 P; apply permut_sym; trivial.   intros a b _ _ a_eq_b; symmetry; trivial.   Qed.   Hint Immediate permut_refl.   Hint Resolve permut_sym. ```
Transitivity.
```   Theorem permut_trans :     forall l1 l2 l3 : list A, permut l1 l2 -> permut l2 l3 -> permut l1 l3.   Proof.   intros l1 l2 l3 P1 P2; apply permut_trans with l2; trivial.   intros a b c _ _ _ a_eq_b b_eq_c; transitivity b; trivial.   Qed.   Add Relation (list A) permut   reflexivity proved by permut_refl     symmetry proved by permut_sym       transitivity proved by permut_trans as LP. Lemma in_impl_mem : forall e l, In e l -> mem e l. Proof. intros e l; induction l as [ | a l]. contradiction. intros [e_eq_a | e_in_l]. left; subst; reflexivity. right; apply IHl; trivial. Qed. Lemma mem_dec : forall a l, {mem a l}+{~ mem a l}. Proof. intros a l; induction l as [ | e l]; simpl. right; intro; trivial. destruct (eq_dec a e) as [a_eq_e | a_diff_e]. left; left; trivial. destruct IHl as [a_mem_l | a_not_mem_l]. left; right; trivial. right; intros [a_eq_e | a_mem_l]. apply a_diff_e; trivial. apply a_not_mem_l; trivial. Defined. Lemma mem_split_set :   forall a l, mem a l -> {a' : A & {l' : list A & {l'' | eq_A a a' /\ l = l' ++ a' :: l''}}}. Proof. intros a l; induction l as [ | e l]; intro a_mem_l. contradiction. destruct (eq_dec a e) as [a_eq_e | a_diff_e]. exists e; exists (@nil A); exists l; split; trivial. assert (a_mem_l' : mem a l). destruct a_mem_l as [a_eq_e | a_mem_l]; trivial. absurd (eq_A a e); trivial. destruct (IHl a_mem_l') as [e' [l' [l'' [a_eq_e' H]]]]; simpl in a_eq_e'; simpl in H; subst l. exists e'; exists (e :: l'); exists l''; split; trivial. Qed. Lemma mem_or_app :   forall l m a, mem a l \/ mem a m <-> mem a (l ++ m). Proof. intros l m a; split. induction l as [ | e l]; intros [a_mem_l | a_mem_m]. contradiction. simpl; trivial. destruct a_mem_l as [a_eq_e | a_mem_l]. simpl; left; trivial. simpl; right; apply IHl; left; trivial. simpl; right; apply IHl; right; trivial. induction l as [ | e l]; intro a_mem_lm. right; trivial. simpl in a_mem_lm; destruct a_mem_lm as [a_eq_e | a_mem_lm]. left; left; trivial. destruct (IHl a_mem_lm) as [a_mem_l | a_mem_m]. left; right; trivial. right; trivial. Qed. Lemma mem_insert :   forall l1 l2 e a, mem a (l1 ++ l2) -> mem a (l1 ++ e :: l2). Proof. intro l1; induction l1 as [ | e1 l1]; intros l2 e a a_mem_l1l2. simpl; right; trivial. simpl in a_mem_l1l2; destruct a_mem_l1l2 as [a_eq_e1 | a_mem_l1l2]. simpl; left; trivial. simpl; right; apply IHl1; trivial. Qed. Lemma diff_mem_remove :   forall l1 l2 e a, ~eq_A a e -> mem a (l1 ++ e :: l2) -> mem a (l1 ++ l2). Proof. intros l1; induction l1 as [ | e1 l1]; simpl; intros l2 e a a_diff_e a_in_l1el2. destruct a_in_l1el2 as [e_eq_a | a_mem_l2]; trivial. absurd (eq_A a e); trivial; symmetry; trivial. destruct a_in_l1el2 as [e1_eq_a | a_mem_l1el2]. left; trivial. right; apply (IHl1 l2 e); trivial. Qed. ```

## Compatibility Properties.

Permutation is compatible with mem.
```   Lemma mem_permut_mem :     forall l1 l2 e, permut l1 l2 -> (mem e l1 <-> mem e l2).   Proof.     assert (forall l1 l2 e, permut l1 l2 -> mem e l1 -> mem e l2).     intro l1; induction l1 as [ | a1 l1]; intros l2 e P e_mem_l1.     contradiction.     inversion P as [ | a' b l' l1' l2' a1_eq_b P' H1 H']; subst.     destruct e_mem_l1 as [e_eq_a1 | e_mem_l1].     setoid_rewrite <- mem_or_app.     right; left; transitivity a1; trivial.     apply mem_insert; apply IHl1; trivial.     intros l1 l2 e P; split; apply H; trivial.     apply permut_sym; trivial.   Qed.    Add Morphism mem         with signature eq_A ==> permut ==> iff         as mem_morph.    Proof.     intros e1 e2 e1_eq_e2 l1 l2 P.     setoid_rewrite (mem_permut_mem e1 P).     clear l1 P; assert (H : forall e1 e2, eq_A e1 e2 -> mem e1 l2 -> mem e2 l2).     clear e1 e2 e1_eq_e2; intros e1 e2 e1_eq_e2;     induction l2 as [ | a l]; simpl; trivial.     intros [e1_eq_a | e1_mem_l]; [left | right; trivial].     transitivity e1; trivial.     symmetry; trivial.     apply IHl; trivial.     split; apply H; trivial.     symmetry; trivial.   Qed.   Lemma cons_permut_mem :     forall l1 l2 e1 e2, eq_A e1 e2 -> permut (e1 :: l1) l2 -> mem e2 l2.   Proof.     intros l1 l2 e1 e2 e1_eq_e2 P; setoid_rewrite <- P; left; trivial.     symmetry; trivial.   Qed. ```
Permutation is compatible with addition and removal of common elements
```  Lemma permut_cons :     forall e1 e2 l1 l2, eq_A e1 e2 ->       (permut l1 l2 <-> permut (e1 :: l1) (e2 :: l2)).   Proof.     intros e1 e2 l1 l2 e1_eq_e2; split; intro P.     apply (@Pcons _ _ eq_A e1 e2 l1 (@nil A) l2); trivial.     replace l2 with (nil ++ l2); trivial;     apply permut_cons_inside with e1 e2; trivial.     intros a1 b1 a2 b2 _ _ _ _ a1_eq_b1 a2_eq_b1 a2_eq_b2;     transitivity a2; trivial.     transitivity b1; trivial.     symmetry; trivial.      Qed.   Add Morphism (List.cons (A:=A))         with signature eq_A ==> permut ==> permut         as add_A_morph.   Proof.     intros e1 e2 e1_eq_e2 l1 l2 P; setoid_rewrite <- (@permut_cons e1 e2 l1 l2); trivial.   Qed.   Lemma permut_add_inside :     forall e1 e2 l1 l2 l3 l4, eq_A e1 e2 ->       (permut (l1 ++ l2) (l3 ++ l4) <->       permut (l1 ++ e1 :: l2) (l3 ++ e2 :: l4)).   Proof.   intros e1 e2 l1 l2 l3 l4 e1_eq_e2; split; intro P.   apply permut_strong; trivial.   apply permut_add_inside with e1 e2; trivial.   intros a1 b1 a2 b2 _ _ _ _ a1_eq_b1 a2_eq_b1 a2_eq_b2;   transitivity a2; trivial.   transitivity b1; trivial.   symmetry; trivial.   Qed.   Lemma permut_cons_inside :     forall e1 e2 l l1 l2, eq_A e1 e2 ->       (permut l (l1 ++ l2) <-> permut (e1 :: l) (l1 ++ e2 :: l2)).   Proof.     intros e1 e2 l l1 l2 e1_eq_e2; apply (permut_add_inside nil l l1 l2 e1_eq_e2).   Qed. ```
Permutation is compatible with append.
``` Lemma permut_app1 :   forall l l1 l2, permut l1 l2 <-> permut (l ++ l1) (l ++ l2). Proof. intros l l1 l2; apply permut_app1. apply EDS.eq_proof. Qed. Lemma permut_app2 :   forall l l1 l2, permut l1 l2 <-> permut (l1 ++ l) (l2 ++ l). Proof. intros l l1 l2; apply permut_app2. apply EDS.eq_proof. Qed. Add Morphism (List.app (A:=A))         with signature permut ==> permut ==> permut         as app_morph. Proof. intros. apply permut_trans with (x1 ++ x3). setoid_rewrite <- permut_app1; trivial. setoid_rewrite <- permut_app2; trivial. Qed. Lemma list_permut_app_app :  forall l1 l2, permut (l1 ++ l2) (l2 ++ l1). Proof. intros l1 l2; apply permut_swapp; apply permut_refl. Qed. ```

## Link with AC syntactic decomposition.

``` Lemma ac_syntactic_aux :  forall (l1 l2 l3 l4 : list A),  permut (l1 ++ l2) (l3 ++ l4) ->  (exists u1, exists u2, exists u3, exists u4,  permut l1 (u1 ++ u2) /\  permut l2 (u3 ++ u4) /\  permut l3 (u1 ++ u3) /\  permut l4 (u2 ++ u4)). Proof. induction l1 as [ | a1 l1]; intros l2 l3 l4 P. exists (nil : list A); exists (nil : list A); exists l3; exists l4; simpl; intuition. simpl in P. assert (a1_in_l3l4 := cons_permut_mem (equiv_refl _ _ eq_proof a1) P). setoid_rewrite <- mem_or_app in a1_in_l3l4; destruct a1_in_l3l4 as [a1_in_l3 | a1_in_l4]. destruct (mem_split_set _ _ a1_in_l3) as [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; setoid_rewrite <- permut_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; intuition; simpl; trivial. setoid_rewrite <- P1; auto. apply permut_sym; setoid_rewrite <- permut_cons_inside; auto. destruct (mem_split_set _ _ a1_in_l4) as [a1' [l4' [l4'' [a1_eq_a1' H]]]]; simpl in a1_eq_a1'; simpl in H; subst l4. rewrite <- app_ass in P; setoid_rewrite <- permut_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. setoid_rewrite <- permut_cons_inside; trivial. reflexivity. apply permut_sym; setoid_rewrite <- permut_cons_inside; trivial; apply permut_sym; trivial. Qed. Lemma ac_syntactic :  forall (l1 l2 l3 l4 : list A),  permut (l2 ++ l1) (l4 ++ l3) ->  (exists u1, exists u2, exists u3, exists u4,  permut l1 (u1 ++ u2) /\  permut l2 (u3 ++ u4) /\  permut l3 (u1 ++ u3) /\  permut l4 (u2 ++ u4)). Proof. intros l1 l2 l3 l4 P; apply ac_syntactic_aux. apply permut_trans with (l2 ++ l1). apply list_permut_app_app. apply permut_trans with (l4 ++ l3); trivial. apply list_permut_app_app. Qed. Lemma permut_dec : forall (l1 l2 : list A), {permut l1 l2}+{~permut l1 l2}. Proof. intro l1; induction l1 as [ | a1 l1]; intro l2. destruct l2. left; apply Pnil. right; intro P; inversion P. destruct (mem_dec a1 l2) as [a1_in_l2 | a1_not_in_l2]. destruct (mem_split_set _ _ a1_in_l2) as [a2 [l2' [l2'' [a1_eq_a2 H]]]]; subst l2. destruct (IHl1 (l2' ++ l2'')) as [Ok | Ko]. left; apply Pcons; trivial. right; intro P; apply Ko. setoid_rewrite <- permut_cons_inside in P; trivial. right; intro P; apply a1_not_in_l2. apply cons_permut_mem with l1 a1; trivial. reflexivity. Defined. Lemma remove_is_sound :   forall x l, match remove _ eq_dec x l with                 | None => ~mem x l                 | Some l' => permut l (x :: l')                 end. Proof. intros x l; generalize (in_remove _ eq_dec x l); destruct (remove _ eq_dec x l) as [ k | ]. intros [x' [l' [l'' [x_eq_x' [H1 H2]]]]]; injection H2; intros; subst. symmetry; setoid_rewrite <- permut_cons_inside; auto. induction l as [ | e l]. intros _ F; contradiction. intros H [e_eq_x | x_mem_l]. apply (H e); trivial. left; trivial. apply IHl; trivial. intros a' x_eq_a' a'_in_l; apply (H a'); trivial; right; trivial. Qed. Function remove_equiv (l1 l2 : list A) {struct l1} : (list A) * (list A) :=   match l1 with     | nil => (l1, l2)     | x1 :: l1' =>         match remove _ eq_dec x1 l2 with         | Some l2' => remove_equiv l1' l2'         | None =>               match remove_equiv l1' l2 with               | (l1'', l2'') => ((x1 :: l1'') , l2'')               end           end      end. Lemma remove_equiv_is_sound:   forall l1 l2, match remove_equiv l1 l2 with   | (l1', l2') => exists l, permut l1 (l ++ l1') /\ permut l2 (l ++ l2') /\                         (forall x, mem x l1' -> mem x l2' -> False)   end. Proof. intros l1 l2; functional induction (remove_equiv l1 l2)     as [ (* Case 1 *) | (* Case 2 *) H1 l2 e1 l1 H2 l2' H H' | (* Case 3 *) H1 l2 e1 l1 H2 H H' l1'' l2'' H'']. exists (@nil A); simpl; intuition. destruct (remove_equiv l1 l2') as [l1'' l2'']; destruct H' as [l [P1 [P2 H']]]. exists (e1 :: l); simpl; split. setoid_rewrite P1; auto. split; trivial. setoid_rewrite <- P2; assert (H'' := remove_is_sound e1 l2); rewrite H in H''; trivial. destruct (remove_equiv l1 l2) as [l1' l2']; injection H''; clear H''; intros; subst l1'' l2''; destruct H' as [l [P1 [P2 H']]]; exists l; split. setoid_rewrite <- permut_cons_inside; trivial. reflexivity. split; trivial. intros x [x_eq_e1 | x_mem_l1'] x_mem_l2'. assert (H'' := remove_is_sound e1 l2); rewrite H in H''. absurd (mem e1 l2); trivial. setoid_rewrite <- x_eq_e1. setoid_rewrite P2. setoid_rewrite <- mem_or_app; right; trivial. apply (H' x); trivial. Qed. End Make. ```