PermutEq.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Omega.

Set Implicit Arguments.

This file is similar to PermutSetoid, except that the equality used here is Coq usual one instead of a setoid equality. In particular, we can then prove the equivalence between Permutation.Permutation and PermutSetoid.permutation.

Section Perm.

  Variable A : Type.
  Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}.

  Notation permutation := (permutation _ eq_dec).
  Notation list_contents := (list_contents _ eq_dec).

we can use multiplicity to define In and NoDup.

  Lemma multiplicity_In :
    forall l a, In a l <-> 0 < multiplicity (list_contents l) a.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (l : list A) (a : A),
In a l <-> 0 < multiplicity (list_contents l) a
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (l : list A) (a : A),
In a l <-> 0 < multiplicity (list_contents l) a
    intros; split; intro H.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l:list A
a:A
H:In a l
0 < multiplicity (list_contents l) a
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l:list A
a:A
H:0 < multiplicity (list_contents l) a
In a l
    eapply In_InA, multiplicity_InA in H; eauto with typeclass_instances.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l:list A
a:A
H:0 < multiplicity (list_contents l) a
In a l
    eapply multiplicity_InA, InA_alt in H as (y & -> & H); eauto with typeclass_instances.
  Qed.

  Lemma multiplicity_In_O :
    forall l a, ~ In a l -> multiplicity (list_contents l) a = 0.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (l : list A) (a : A),
~ In a l -> multiplicity (list_contents l) a = 0
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (l : list A) (a : A),
~ In a l -> multiplicity (list_contents l) a = 0
    intros l a; rewrite multiplicity_In;
      destruct (multiplicity (list_contents l) a); auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l:list A
a:A
n:nat
~ 0 < S n -> S n = 0
    destruct 1; auto with arith.
  Qed.

  Lemma multiplicity_In_S :
    forall l a, In a l -> multiplicity (list_contents l) a >= 1.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (l : list A) (a : A),
In a l -> multiplicity (list_contents l) a >= 1
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (l : list A) (a : A),
In a l -> multiplicity (list_contents l) a >= 1
    intros l a; rewrite multiplicity_In; auto.
  Qed.

  Lemma multiplicity_NoDup :
    forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l : list A,
NoDup l <->
(forall a : A, multiplicity (list_contents l) a <= 1)
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l : list A,
NoDup l <->
(forall a : A, multiplicity (list_contents l) a <= 1)
    induction l.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
NoDup nil <->
(forall a : A, multiplicity (list_contents nil) a <= 1)
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
NoDup (a :: l) <->
(forall a0 : A,
 multiplicity (list_contents (a :: l)) a0 <= 1)
    simpl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
NoDup nil <-> (A -> 0 <= 1)
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
NoDup (a :: l) <->
(forall a0 : A,
 multiplicity (list_contents (a :: l)) a0 <= 1)
    split; auto with arith.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
(A -> 0 <= 1) -> NoDup nil
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
NoDup (a :: l) <->
(forall a0 : A,
 multiplicity (list_contents (a :: l)) a0 <= 1)
    intros; apply NoDup_nil.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
NoDup (a :: l) <->
(forall a0 : A,
 multiplicity (list_contents (a :: l)) a0 <= 1)
    split; simpl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
NoDup (a :: l) ->
forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eq_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDup (a :: l)
    inversion_clear 1.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H0:~ In a l
H1:NoDup l
forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eq_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDup (a :: l)
    rewrite IHl in H1.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H0:~ In a l
H1:forall a0 : A,
multiplicity (list_contents l) a0 <= 1
forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eq_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDup (a :: l)
    intros; destruct (eq_dec a a0) as [H2|H2]; simpl; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a1 : A,
 multiplicity (list_contents l) a1 <= 1)
H0:~ In a l
H1:forall a1 : A,
multiplicity (list_contents l) a1 <= 1
a0:A
H2:a = a0
S (multiplicity (list_contents l) a0) <= 1
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eq_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDup (a :: l)
    subst a0.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H0:~ In a l
H1:forall a0 : A,
multiplicity (list_contents l) a0 <= 1
S (multiplicity (list_contents l) a) <= 1
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eq_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDup (a :: l)
    rewrite multiplicity_In_O; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eq_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDup (a :: l)
    intros; constructor.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
~ In a l
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDup l
    rewrite multiplicity_In.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
~ 0 < multiplicity (list_contents l) a
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDup l
    generalize (H a).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
(if eq_dec a a then 1 else 0) +
multiplicity (list_contents l) a <= 1 ->
~ 0 < multiplicity (list_contents l) a
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDup l
    destruct (eq_dec a a) as [H0|H0].A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
H0:a = a
1 + multiplicity (list_contents l) a <= 1 ->
~ 0 < multiplicity (list_contents l) a
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
H0:a <> a
0 + multiplicity (list_contents l) a <= 1 ->
~ 0 < multiplicity (list_contents l) a
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDup l
    destruct (multiplicity (list_contents l) a); auto with arith.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
H0:a = a
n:nat
1 + S n <= 1 -> ~ 0 < S n
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
H0:a <> a
0 + multiplicity (list_contents l) a <= 1 ->
~ 0 < multiplicity (list_contents l) a
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDup l
    simpl; inversion 1.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
H0:a = a
n:nat
H1:S (S n) <= 1
m:nat
H3:S (S n) <= 0
H2:m = 0
~ 0 < S n
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
H0:a <> a
0 + multiplicity (list_contents l) a <= 1 ->
~ 0 < multiplicity (list_contents l) a
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDup l
    inversion H3.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
H0:a <> a
0 + multiplicity (list_contents l) a <= 1 ->
~ 0 < multiplicity (list_contents l) a
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDup l
    destruct H0; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDup l
    rewrite IHl; intros.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a1 : A,
 multiplicity (list_contents l) a1 <= 1)
H:forall a1 : A,
(if eq_dec a a1 then 1 else 0) +
multiplicity (list_contents l) a1 <= 1
a0:A
multiplicity (list_contents l) a0 <= 1
    generalize (H a0); auto with arith.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:NoDup l <->
(forall a1 : A,
 multiplicity (list_contents l) a1 <= 1)
H:forall a1 : A,
(if eq_dec a a1 then 1 else 0) +
multiplicity (list_contents l) a1 <= 1
a0:A
(if eq_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1 ->
multiplicity (list_contents l) a0 <= 1
    destruct (eq_dec a a0); simpl; auto with arith.
  Qed.

  Lemma NoDup_permut :
    forall l l', NoDup l -> NoDup l' ->
      (forall x, In x l <-> In x l') -> permutation l l'.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l l' : list A,
NoDup l ->
NoDup l' ->
(forall x : A, In x l <-> In x l') -> permutation l l'
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l l' : list A,
NoDup l ->
NoDup l' ->
(forall x : A, In x l <-> In x l') -> permutation l l'
    intros.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
H:NoDup l
H0:NoDup l'
H1:forall x : A, In x l <-> In x l'
permutation l l'
    red; unfold meq; intros.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
H:NoDup l
H0:NoDup l'
H1:forall x : A, In x l <-> In x l'
a:A
multiplicity (list_contents l) a =
multiplicity (list_contents l') a
    rewrite multiplicity_NoDup in H, H0.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
H:forall a0 : A,
multiplicity (list_contents l) a0 <= 1
H0:forall a0 : A,
multiplicity (list_contents l') a0 <= 1
H1:forall x : A, In x l <-> In x l'
a:A
multiplicity (list_contents l) a =
multiplicity (list_contents l') a
    generalize (H a) (H0 a) (H1 a); clear H H0 H1.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
a:A
multiplicity (list_contents l) a <= 1 ->
multiplicity (list_contents l') a <= 1 ->
In a l <-> In a l' ->
multiplicity (list_contents l) a =
multiplicity (list_contents l') a
    do 2 rewrite multiplicity_In.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
a:A
multiplicity (list_contents l) a <= 1 ->
multiplicity (list_contents l') a <= 1 ->
0 < multiplicity (list_contents l) a <->
0 < multiplicity (list_contents l') a ->
multiplicity (list_contents l) a =
multiplicity (list_contents l') a
    destruct 3; omega.
  Qed.

Permutation is compatible with In.

  Lemma permut_In_In :
    forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (l1 l2 : list A) (e : A),
permutation l1 l2 -> In e l1 -> In e l2
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (l1 l2 : list A) (e : A),
permutation l1 l2 -> In e l1 -> In e l2
    unfold PermutSetoid.permutation, meq; intros l1 l2 e P IN.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l1, l2:list A
e:A
P:forall a : A,
multiplicity (list_contents l1) a =
multiplicity (list_contents l2) a
IN:In e l1
In e l2
    generalize (P e); clear P.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l1, l2:list A
e:A
IN:In e l1
multiplicity (list_contents l1) e =
multiplicity (list_contents l2) e -> In e l2
    destruct (In_dec eq_dec e l2) as [H|H]; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l1, l2:list A
e:A
IN:In e l1
H:~ In e l2
multiplicity (list_contents l1) e =
multiplicity (list_contents l2) e -> In e l2
    rewrite (multiplicity_In_O _ _ H).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l1, l2:list A
e:A
IN:In e l1
H:~ In e l2
multiplicity (list_contents l1) e = 0 -> In e l2
    intros.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l1, l2:list A
e:A
IN:In e l1
H:~ In e l2
H0:multiplicity (list_contents l1) e = 0
In e l2
    generalize (multiplicity_In_S _ _ IN).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l1, l2:list A
e:A
IN:In e l1
H:~ In e l2
H0:multiplicity (list_contents l1) e = 0
multiplicity (list_contents l1) e >= 1 -> In e l2
    rewrite H0.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l1, l2:list A
e:A
IN:In e l1
H:~ In e l2
H0:multiplicity (list_contents l1) e = 0
0 >= 1 -> In e l2
    inversion 1.
  Qed.

  Lemma permut_cons_In :
    forall l1 l2 e, permutation (e :: l1) l2 -> In e l2.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (l1 l2 : list A) (e : A),
permutation (e :: l1) l2 -> In e l2
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (l1 l2 : list A) (e : A),
permutation (e :: l1) l2 -> In e l2
    intros; eapply permut_In_In; eauto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l1, l2:list A
e:A
H:permutation (e :: l1) l2
In e (e :: l1)
    red; auto.
  Qed.

Permutation of an empty list.

  Lemma permut_nil :
    forall l, permutation l nil -> l = nil.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l : list A, permutation l nil -> l = nil
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l : list A, permutation l nil -> l = nil
    intro l; destruct l as [ | e l ]; trivial.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
e:A
l:list A
permutation (e :: l) nil -> e :: l = nil
    assert (In e (e::l)) by (red; auto).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
e:A
l:list A
H:In e (e :: l)
permutation (e :: l) nil -> e :: l = nil
    intro Abs; generalize (permut_In_In _ Abs H).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
e:A
l:list A
H:In e (e :: l)
Abs:permutation (e :: l) nil
In e nil -> e :: l = nil
    inversion 1.
  Qed.

When used with eq, this permutation notion is equivalent to the one defined in List.v.

  Lemma permutation_Permutation :
    forall l l', Permutation l l' <-> permutation l l'.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l l' : list A,
Permutation l l' <-> permutation l l'
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l l' : list A,
Permutation l l' <-> permutation l l'
    split.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
Permutation l l' -> permutation l l'
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
permutation l l' -> Permutation l l'
    induction 1.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
permutation nil nil
A:Type
eq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
x:A
l, l':list A
H:Permutation l l'
IHPermutation:permutation l l'
permutation (x :: l) (x :: l')
A:Type
eq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
x, y:A
l:list A
permutation (y :: x :: l) (x :: y :: l)
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:permutation l l'
IHPermutation2:permutation l' l''
permutation l l''
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
permutation l l' -> Permutation l l'
    apply permut_refl.A:Type
eq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
x:A
l, l':list A
H:Permutation l l'
IHPermutation:permutation l l'
permutation (x :: l) (x :: l')
A:Type
eq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
x, y:A
l:list A
permutation (y :: x :: l) (x :: y :: l)
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:permutation l l'
IHPermutation2:permutation l' l''
permutation l l''
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
permutation l l' -> Permutation l l'
    apply permut_cons; auto.A:Type
eq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
x, y:A
l:list A
permutation (y :: x :: l) (x :: y :: l)
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:permutation l l'
IHPermutation2:permutation l' l''
permutation l l''
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
permutation l l' -> Permutation l l'
    change (permutation (y::x::l) ((x::nil)++y::l)).A:Type
eq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
x, y:A
l:list A
permutation (y :: x :: l) ((x :: nil) ++ y :: l)
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:permutation l l'
IHPermutation2:permutation l' l''
permutation l l''
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
permutation l l' -> Permutation l l'
    apply permut_add_cons_inside; simpl; apply permut_refl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:permutation l l'
IHPermutation2:permutation l' l''
permutation l l''
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
permutation l l' -> Permutation l l'
    apply permut_trans with l'; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
permutation l l' -> Permutation l l'
    revert l'.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l:list A
forall l' : list A,
permutation l l' -> Permutation l l'
    induction l.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l' : list A,
permutation nil l' -> Permutation nil l'
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:forall l' : list A,
permutation l l' -> Permutation l l'
forall l' : list A,
permutation (a :: l) l' -> Permutation (a :: l) l'
    intros.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l':list A
H:permutation nil l'
Permutation nil l'
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:forall l' : list A,
permutation l l' -> Permutation l l'
forall l' : list A,
permutation (a :: l) l' -> Permutation (a :: l) l'
    rewrite (permut_nil (permut_sym H)).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l':list A
H:permutation nil l'
Permutation nil nil
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:forall l' : list A,
permutation l l' -> Permutation l l'
forall l' : list A,
permutation (a :: l) l' -> Permutation (a :: l) l'
    apply Permutation_refl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:forall l' : list A,
permutation l l' -> Permutation l l'
forall l' : list A,
permutation (a :: l) l' -> Permutation (a :: l) l'
    intros.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:forall l'0 : list A,
permutation l l'0 -> Permutation l l'0
l':list A
H:permutation (a :: l) l'
Permutation (a :: l) l'
    destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:forall l'0 : list A,
permutation l l'0 -> Permutation l l'0
l':list A
H:permutation (a :: l) l'
h2, t2:list A
H1:l' = h2 ++ a :: t2
Permutation (a :: l) l'
    subst l'.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:forall l' : list A,
permutation l l' -> Permutation l l'
h2, t2:list A
H:permutation (a :: l) (h2 ++ a :: t2)
Permutation (a :: l) (h2 ++ a :: t2)
    apply Permutation_cons_app.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:forall l' : list A,
permutation l l' -> Permutation l l'
h2, t2:list A
H:permutation (a :: l) (h2 ++ a :: t2)
Permutation l (h2 ++ t2)
    apply IHl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IHl:forall l' : list A,
permutation l l' -> Permutation l l'
h2, t2:list A
H:permutation (a :: l) (h2 ++ a :: t2)
permutation l (h2 ++ t2)
    apply permut_remove_hd with a; auto with typeclass_instances.
  Qed.

Permutation for short lists.

  Lemma permut_length_1:
    forall a b, permutation (a :: nil) (b :: nil)  -> a=b.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall a b : A,
permutation (a :: nil) (b :: nil) -> a = b
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall a b : A,
permutation (a :: nil) (b :: nil) -> a = b
    intros a b; unfold PermutSetoid.permutation, meq; intro P;
      generalize (P b); clear P; simpl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
(if eq_dec a b then 1 else 0) + 0 =
(if eq_dec b b then 1 else 0) + 0 -> a = b
    destruct (eq_dec b b) as [H|H]; [ | destruct H; auto].A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
H:b = b
(if eq_dec a b then 1 else 0) + 0 = 1 + 0 -> a = b
    destruct (eq_dec a b); simpl; auto; intros; discriminate.
  Qed.

  Lemma permut_length_2 :
    forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
      (a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall a1 b1 a2 b2 : A,
permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall a1 b1 a2 b2 : A,
permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    intros a1 b1 a2 b2 P.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    assert (H:=permut_cons_In P).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H:In a1 (a2 :: b2 :: nil)
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    inversion_clear H.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:a2 = a1
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:In a1 (b2 :: nil)
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    left; split; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:a2 = a1
b1 = b2
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:In a1 (b2 :: nil)
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    apply permut_length_1.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:a2 = a1
permutation (b1 :: nil) (b2 :: nil)
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:In a1 (b2 :: nil)
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    red; red; intros.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:a2 = a1
a:A
multiplicity (list_contents (b1 :: nil)) a =
multiplicity (list_contents (b2 :: nil)) a
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:In a1 (b2 :: nil)
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    generalize (P a); clear P; simpl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H0:a2 = a1
a:A
(if eq_dec a1 a then 1 else 0) +
((if eq_dec b1 a then 1 else 0) + 0) =
(if eq_dec a2 a then 1 else 0) +
((if eq_dec b2 a then 1 else 0) + 0) ->
(if eq_dec b1 a then 1 else 0) + 0 =
(if eq_dec b2 a then 1 else 0) + 0
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:In a1 (b2 :: nil)
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    destruct (eq_dec a1 a) as [H2|H2];
      destruct (eq_dec a2 a) as [H3|H3]; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H0:a2 = a1
a:A
H2:a1 = a
H3:a2 <> a
1 + ((if eq_dec b1 a then 1 else 0) + 0) =
0 + ((if eq_dec b2 a then 1 else 0) + 0) ->
(if eq_dec b1 a then 1 else 0) + 0 =
(if eq_dec b2 a then 1 else 0) + 0
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H0:a2 = a1
a:A
H2:a1 <> a
H3:a2 = a
0 + ((if eq_dec b1 a then 1 else 0) + 0) =
1 + ((if eq_dec b2 a then 1 else 0) + 0) ->
(if eq_dec b1 a then 1 else 0) + 0 =
(if eq_dec b2 a then 1 else 0) + 0
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:In a1 (b2 :: nil)
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    destruct H3; transitivity a1; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H0:a2 = a1
a:A
H2:a1 <> a
H3:a2 = a
0 + ((if eq_dec b1 a then 1 else 0) + 0) =
1 + ((if eq_dec b2 a then 1 else 0) + 0) ->
(if eq_dec b1 a then 1 else 0) + 0 =
(if eq_dec b2 a then 1 else 0) + 0
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:In a1 (b2 :: nil)
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    destruct H2; transitivity a2; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:In a1 (b2 :: nil)
a1 = a2 /\ b1 = b2 \/ a1 = b2 /\ a2 = b1
    right.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H0:In a1 (b2 :: nil)
a1 = b2 /\ a2 = b1
    inversion_clear H0; [|inversion H].A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H:b2 = a1
a1 = b2 /\ a2 = b1
    split; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H:b2 = a1
a2 = b1
    apply permut_length_1.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H:b2 = a1
permutation (a2 :: nil) (b1 :: nil)
    red; red; intros.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
P:permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil)
H:b2 = a1
a:A
multiplicity (list_contents (a2 :: nil)) a =
multiplicity (list_contents (b1 :: nil)) a
    generalize (P a); clear P; simpl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H:b2 = a1
a:A
(if eq_dec a1 a then 1 else 0) +
((if eq_dec b1 a then 1 else 0) + 0) =
(if eq_dec a2 a then 1 else 0) +
((if eq_dec b2 a then 1 else 0) + 0) ->
(if eq_dec a2 a then 1 else 0) + 0 =
(if eq_dec b1 a then 1 else 0) + 0
    destruct (eq_dec a1 a) as [H2|H2];
      destruct (eq_dec b2 a) as [H3|H3]; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H:b2 = a1
a:A
H2:a1 = a
H3:b2 = a
1 + ((if eq_dec b1 a then 1 else 0) + 0) =
(if eq_dec a2 a then 1 else 0) + (1 + 0) ->
(if eq_dec a2 a then 1 else 0) + 0 =
(if eq_dec b1 a then 1 else 0) + 0
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H:b2 = a1
a:A
H2:a1 = a
H3:b2 <> a
1 + ((if eq_dec b1 a then 1 else 0) + 0) =
(if eq_dec a2 a then 1 else 0) + (0 + 0) ->
(if eq_dec a2 a then 1 else 0) + 0 =
(if eq_dec b1 a then 1 else 0) + 0
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H:b2 = a1
a:A
H2:a1 <> a
H3:b2 = a
0 + ((if eq_dec b1 a then 1 else 0) + 0) =
(if eq_dec a2 a then 1 else 0) + (1 + 0) ->
(if eq_dec a2 a then 1 else 0) + 0 =
(if eq_dec b1 a then 1 else 0) + 0
    simpl; rewrite <- plus_n_Sm; inversion 1; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H:b2 = a1
a:A
H2:a1 = a
H3:b2 <> a
1 + ((if eq_dec b1 a then 1 else 0) + 0) =
(if eq_dec a2 a then 1 else 0) + (0 + 0) ->
(if eq_dec a2 a then 1 else 0) + 0 =
(if eq_dec b1 a then 1 else 0) + 0
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H:b2 = a1
a:A
H2:a1 <> a
H3:b2 = a
0 + ((if eq_dec b1 a then 1 else 0) + 0) =
(if eq_dec a2 a then 1 else 0) + (1 + 0) ->
(if eq_dec a2 a then 1 else 0) + 0 =
(if eq_dec b1 a then 1 else 0) + 0
    destruct H3; transitivity a1; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a1, b1, a2, b2:A
H:b2 = a1
a:A
H2:a1 <> a
H3:b2 = a
0 + ((if eq_dec b1 a then 1 else 0) + 0) =
(if eq_dec a2 a then 1 else 0) + (1 + 0) ->
(if eq_dec a2 a then 1 else 0) + 0 =
(if eq_dec b1 a then 1 else 0) + 0
    destruct H2; transitivity b2; auto.
  Qed.

Permutation is compatible with length.

  Lemma permut_length :
    forall l1 l2, permutation l1 l2 -> length l1 = length l2.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l1 l2 : list A,
permutation l1 l2 -> length l1 = length l2
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall l1 l2 : list A,
permutation l1 l2 -> length l1 = length l2
    induction l1; intros l2 H.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
l2:list A
H:permutation nil l2
length nil = length l2
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l1:list A
IHl1:forall l0 : list A,
permutation l1 l0 -> length l1 = length l0
l2:list A
H:permutation (a :: l1) l2
length (a :: l1) = length l2
    rewrite (permut_nil (permut_sym H)); auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l1:list A
IHl1:forall l0 : list A,
permutation l1 l0 -> length l1 = length l0
l2:list A
H:permutation (a :: l1) l2
length (a :: l1) = length l2
    destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l1:list A
IHl1:forall l0 : list A,
permutation l1 l0 -> length l1 = length l0
l2:list A
H:permutation (a :: l1) l2
h2, t2:list A
H1:l2 = h2 ++ a :: t2
length (a :: l1) = length l2
    subst l2.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2, t2:list A
H:permutation (a :: l1) (h2 ++ a :: t2)
length (a :: l1) = length (h2 ++ a :: t2)
    rewrite app_length.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2, t2:list A
H:permutation (a :: l1) (h2 ++ a :: t2)
length (a :: l1) = length h2 + length (a :: t2)
    simpl; rewrite <- plus_n_Sm; f_equal.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2, t2:list A
H:permutation (a :: l1) (h2 ++ a :: t2)
length l1 = length h2 + length t2
    rewrite <- app_length.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2, t2:list A
H:permutation (a :: l1) (h2 ++ a :: t2)
length l1 = length (h2 ++ t2)
    apply IHl1.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2, t2:list A
H:permutation (a :: l1) (h2 ++ a :: t2)
permutation l1 (h2 ++ t2)
    apply permut_remove_hd with a; auto with typeclass_instances.
  Qed.

  Variable B : Type.
  Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }.

Permutation is compatible with map.

  Lemma permutation_map :
    forall f l1 l2, permutation l1 l2 ->
      PermutSetoid.permutation _ eqB_dec (map f l1) (map f l2).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
forall (f : A -> B) (l1 l2 : list A),
permutation l1 l2 ->
PermutSetoid.permutation eq eqB_dec (map f l1)
  (map f l2)
  Proof.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
forall (f : A -> B) (l1 l2 : list A),
permutation l1 l2 ->
PermutSetoid.permutation eq eqB_dec (map f l1)
  (map f l2)
    intros f; induction l1.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
forall l2 : list A,
permutation nil l2 ->
PermutSetoid.permutation eq eqB_dec (map f nil)
  (map f l2)
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l2)
forall l2 : list A,
permutation (a :: l1) l2 ->
PermutSetoid.permutation eq eqB_dec 
  (map f (a :: l1)) (map f l2)
    intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l2)
forall l2 : list A,
permutation (a :: l1) l2 ->
PermutSetoid.permutation eq eqB_dec (map f (a :: l1))
  (map f l2)
    intros l2 P.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l0 : list A,
permutation l1 l0 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l0)
l2:list A
P:permutation (a :: l1) l2
PermutSetoid.permutation eq eqB_dec (map f (a :: l1))
  (map f l2)
    simpl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l0 : list A,
permutation l1 l0 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l0)
l2:list A
P:permutation (a :: l1) l2
PermutSetoid.permutation eq eqB_dec (f a :: map f l1)
  (map f l2)
    destruct (In_split _ _ (permut_cons_In P)) as (h2,(t2,H1)).A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l0 : list A,
permutation l1 l0 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l0)
l2:list A
P:permutation (a :: l1) l2
h2, t2:list A
H1:l2 = h2 ++ a :: t2
PermutSetoid.permutation eq eqB_dec (f a :: map f l1)
  (map f l2)
    subst l2.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l2)
h2, t2:list A
P:permutation (a :: l1) (h2 ++ a :: t2)
PermutSetoid.permutation eq eqB_dec (f a :: map f l1)
  (map f (h2 ++ a :: t2))
    rewrite map_app.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l2)
h2, t2:list A
P:permutation (a :: l1) (h2 ++ a :: t2)
PermutSetoid.permutation eq eqB_dec (f a :: map f l1)
  (map f h2 ++ map f (a :: t2))
    simpl.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l2)
h2, t2:list A
P:permutation (a :: l1) (h2 ++ a :: t2)
PermutSetoid.permutation eq eqB_dec (f a :: map f l1)
  (map f h2 ++ f a :: map f t2)
    apply permut_add_cons_inside.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l2)
h2, t2:list A
P:permutation (a :: l1) (h2 ++ a :: t2)
PermutSetoid.permutation eq eqB_dec (map f l1)
  (map f h2 ++ map f t2)
    rewrite <- map_app.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l2)
h2, t2:list A
P:permutation (a :: l1) (h2 ++ a :: t2)
PermutSetoid.permutation eq eqB_dec (map f l1)
  (map f (h2 ++ t2))
    apply IHl1; auto.A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
B:Type
eqB_dec:forall x y : B, {x = y} + {x <> y}
f:A -> B
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 ->
PermutSetoid.permutation eq eqB_dec 
  (map f l1) (map f l2)
h2, t2:list A
P:permutation (a :: l1) (h2 ++ a :: t2)
permutation l1 (h2 ++ t2)
    apply permut_remove_hd with a; auto with typeclass_instances.
  Qed.

End Perm.