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 Omega Relations Multiset SetoidList.

This file is deprecated, use Permutation.v instead.

Indeed, this file defines a notion of permutation based on multisets (there exists a permutation between two lists iff every elements have the same multiplicity in the two lists) which requires a more complex apparatus (the equipment of the domain with a decidable equality) than Permutation in Permutation.v.

The relation between the two relations are in lemma permutation_Permutation.

File Permutation concerns Leibniz equality : it shows in particular that List.Permutation and permutation are equivalent in this context.

Set Implicit Arguments.

Local Notation "[ ]" := nil.
Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).

Section Permut.

From lists to multisets

Variable A : Type.
Variable eqA : relation A.
Hypothesis eqA_equiv : Equivalence eqA.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.

Let emptyBag := EmptyBag A.
Let singletonBag := SingletonBag _ eqA_dec.

contents of a list

Fixpoint list_contents (l:list A) : multiset A :=
  match l with
  | [] => emptyBag
  | a :: l => munion (singletonBag a) (list_contents l)
  end.

Lemma list_contents_app :
  forall l m:list A,
    meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l m : list A,
meq (list_contents (l ++ m))
  (munion (list_contents l) (list_contents m))
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l m : list A,
meq (list_contents (l ++ m))
  (munion (list_contents l) (list_contents m))
  simple induction l; simpl; auto with datatypes.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
forall (a : A) (l0 : list A),
(forall m : list A,
 meq (list_contents (l0 ++ m))
   (munion (list_contents l0) (list_contents m))) ->
forall m : list A,
meq
  (munion (singletonBag a) (list_contents (l0 ++ m)))
  (munion (munion (singletonBag a) (list_contents l0))
     (list_contents m))
  intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
H:forall m0 : list A,
meq (list_contents (l0 ++ m0))
  (munion (list_contents l0) (list_contents m0))
m:list A
meq
  (munion (singletonBag a) (list_contents (l0 ++ m)))
  (munion (munion (singletonBag a) (list_contents l0))
     (list_contents m))
  apply meq_trans with
    (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
    auto with datatypes.
Qed.

permutation: definition and basic properties

Definition permutation (l m:list A) := meq (list_contents l) (list_contents m).

Lemma permut_refl : forall l:list A, permutation l l.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A, permutation l l
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A, permutation l l
  unfold permutation; auto with datatypes.
Qed.

Lemma permut_sym :
  forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l1 l2 : list A,
permutation l1 l2 -> permutation l2 l1
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l1 l2 : list A,
permutation l1 l2 -> permutation l2 l1
  unfold permutation, meq; intros; symmetry; trivial.
Qed.

Lemma permut_trans :
  forall l m n:list A, permutation l m -> permutation m n -> permutation l n.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l m n : list A,
permutation l m -> permutation m n -> permutation l n
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l m n : list A,
permutation l m -> permutation m n -> permutation l n
  unfold permutation; intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, m, n:list A
H:meq (list_contents l) (list_contents m)
H0:meq (list_contents m) (list_contents n)
meq (list_contents l) (list_contents n)
  apply meq_trans with (list_contents m); auto with datatypes.
Qed.

Lemma permut_cons_eq :
  forall l m:list A,
    permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l m : list A,
permutation l m ->
forall a a' : A,
eqA a a' -> permutation (a :: l) (a' :: m)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l m : list A,
permutation l m ->
forall a a' : A,
eqA a a' -> permutation (a :: l) (a' :: m)
  unfold permutation; simpl; intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, m:list A
H:meq (list_contents l) (list_contents m)
a, a':A
H0:eqA a a'
meq (munion (singletonBag a) (list_contents l))
  (munion (singletonBag a') (list_contents m))
  apply meq_trans with (munion (singletonBag a') (list_contents l)).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, m:list A
H:meq (list_contents l) (list_contents m)
a, a':A
H0:eqA a a'
meq (munion (singletonBag a) (list_contents l))
  (munion (singletonBag a') (list_contents l))
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, m:list A
H:meq (list_contents l) (list_contents m)
a, a':A
H0:eqA a a'
meq (munion (singletonBag a') (list_contents l))
  (munion (singletonBag a') (list_contents m))
  apply meq_left, meq_singleton; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, m:list A
H:meq (list_contents l) (list_contents m)
a, a':A
H0:eqA a a'
meq (munion (singletonBag a') (list_contents l))
  (munion (singletonBag a') (list_contents m))
  auto with datatypes.
Qed.

Lemma permut_cons :
  forall l m:list A,
    permutation l m -> forall a:A, permutation (a :: l) (a :: m).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l m : list A,
permutation l m ->
forall a : A, permutation (a :: l) (a :: m)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l m : list A,
permutation l m ->
forall a : A, permutation (a :: l) (a :: m)
  unfold permutation; simpl; auto with datatypes.
Qed.

Lemma permut_app :
  forall l l' m m':list A,
    permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l l' m m' : list A,
permutation l l' ->
permutation m m' -> permutation (l ++ m) (l' ++ m')
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l l' m m' : list A,
permutation l l' ->
permutation m m' -> permutation (l ++ m) (l' ++ m')
  unfold permutation; intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l', m, m':list A
H:meq (list_contents l) (list_contents l')
H0:meq (list_contents m) (list_contents m')
meq (list_contents (l ++ m))
  (list_contents (l' ++ m'))
  apply meq_trans with (munion (list_contents l) (list_contents m));
    auto using permut_cons, list_contents_app with datatypes.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l', m, m':list A
H:meq (list_contents l) (list_contents l')
H0:meq (list_contents m) (list_contents m')
meq (munion (list_contents l) (list_contents m))
  (list_contents (l' ++ m'))
  apply meq_trans with (munion (list_contents l') (list_contents m'));
    auto using permut_cons, list_contents_app with datatypes.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l', m, m':list A
H:meq (list_contents l) (list_contents l')
H0:meq (list_contents m) (list_contents m')
meq (munion (list_contents l) (list_contents m))
  (munion (list_contents l') (list_contents m'))
  apply meq_trans with (munion (list_contents l') (list_contents m));
    auto using permut_cons, list_contents_app with datatypes.
Qed.

Lemma permut_add_inside_eq :
  forall a a' l1 l2 l3 l4, eqA a a' ->
    permutation (l1 ++ l2) (l3 ++ l4) ->
    permutation (l1 ++ a :: l2) (l3 ++ a' :: l4).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a a' : A) (l1 l2 l3 l4 : list A),
eqA a a' ->
permutation (l1 ++ l2) (l3 ++ l4) ->
permutation (l1 ++ a :: l2) (l3 ++ a' :: l4)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a a' : A) (l1 l2 l3 l4 : list A),
eqA a a' ->
permutation (l1 ++ l2) (l3 ++ l4) ->
permutation (l1 ++ a :: l2) (l3 ++ a' :: l4)
  unfold permutation, meq in *; intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a, a':A
l1, l2, l3, l4:list A
H:eqA a a'
H0:forall a1 : A,
multiplicity (list_contents (l1 ++ l2)) a1 =
multiplicity (list_contents (l3 ++ l4)) a1
a0:A
multiplicity (list_contents (l1 ++ a :: l2)) a0 =
multiplicity (list_contents (l3 ++ a' :: l4)) a0
  specialize H0 with a0.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a, a':A
l1, l2, l3, l4:list A
H:eqA a a'
a0:A
H0:multiplicity (list_contents (l1 ++ l2)) a0 =
multiplicity (list_contents (l3 ++ l4)) a0
multiplicity (list_contents (l1 ++ a :: l2)) a0 =
multiplicity (list_contents (l3 ++ a' :: l4)) a0
  repeat rewrite list_contents_app in *; simpl in *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a, a':A
l1, l2, l3, l4:list A
H:eqA a a'
a0:A
H0:multiplicity (list_contents l1) a0 +
multiplicity (list_contents l2) a0 =
multiplicity (list_contents l3) a0 +
multiplicity (list_contents l4) a0
multiplicity (list_contents l1) a0 +
((if eqA_dec a a0 then 1 else 0) +
 multiplicity (list_contents l2) a0) =
multiplicity (list_contents l3) a0 +
((if eqA_dec a' a0 then 1 else 0) +
 multiplicity (list_contents l4) a0)
  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite H in Ha;
    decide (eqA_dec a' a0) with Ha; simpl; auto with arith.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a, a':A
l1, l2, l3, l4:list A
H:eqA a a'
a0:A
H0:multiplicity (list_contents l1) a0 +
multiplicity (list_contents l2) a0 =
multiplicity (list_contents l3) a0 +
multiplicity (list_contents l4) a0
Ha:eqA a' a0
multiplicity (list_contents l1) a0 +
S (multiplicity (list_contents l2) a0) =
multiplicity (list_contents l3) a0 +
S (multiplicity (list_contents l4) a0)
  do 2 rewrite <- plus_n_Sm; f_equal; auto.
Qed.

Lemma permut_add_inside :
  forall a l1 l2 l3 l4,
    permutation (l1 ++ l2) (l3 ++ l4) ->
    permutation (l1 ++ a :: l2) (l3 ++ a :: l4).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a : A) (l1 l2 l3 l4 : list A),
permutation (l1 ++ l2) (l3 ++ l4) ->
permutation (l1 ++ a :: l2) (l3 ++ a :: l4)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a : A) (l1 l2 l3 l4 : list A),
permutation (l1 ++ l2) (l3 ++ l4) ->
permutation (l1 ++ a :: l2) (l3 ++ a :: l4)
  unfold permutation, meq in *; intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1, l2, l3, l4:list A
H:forall a1 : A,
multiplicity (list_contents (l1 ++ l2)) a1 =
multiplicity (list_contents (l3 ++ l4)) a1
a0:A
multiplicity (list_contents (l1 ++ a :: l2)) a0 =
multiplicity (list_contents (l3 ++ a :: l4)) a0
  generalize (H a0); clear H.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1, l2, l3, l4:list A
a0:A
multiplicity (list_contents (l1 ++ l2)) a0 =
multiplicity (list_contents (l3 ++ l4)) a0 ->
multiplicity (list_contents (l1 ++ a :: l2)) a0 =
multiplicity (list_contents (l3 ++ a :: l4)) a0
  do 4 rewrite list_contents_app.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1, l2, l3, l4:list A
a0:A
multiplicity
  (munion (list_contents l1) (list_contents l2)) a0 =
multiplicity
  (munion (list_contents l3) (list_contents l4)) a0 ->
multiplicity
  (munion (list_contents l1) (list_contents (a :: l2)))
  a0 =
multiplicity
  (munion (list_contents l3) (list_contents (a :: l4)))
  a0
  simpl.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1, l2, l3, l4:list A
a0:A
multiplicity (list_contents l1) a0 +
multiplicity (list_contents l2) a0 =
multiplicity (list_contents l3) a0 +
multiplicity (list_contents l4) a0 ->
multiplicity (list_contents l1) a0 +
((if eqA_dec a a0 then 1 else 0) +
 multiplicity (list_contents l2) a0) =
multiplicity (list_contents l3) a0 +
((if eqA_dec a a0 then 1 else 0) +
 multiplicity (list_contents l4) a0)
  destruct (eqA_dec a a0); simpl; auto with arith.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1, l2, l3, l4:list A
a0:A
e:eqA a a0
multiplicity (list_contents l1) a0 +
multiplicity (list_contents l2) a0 =
multiplicity (list_contents l3) a0 +
multiplicity (list_contents l4) a0 ->
multiplicity (list_contents l1) a0 +
S (multiplicity (list_contents l2) a0) =
multiplicity (list_contents l3) a0 +
S (multiplicity (list_contents l4) a0)
  do 2 rewrite <- plus_n_Sm; f_equal; auto.
Qed.

Lemma permut_add_cons_inside_eq :
  forall a a' l l1 l2, eqA a a' ->
    permutation l (l1 ++ l2) ->
    permutation (a :: l) (l1 ++ a' :: l2).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a a' : A) (l l1 l2 : list A),
eqA a a' ->
permutation l (l1 ++ l2) ->
permutation (a :: l) (l1 ++ a' :: l2)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a a' : A) (l l1 l2 : list A),
eqA a a' ->
permutation l (l1 ++ l2) ->
permutation (a :: l) (l1 ++ a' :: l2)
  intros;
  replace (a :: l) with ([] ++ a :: l); trivial;
    apply permut_add_inside_eq; trivial.
Qed.

Lemma permut_add_cons_inside :
  forall a l l1 l2,
    permutation l (l1 ++ l2) ->
    permutation (a :: l) (l1 ++ a :: l2).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a : A) (l l1 l2 : list A),
permutation l (l1 ++ l2) ->
permutation (a :: l) (l1 ++ a :: l2)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a : A) (l l1 l2 : list A),
permutation l (l1 ++ l2) ->
permutation (a :: l) (l1 ++ a :: l2)
  intros;
    replace (a :: l) with ([] ++ a :: l); trivial;
	apply permut_add_inside; trivial.
Qed.

Lemma permut_middle :
  forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l m : list A) (a : A),
permutation (a :: l ++ m) (l ++ a :: m)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l m : list A) (a : A),
permutation (a :: l ++ m) (l ++ a :: m)
  intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl.
Qed.

Lemma permut_sym_app :
  forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l1 l2 : list A,
permutation (l1 ++ l2) (l2 ++ l1)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l1 l2 : list A,
permutation (l1 ++ l2) (l2 ++ l1)
  intros l1 l2;
    unfold permutation, meq;
	intro a; do 2 rewrite list_contents_app; simpl;
	  auto with arith.
Qed.

Lemma permut_rev :
  forall l, permutation l (rev l).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A, permutation l (rev l)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A, permutation l (rev l)
  induction l.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
permutation [ ] (rev [ ])
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:permutation l (rev l)
permutation (a :: l) (rev (a :: l))
  simpl; trivial using permut_refl.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:permutation l (rev l)
permutation (a :: l) (rev (a :: l))
  simpl.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:permutation l (rev l)
permutation (a :: l) (rev l ++ [a])
  apply permut_add_cons_inside.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:permutation l (rev l)
permutation l (rev l ++ [ ])
  rewrite app_nil_r.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:permutation l (rev l)
permutation l (rev l) trivial.
Qed.

Some inversion results.

Lemma permut_conv_inv :
  forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (e : A) (l1 l2 : list A),
permutation (e :: l1) (e :: l2) -> permutation l1 l2
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (e : A) (l1 l2 : list A),
permutation (e :: l1) (e :: l2) -> permutation l1 l2
  intros e l1 l2; unfold permutation, meq; simpl; intros H a;
    generalize (H a); apply plus_reg_l.
Qed.

Lemma permut_app_inv1 :
  forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l l1 l2 : list A,
permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l l1 l2 : list A,
permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2
  intros l l1 l2; unfold permutation, meq; simpl;
    intros H a; generalize (H a); clear H.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a:A
multiplicity (list_contents (l1 ++ l)) a =
multiplicity (list_contents (l2 ++ l)) a ->
multiplicity (list_contents l1) a =
multiplicity (list_contents l2) a
  do 2 rewrite list_contents_app.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a:A
multiplicity
  (munion (list_contents l1) (list_contents l)) a =
multiplicity
  (munion (list_contents l2) (list_contents l)) a ->
multiplicity (list_contents l1) a =
multiplicity (list_contents l2) a
  simpl.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a:A
multiplicity (list_contents l1) a +
multiplicity (list_contents l) a =
multiplicity (list_contents l2) a +
multiplicity (list_contents l) a ->
multiplicity (list_contents l1) a =
multiplicity (list_contents l2) a
  intros; apply plus_reg_l with (multiplicity (list_contents l) a).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a:A
H:multiplicity (list_contents l1) a +
multiplicity (list_contents l) a =
multiplicity (list_contents l2) a +
multiplicity (list_contents l) a
multiplicity (list_contents l) a +
multiplicity (list_contents l1) a =
multiplicity (list_contents l) a +
multiplicity (list_contents l2) a
  rewrite plus_comm; rewrite H; rewrite plus_comm.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a:A
H:multiplicity (list_contents l1) a +
multiplicity (list_contents l) a =
multiplicity (list_contents l2) a +
multiplicity (list_contents l) a
multiplicity (list_contents l) a +
multiplicity (list_contents l2) a =
multiplicity (list_contents l) a +
multiplicity (list_contents l2) a
  trivial.
Qed.

we can use multiplicity to define InA and NoDupA.

Fact if_eqA_then : forall a a' (B:Type)(b b':B),
 eqA a a' -> (if eqA_dec a a' then b else b') = b.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a a' : A) (B : Type) (b b' : B),
eqA a a' -> (if eqA_dec a a' then b else b') = b
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a a' : A) (B : Type) (b b' : B),
eqA a a' -> (if eqA_dec a a' then b else b') = b
  intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a, a':A
B:Type
b, b':B
H:eqA a a'
(if eqA_dec a a' then b else b') = b destruct eqA_dec as [_|NEQ]; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a, a':A
B:Type
b, b':B
H:eqA a a'
NEQ:~ eqA a a'
b' = b
  contradict NEQ; auto.
Qed.

Lemma permut_app_inv2 :
  forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l l1 l2 : list A,
permutation (l ++ l1) (l ++ l2) -> permutation l1 l2
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l l1 l2 : list A,
permutation (l ++ l1) (l ++ l2) -> permutation l1 l2
  intros l l1 l2; unfold permutation, meq; simpl;
    intros H a; generalize (H a); clear H.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a:A
multiplicity (list_contents (l ++ l1)) a =
multiplicity (list_contents (l ++ l2)) a ->
multiplicity (list_contents l1) a =
multiplicity (list_contents l2) a
  do 2 rewrite list_contents_app.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a:A
multiplicity
  (munion (list_contents l) (list_contents l1)) a =
multiplicity
  (munion (list_contents l) (list_contents l2)) a ->
multiplicity (list_contents l1) a =
multiplicity (list_contents l2) a
  simpl.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a:A
multiplicity (list_contents l) a +
multiplicity (list_contents l1) a =
multiplicity (list_contents l) a +
multiplicity (list_contents l2) a ->
multiplicity (list_contents l1) a =
multiplicity (list_contents l2) a
  intros; apply plus_reg_l with (multiplicity (list_contents l) a).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a:A
H:multiplicity (list_contents l) a +
multiplicity (list_contents l1) a =
multiplicity (list_contents l) a +
multiplicity (list_contents l2) a
multiplicity (list_contents l) a +
multiplicity (list_contents l1) a =
multiplicity (list_contents l) a +
multiplicity (list_contents l2) a
  trivial.
Qed.

Lemma permut_remove_hd_eq :
  forall l l1 l2 a b, eqA a b ->
    permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l l1 l2 : list A) (a b : A),
eqA a b ->
permutation (a :: l) (l1 ++ b :: l2) ->
permutation l (l1 ++ l2)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l l1 l2 : list A) (a b : A),
eqA a b ->
permutation (a :: l) (l1 ++ b :: l2) ->
permutation l (l1 ++ l2)
  unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a, b:A
Heq:eqA a b
H:forall a1 : A,
(if eqA_dec a a1 then 1 else 0) +
multiplicity (list_contents l) a1 =
multiplicity (list_contents (l1 ++ b :: l2)) a1
a0:A
multiplicity (list_contents l) a0 =
multiplicity (list_contents (l1 ++ l2)) a0
  specialize H with a0.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a, b:A
Heq:eqA a b
a0:A
H:(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 =
multiplicity (list_contents (l1 ++ b :: l2)) a0
multiplicity (list_contents l) a0 =
multiplicity (list_contents (l1 ++ l2)) a0
  rewrite list_contents_app in *; simpl in *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a, b:A
Heq:eqA a b
a0:A
H:(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 =
multiplicity (list_contents l1) a0 +
((if eqA_dec b a0 then 1 else 0) +
 multiplicity (list_contents l2) a0)
multiplicity (list_contents l) a0 =
multiplicity (list_contents l1) a0 +
multiplicity (list_contents l2) a0
  apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a, b:A
Heq:eqA a b
a0:A
H:(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 =
multiplicity (list_contents l1) a0 +
((if eqA_dec b a0 then 1 else 0) +
 multiplicity (list_contents l2) a0)
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 =
(if eqA_dec a a0 then 1 else 0) +
(multiplicity (list_contents l1) a0 +
 multiplicity (list_contents l2) a0)
  rewrite H; clear H.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a, b:A
Heq:eqA a b
a0:A
multiplicity (list_contents l1) a0 +
((if eqA_dec b a0 then 1 else 0) +
 multiplicity (list_contents l2) a0) =
(if eqA_dec a a0 then 1 else 0) +
(multiplicity (list_contents l1) a0 +
 multiplicity (list_contents l2) a0)
  symmetry; rewrite plus_comm, <- ! plus_assoc; f_equal.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a, b:A
Heq:eqA a b
a0:A
multiplicity (list_contents l2) a0 +
(if eqA_dec a a0 then 1 else 0) =
(if eqA_dec b a0 then 1 else 0) +
multiplicity (list_contents l2) a0
  rewrite plus_comm.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l1, l2:list A
a, b:A
Heq:eqA a b
a0:A
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l2) a0 =
(if eqA_dec b a0 then 1 else 0) +
multiplicity (list_contents l2) a0
  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite Heq in Ha;
    decide (eqA_dec b a0) with Ha; reflexivity.
Qed.

Lemma permut_remove_hd :
  forall l l1 l2 a,
    permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l l1 l2 : list A) (a : A),
permutation (a :: l) (l1 ++ a :: l2) ->
permutation l (l1 ++ l2)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l l1 l2 : list A) (a : A),
permutation (a :: l) (l1 ++ a :: l2) ->
permutation l (l1 ++ l2)
  eauto using permut_remove_hd_eq, Equivalence_Reflexive.
Qed.

Fact if_eqA_else : forall a a' (B:Type)(b b':B),
 ~eqA a a' -> (if eqA_dec a a' then b else b') = b'.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a a' : A) (B : Type) (b b' : B),
~ eqA a a' -> (if eqA_dec a a' then b else b') = b'
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a a' : A) (B : Type) (b b' : B),
~ eqA a a' -> (if eqA_dec a a' then b else b') = b'
  intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a, a':A
B:Type
b, b':B
H:~ eqA a a'
(if eqA_dec a a' then b else b') = b' decide (eqA_dec a a') with H; auto.
Qed.

Fact if_eqA_refl : forall a (B:Type)(b b':B),
 (if eqA_dec a a then b else b') = b.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a : A) (B : Type) (b b' : B),
(if eqA_dec a a then b else b') = b
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a : A) (B : Type) (b b' : B),
(if eqA_dec a a then b else b') = b
  intros; apply (decide_left (eqA_dec a a)); auto with *.
Qed.

PL: Inutilisable dans un rewrite sans un change prealable.

Instance if_eqA (B:Type)(b b':B) :
 Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
B:Type
b, b':B
Proper (eqA ==> eqA ==> eq)
  (fun x y : A => if eqA_dec x y then b else b')
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
B:Type
b, b':B
Proper (eqA ==> eqA ==> eq)
  (fun x y : A => if eqA_dec x y then b else b')
 intros x x' Hxx' y y' Hyy'.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
B:Type
b, b':B
x, x':A
Hxx':eqA x x'
y, y':A
Hyy':eqA y y'
(if eqA_dec x y then b else b') =
(if eqA_dec x' y' then b else b')
 intros; destruct (eqA_dec x y) as [H|H];
  destruct (eqA_dec x' y') as [H'|H']; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
B:Type
b, b':B
x, x':A
Hxx':eqA x x'
y, y':A
Hyy':eqA y y'
H:eqA x y
H':~ eqA x' y'
b = b'
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
B:Type
b, b':B
x, x':A
Hxx':eqA x x'
y, y':A
Hyy':eqA y y'
H:~ eqA x y
H':eqA x' y'
b' = b
 contradict H'; transitivity x; auto with *; transitivity y; auto with *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
B:Type
b, b':B
x, x':A
Hxx':eqA x x'
y, y':A
Hyy':eqA y y'
H:~ eqA x y
H':eqA x' y'
b' = b
 contradict H; transitivity x'; auto with *; transitivity y'; auto with *.
Qed.

Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B),
 eqA a1 a1' -> (if eqA_dec a1 a2 then b else b') =
               (if eqA_dec a1' a2 then b else b').A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a1 a1' a2 : A) (B : Type) (b b' : B),
eqA a1 a1' ->
(if eqA_dec a1 a2 then b else b') =
(if eqA_dec a1' a2 then b else b')
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a1 a1' a2 : A) (B : Type) (b b' : B),
eqA a1 a1' ->
(if eqA_dec a1 a2 then b else b') =
(if eqA_dec a1' a2 then b else b')
 intros; destruct (eqA_dec a1 a2) as [A1|A1];
  destruct (eqA_dec a1' a2) as [A1'|A1']; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, a1', a2:A
B:Type
b, b':B
H:eqA a1 a1'
A1:eqA a1 a2
A1':~ eqA a1' a2
b = b'
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, a1', a2:A
B:Type
b, b':B
H:eqA a1 a1'
A1:~ eqA a1 a2
A1':eqA a1' a2
b' = b
 contradict A1'; transitivity a1; eauto with *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, a1', a2:A
B:Type
b, b':B
H:eqA a1 a1'
A1:~ eqA a1 a2
A1':eqA a1' a2
b' = b
 contradict A1; transitivity a1'; eauto with *.
Qed.

Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B),
 eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') =
               (if eqA_dec a1 a2' then b else b').A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a1 a2 a2' : A) (B : Type) (b b' : B),
eqA a2 a2' ->
(if eqA_dec a1 a2 then b else b') =
(if eqA_dec a1 a2' then b else b')
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a1 a2 a2' : A) (B : Type) (b b' : B),
eqA a2 a2' ->
(if eqA_dec a1 a2 then b else b') =
(if eqA_dec a1 a2' then b else b')
 intros; destruct (eqA_dec a1 a2) as [A2|A2];
  destruct (eqA_dec a1 a2') as [A2'|A2']; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, a2, a2':A
B:Type
b, b':B
H:eqA a2 a2'
A2:eqA a1 a2
A2':~ eqA a1 a2'
b = b'
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, a2, a2':A
B:Type
b, b':B
H:eqA a2 a2'
A2:~ eqA a1 a2
A2':eqA a1 a2'
b' = b
 contradict A2'; transitivity a2; eauto with *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, a2, a2':A
B:Type
b, b':B
H:eqA a2 a2'
A2:~ eqA a1 a2
A2':eqA a1 a2'
b' = b
 contradict A2; transitivity a2'; eauto with *.
Qed.


Instance multiplicity_eqA (l:list A) :
 Proper (eqA==>@eq _) (multiplicity (list_contents l)).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
Proper (eqA ==> eq) (multiplicity (list_contents l))
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
Proper (eqA ==> eq) (multiplicity (list_contents l))
  intros x x' Hxx'.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x0 y : A, {eqA x0 y} + {~ eqA x0 y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
x, x':A
Hxx':eqA x x'
multiplicity (list_contents l) x =
multiplicity (list_contents l) x'
  induction l as [|y l Hl]; simpl; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
y:A
l:list A
x, x':A
Hxx':eqA x x'
Hl:multiplicity (list_contents l) x =
multiplicity (list_contents l) x'
(if eqA_dec y x then 1 else 0) +
multiplicity (list_contents l) x =
(if eqA_dec y x' then 1 else 0) +
multiplicity (list_contents l) x'
  rewrite (@if_eqA_rewrite_r y x x'); auto.
Qed.

Lemma multiplicity_InA :
  forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l : list A) (a : A),
InA eqA a l <-> 0 < multiplicity (list_contents l) a
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l : list A) (a : A),
InA eqA a l <-> 0 < multiplicity (list_contents l) a
  induction l.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall a : A,
InA eqA a [ ] <->
0 < multiplicity (list_contents [ ]) a
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
forall a0 : A,
InA eqA a0 (a :: l) <->
0 < multiplicity (list_contents (a :: l)) a0
  simpl.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall a : A, InA eqA a [ ] <-> 0 < 0
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
forall a0 : A,
InA eqA a0 (a :: l) <->
0 < multiplicity (list_contents (a :: l)) a0
  split; inversion 1.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
forall a0 : A,
InA eqA a0 (a :: l) <->
0 < multiplicity (list_contents (a :: l)) a0
  simpl.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
forall a0 : A,
InA eqA a0 (a :: l) <->
0 <
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0
  intros a'; split; intros H.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
H:InA eqA a' (a :: l)
0 <
(if eqA_dec a a' then 1 else 0) +
multiplicity (list_contents l) a'
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
H:0 <
(if eqA_dec a a' then 1 else 0) +
multiplicity (list_contents l) a'
InA eqA a' (a :: l) inversion_clear H.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
H0:eqA a' a
0 <
(if eqA_dec a a' then 1 else 0) +
multiplicity (list_contents l) a'
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
H0:InA eqA a' l
0 <
(if eqA_dec a a' then 1 else 0) +
multiplicity (list_contents l) a'
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
H:0 <
(if eqA_dec a a' then 1 else 0) +
multiplicity (list_contents l) a'
InA eqA a' (a :: l)
  apply (decide_left (eqA_dec a a')); auto with *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
H0:InA eqA a' l
0 <
(if eqA_dec a a' then 1 else 0) +
multiplicity (list_contents l) a'
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
H:0 <
(if eqA_dec a a' then 1 else 0) +
multiplicity (list_contents l) a'
InA eqA a' (a :: l)
  destruct (eqA_dec a a'); auto with *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
H0:InA eqA a' l
n:~ eqA a a'
0 < 0 + multiplicity (list_contents l) a'
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
H:0 <
(if eqA_dec a a' then 1 else 0) +
multiplicity (list_contents l) a'
InA eqA a' (a :: l) simpl; rewrite <- IHl; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
H:0 <
(if eqA_dec a a' then 1 else 0) +
multiplicity (list_contents l) a'
InA eqA a' (a :: l)
  destruct (eqA_dec a a'); auto with *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
n:~ eqA a a'
H:0 < 0 + multiplicity (list_contents l) a'
InA eqA a' (a :: l) right.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:forall a0 : A,
InA eqA a0 l <->
0 < multiplicity (list_contents l) a0
a':A
n:~ eqA a a'
H:0 < 0 + multiplicity (list_contents l) a'
InA eqA a' l rewrite IHl; auto.
Qed.

Lemma multiplicity_InA_O :
  forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l : list A) (a : A),
~ InA eqA a l -> multiplicity (list_contents l) a = 0
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l : list A) (a : A),
~ InA eqA a l -> multiplicity (list_contents l) a = 0
  intros l a; rewrite multiplicity_InA;
    destruct (multiplicity (list_contents l) a); auto with arith.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
n:nat
~ 0 < S n -> S n = 0
  destruct 1; auto with arith.
Qed.

Lemma multiplicity_InA_S :
  forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l : list A) (a : A),
InA eqA a l -> multiplicity (list_contents l) a >= 1
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l : list A) (a : A),
InA eqA a l -> multiplicity (list_contents l) a >= 1
  intros l a; rewrite multiplicity_InA; auto with arith.
Qed.

Lemma multiplicity_NoDupA : forall l,
  NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A,
NoDupA eqA l <->
(forall a : A, multiplicity (list_contents l) a <= 1)
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A,
NoDupA eqA l <->
(forall a : A, multiplicity (list_contents l) a <= 1)
  induction l.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
NoDupA eqA [ ] <->
(forall a : A, multiplicity (list_contents [ ]) a <= 1)
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
NoDupA eqA (a :: l) <->
(forall a0 : A,
 multiplicity (list_contents (a :: l)) a0 <= 1)
  simpl.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
NoDupA eqA [ ] <-> (A -> 0 <= 1)
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
NoDupA eqA (a :: l) <->
(forall a0 : A,
 multiplicity (list_contents (a :: l)) a0 <= 1)
  split; auto with arith.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
NoDupA eqA (a :: l) <->
(forall a0 : A,
 multiplicity (list_contents (a :: l)) a0 <= 1)
  split; simpl.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
NoDupA eqA (a :: l) ->
forall a0 : A,
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eqA_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDupA eqA (a :: l)
  inversion_clear 1.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H0:~ InA eqA a l
H1:NoDupA eqA l
forall a0 : A,
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eqA_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDupA eqA (a :: l)
  rewrite IHl in H1.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H0:~ InA eqA a l
H1:forall a0 : A,
multiplicity (list_contents l) a0 <= 1
forall a0 : A,
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eqA_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDupA eqA (a :: l)
  intros; destruct (eqA_dec a a0) as [EQ|NEQ]; simpl; auto with *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a1 : A,
 multiplicity (list_contents l) a1 <= 1)
H0:~ InA eqA a l
H1:forall a1 : A,
multiplicity (list_contents l) a1 <= 1
a0:A
EQ:eqA a a0
S (multiplicity (list_contents l) a0) <= 1
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eqA_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDupA eqA (a :: l)
  rewrite <- EQ.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a1 : A,
 multiplicity (list_contents l) a1 <= 1)
H0:~ InA eqA a l
H1:forall a1 : A,
multiplicity (list_contents l) a1 <= 1
a0:A
EQ:eqA a a0
S (multiplicity (list_contents l) a) <= 1
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eqA_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDupA eqA (a :: l)
  rewrite multiplicity_InA_O; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
(forall a0 : A,
 (if eqA_dec a a0 then 1 else 0) +
 multiplicity (list_contents l) a0 <= 1) ->
NoDupA eqA (a :: l)
  intros; constructor.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
~ InA eqA a l
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDupA eqA l
  rewrite multiplicity_InA.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
~ 0 < multiplicity (list_contents l) a
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDupA eqA l
  specialize (H a).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:(if eqA_dec a a then 1 else 0) +
multiplicity (list_contents l) a <= 1
~ 0 < multiplicity (list_contents l) a
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDupA eqA l
  rewrite if_eqA_refl in H.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:1 + multiplicity (list_contents l) a <= 1
~ 0 < multiplicity (list_contents l) a
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDupA eqA l
  clear IHl; omega.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a0 : A,
 multiplicity (list_contents l) a0 <= 1)
H:forall a0 : A,
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
NoDupA eqA l
  rewrite IHl; intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a1 : A,
 multiplicity (list_contents l) a1 <= 1)
H:forall a1 : A,
(if eqA_dec a a1 then 1 else 0) +
multiplicity (list_contents l) a1 <= 1
a0:A
multiplicity (list_contents l) a0 <= 1
  specialize (H a0).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
IHl:NoDupA eqA l <->
(forall a1 : A,
 multiplicity (list_contents l) a1 <= 1)
a0:A
H:(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l) a0 <= 1
multiplicity (list_contents l) a0 <= 1 omega.
Qed.

Permutation is compatible with InA.

Lemma permut_InA_InA :
  forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l1 l2 : list A) (e : A),
permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l1 l2 : list A) (e : A),
permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2
  intros l1 l2 e.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l1, l2:list A
e:A
permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2
  do 2 rewrite multiplicity_InA.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l1, l2:list A
e:A
permutation l1 l2 ->
0 < multiplicity (list_contents l1) e ->
0 < multiplicity (list_contents l2) e
  unfold permutation, meq.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l1, l2:list A
e:A
(forall a : A,
 multiplicity (list_contents l1) a =
 multiplicity (list_contents l2) a) ->
0 < multiplicity (list_contents l1) e ->
0 < multiplicity (list_contents l2) e
  intros H;rewrite H; auto.
Qed.

Lemma permut_cons_InA :
  forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l1 l2 : list A) (e : A),
permutation (e :: l1) l2 -> InA eqA e l2
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (l1 l2 : list A) (e : A),
permutation (e :: l1) l2 -> InA eqA e l2
  intros; apply (permut_InA_InA (e:=e) H); auto with *.
Qed.

Permutation of an empty list.

Lemma permut_nil :
  forall l, permutation l [] -> l = [].A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A, permutation l [ ] -> l = [ ]
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A, permutation l [ ] -> l = [ ]
  intro l; destruct l as [ | e l ]; trivial.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
e:A
l:list A
permutation (e :: l) [ ] -> e :: l = [ ]
  assert (InA eqA e (e::l)) by (auto with *).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
e:A
l:list A
H:InA eqA e (e :: l)
permutation (e :: l) [ ] -> e :: l = [ ]
  intro Abs; generalize (permut_InA_InA Abs H).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
e:A
l:list A
H:InA eqA e (e :: l)
Abs:permutation (e :: l) [ ]
InA eqA e [ ] -> e :: l = [ ]
  inversion 1.
Qed.

Permutation for short lists.

Lemma permut_length_1:
  forall a b, permutation [a] [b] -> eqA a b.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall a b : A, permutation [a] [b] -> eqA a b
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall a b : A, permutation [a] [b] -> eqA a b
  intros a b; unfold permutation, meq.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a, b:A
(forall a0 : A,
 multiplicity (list_contents [a]) a0 =
 multiplicity (list_contents [b]) a0) -> eqA a b
  intro P; specialize (P b); simpl in *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a, b:A
P:(if eqA_dec a b then 1 else 0) + 0 =
(if eqA_dec b b then 1 else 0) + 0
eqA a b
  rewrite if_eqA_refl in *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a, b:A
P:(if eqA_dec a b then 1 else 0) + 0 = 1 + 0
eqA a b
  destruct (eqA_dec a b); simpl; auto; discriminate.
Qed.

Lemma permut_length_2 :
  forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] ->
    (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall a1 b1 a2 b2 : A,
permutation [a1; b1] [a2; b2] ->
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall a1 b1 a2 b2 : A,
permutation [a1; b1] [a2; b2] ->
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
  intros a1 b1 a2 b2 P.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
  assert (H:=permut_cons_InA P).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H:InA eqA a1 [a2; b2]
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
  inversion_clear H.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:eqA a1 a2
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:InA eqA a1 [b2]
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
  left; split; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:eqA a1 a2
eqA b1 b2
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:InA eqA a1 [b2]
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
  apply permut_length_1.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:eqA a1 a2
permutation [b1] [b2]
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:InA eqA a1 [b2]
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
  red; red; intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:eqA a1 a2
a:A
multiplicity (list_contents [b1]) a =
multiplicity (list_contents [b2]) a
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:InA eqA a1 [b2]
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
  specialize (P a).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2, a:A
P:multiplicity (list_contents [a1; b1]) a =
multiplicity (list_contents [a2; b2]) a
H0:eqA a1 a2
multiplicity (list_contents [b1]) a =
multiplicity (list_contents [b2]) a
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:InA eqA a1 [b2]
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1 simpl in *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2, a:A
P:(if eqA_dec a1 a then 1 else 0) +
((if eqA_dec b1 a then 1 else 0) + 0) =
(if eqA_dec a2 a then 1 else 0) +
((if eqA_dec b2 a then 1 else 0) + 0)
H0:eqA a1 a2
(if eqA_dec b1 a then 1 else 0) + 0 =
(if eqA_dec b2 a then 1 else 0) + 0
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:InA eqA a1 [b2]
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
  rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2, a:A
P:(if eqA_dec a2 a then 1 else 0) +
((if eqA_dec b1 a then 1 else 0) + 0) =
(if eqA_dec a2 a then 1 else 0) +
((if eqA_dec b2 a then 1 else 0) + 0)
H0:eqA a1 a2
(if eqA_dec b1 a then 1 else 0) + 0 =
(if eqA_dec b2 a then 1 else 0) + 0
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:InA eqA a1 [b2]
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1 omega.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:InA eqA a1 [b2]
eqA a1 a2 /\ eqA b1 b2 \/ eqA a1 b2 /\ eqA a2 b1
  right.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H0:InA eqA a1 [b2]
eqA a1 b2 /\ eqA a2 b1
  inversion_clear H0; [|inversion H].A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H:eqA a1 b2
eqA a1 b2 /\ eqA a2 b1
  split; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H:eqA a1 b2
eqA a2 b1
  apply permut_length_1.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H:eqA a1 b2
permutation [a2] [b1]
  red; red; intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2:A
P:permutation [a1; b1] [a2; b2]
H:eqA a1 b2
a:A
multiplicity (list_contents [a2]) a =
multiplicity (list_contents [b1]) a
  specialize (P a); simpl in *.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2, a:A
P:(if eqA_dec a1 a then 1 else 0) +
((if eqA_dec b1 a then 1 else 0) + 0) =
(if eqA_dec a2 a then 1 else 0) +
((if eqA_dec b2 a then 1 else 0) + 0)
H:eqA a1 b2
(if eqA_dec a2 a then 1 else 0) + 0 =
(if eqA_dec b1 a then 1 else 0) + 0
  rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a1, b1, a2, b2, a:A
P:(if eqA_dec b2 a then 1 else 0) +
((if eqA_dec b1 a then 1 else 0) + 0) =
(if eqA_dec a2 a then 1 else 0) +
((if eqA_dec b2 a then 1 else 0) + 0)
H:eqA a1 b2
(if eqA_dec a2 a then 1 else 0) + 0 =
(if eqA_dec b1 a then 1 else 0) + 0 omega.
Qed.

Permutation is compatible with length.

Lemma permut_length :
  forall l1 l2, permutation l1 l2 -> length l1 = length l2.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l1 l2 : list A,
permutation l1 l2 -> length l1 = length l2
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l1 l2 : list A,
permutation l1 l2 -> length l1 = length l2
  induction l1; intros l2 H.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l2:list A
H:permutation [ ] l2
length [ ] = length l2
A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
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
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
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
  assert (H0:=permut_cons_InA H).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
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
H0:InA eqA a l2
length (a :: l1) = length l2
  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
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
H0:InA eqA a l2
h2:list A
b:A
t2:list A
H1:eqA a b
H2:l2 = h2 ++ b :: t2
length (a :: l1) = length l2
  subst l2.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
H:permutation (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
length (a :: l1) = length (h2 ++ b :: t2)
  rewrite app_length.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
H:permutation (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
length (a :: l1) = length h2 + length (b :: t2)
  simpl; rewrite <- plus_n_Sm; f_equal.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
H:permutation (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
length l1 = length h2 + length t2
  rewrite <- app_length.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
H:permutation (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
length l1 = length (h2 ++ t2)
  apply IHl1.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
H:permutation (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation l1 (h2 ++ t2)
  apply permut_remove_hd with b.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
H:permutation (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation (b :: l1) (h2 ++ b :: t2)
  apply permut_trans with (a::l1); auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
H:permutation (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation (b :: l1) (a :: l1)
  revert H1; unfold permutation, meq; simpl.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
H:permutation (a :: l1) (h2 ++ b :: t2)
eqA a b ->
forall a0 : A,
(if eqA_dec b a0 then 1 else 0) +
multiplicity (list_contents l1) a0 =
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents l1) a0
  intros; f_equal; auto.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l1:list A
IHl1:forall l2 : list A,
permutation l1 l2 -> length l1 = length l2
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
H:permutation (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
a0:A
(if eqA_dec b a0 then 1 else 0) =
(if eqA_dec a a0 then 1 else 0)
  rewrite (@if_eqA_rewrite_l a b a0); auto.
Qed.

Lemma NoDupA_equivlistA_permut :
  forall l l', NoDupA eqA l -> NoDupA eqA l' ->
    equivlistA eqA l l' -> permutation l l'.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l l' : list A,
NoDupA eqA l ->
NoDupA eqA l' ->
equivlistA eqA l l' -> permutation l l'
Proof.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l l' : list A,
NoDupA eqA l ->
NoDupA eqA l' ->
equivlistA eqA l l' -> permutation l l'
  intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l':list A
H:NoDupA eqA l
H0:NoDupA eqA l'
H1:equivlistA eqA l l'
permutation l l'
  red; unfold meq; intros.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l':list A
H:NoDupA eqA l
H0:NoDupA eqA l'
H1:equivlistA eqA l l'
a:A
multiplicity (list_contents l) a =
multiplicity (list_contents l') a
  rewrite multiplicity_NoDupA in H, H0.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
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:equivlistA eqA l 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
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l, l':list A
a:A
multiplicity (list_contents l) a <= 1 ->
multiplicity (list_contents l') a <= 1 ->
InA eqA a l <-> InA eqA a l' ->
multiplicity (list_contents l) a =
multiplicity (list_contents l') a
  do 2 rewrite multiplicity_InA.A:Type
eqA:relation A
eqA_equiv:Equivalence eqA
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
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.

End Permut.

Section Permut_map.

Variables A B : Type.

Variable eqA : relation A.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
Hypothesis eqA_equiv : Equivalence eqA.

Variable eqB : B->B->Prop.
Hypothesis eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
Hypothesis eqB_trans : Transitive eqB.

Permutation is compatible with map.

Lemma permut_map :
  forall f,
    (Proper (eqA==>eqB) f) ->
    forall l1 l2, permutation _ eqA_dec l1 l2 ->
      permutation _ eqB_dec (map f l1) (map f l2).A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
forall f : A -> B,
Proper (eqA ==> eqB) f ->
forall l1 l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
Proof.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
forall f : A -> B,
Proper (eqA ==> eqB) f ->
forall l1 l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
  intros f; induction l1.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
forall l2 : list A,
permutation eqA eqA_dec [ ] l2 ->
permutation eqB eqB_dec (map f [ ]) (map f l2)
A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
forall l2 : list A,
permutation eqA eqA_dec (a :: l1) l2 ->
permutation eqB eqB_dec (map f (a :: l1)) (map f l2)
  intros l2 P; rewrite (permut_nil eqA_equiv (permut_sym P)); apply permut_refl.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
forall l2 : list A,
permutation eqA eqA_dec (a :: l1) l2 ->
permutation eqB eqB_dec (map f (a :: l1)) (map f l2)
  intros l2 P.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l0 : list A,
permutation eqA eqA_dec l1 l0 ->
permutation eqB eqB_dec (map f l1) (map f l0)
l2:list A
P:permutation eqA eqA_dec (a :: l1) l2
permutation eqB eqB_dec (map f (a :: l1)) (map f l2)
  simpl.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l0 : list A,
permutation eqA eqA_dec l1 l0 ->
permutation eqB eqB_dec (map f l1) (map f l0)
l2:list A
P:permutation eqA eqA_dec (a :: l1) l2
permutation eqB eqB_dec (f a :: map f l1) (map f l2)
  assert (H0:=permut_cons_InA eqA_equiv P).A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l0 : list A,
permutation eqA eqA_dec l1 l0 ->
permutation eqB eqB_dec (map f l1) (map f l0)
l2:list A
P:permutation eqA eqA_dec (a :: l1) l2
H0:InA eqA a l2
permutation eqB eqB_dec (f a :: map f l1) (map f l2)
  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l0 : list A,
permutation eqA eqA_dec l1 l0 ->
permutation eqB eqB_dec (map f l1) (map f l0)
l2:list A
P:permutation eqA eqA_dec (a :: l1) l2
H0:InA eqA a l2
h2:list A
b:A
t2:list A
H1:eqA a b
H2:l2 = h2 ++ b :: t2
permutation eqB eqB_dec (f a :: map f l1) (map f l2)
  subst l2.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec (f a :: map f l1)
  (map f (h2 ++ b :: t2))
  rewrite map_app.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec (f a :: map f l1)
  (map f h2 ++ map f (b :: t2))
  simpl.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec (f a :: map f l1)
  (map f h2 ++ f b :: map f t2)
  apply permut_trans with (f b :: map f l1).A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec (f a :: map f l1)
  (f b :: map f l1)
A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec 
  (f b :: map f l1) (map f h2 ++ f b :: map f t2)
  revert H1; unfold permutation, meq; simpl.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
eqA a b ->
forall a0 : B,
(if eqB_dec (f a) a0 then 1 else 0) +
multiplicity (list_contents eqB eqB_dec (map f l1)) a0 =
(if eqB_dec (f b) a0 then 1 else 0) +
multiplicity (list_contents eqB eqB_dec (map f l1)) a0
A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec 
  (f b :: map f l1) (map f h2 ++ f b :: map f t2)
  intros; f_equal; auto.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
a0:B
(if eqB_dec (f a) a0 then 1 else 0) =
(if eqB_dec (f b) a0 then 1 else 0)
A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec 
  (f b :: map f l1) (map f h2 ++ f b :: map f t2)
  destruct (eqB_dec (f b) a0) as [H2|H2];
    destruct (eqB_dec (f a) a0) as [H3|H3]; auto.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
a0:B
H2:eqB (f b) a0
H3:~ eqB (f a) a0
0 = 1
A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
a0:B
H2:~ eqB (f b) a0
H3:eqB (f a) a0
1 = 0
A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec 
  (f b :: map f l1) (map f h2 ++ f b :: map f t2)
  destruct H3; transitivity (f b); auto with *.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
a0:B
H2:~ eqB (f b) a0
H3:eqB (f a) a0
1 = 0
A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec 
  (f b :: map f l1) (map f h2 ++ f b :: map f t2)
  destruct H2; transitivity (f a); auto with *.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec (f b :: map f l1)
  (map f h2 ++ f b :: map f t2)
  apply permut_add_cons_inside.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec (map f l1)
  (map f h2 ++ map f t2)
  rewrite <- map_app.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqB eqB_dec (map f l1) (map f (h2 ++ t2))
  apply IHl1; auto.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqA eqA_dec l1 (h2 ++ t2)
  apply permut_remove_hd with b; trivial.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqA eqA_dec (b :: l1) (h2 ++ b :: t2)
  apply permut_trans with (a::l1); auto.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
permutation eqA eqA_dec (b :: l1) (a :: l1)
  revert H1; unfold permutation, meq; simpl.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
eqA a b ->
forall a0 : A,
(if eqA_dec b a0 then 1 else 0) +
multiplicity (list_contents eqA eqA_dec l1) a0 =
(if eqA_dec a a0 then 1 else 0) +
multiplicity (list_contents eqA eqA_dec l1) a0
  intros; f_equal; auto.A, B:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
eqB:B -> B -> Prop
eqB_dec:forall x y : B, {eqB x y} + {~ eqB x y}
eqB_trans:Transitive eqB
f:A -> B
H:Proper (eqA ==> eqB) f
a:A
l1:list A
IHl1:forall l2 : list A,
permutation eqA eqA_dec l1 l2 ->
permutation eqB eqB_dec (map f l1) (map f l2)
h2:list A
b:A
t2:list A
H0:InA eqA a (h2 ++ b :: t2)
P:permutation eqA eqA_dec (a :: l1) (h2 ++ b :: t2)
H1:eqA a b
a0:A
(if eqA_dec b a0 then 1 else 0) =
(if eqA_dec a a0 then 1 else 0)
  rewrite (@if_eqA_rewrite_l _ _ eqA_equiv eqA_dec a b a0); auto.
Qed.

End Permut_map.

Require Import Permutation.

Section Permut_permut.

Variable A : Type.

Variable eqA : relation A.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
Hypothesis eqA_equiv : Equivalence eqA.

Lemma Permutation_impl_permutation : forall l l',
  Permutation l l' -> permutation _ eqA_dec l l'.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
forall l l' : list A,
Permutation l l' -> permutation eqA eqA_dec l l'
Proof.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
forall l l' : list A,
Permutation l l' -> permutation eqA eqA_dec l l'
  induction 1.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
permutation eqA eqA_dec [ ] [ ]
A:Type
eqA:relation A
eqA_dec:forall x0 y : A, {eqA x0 y} + {~ eqA x0 y}
eqA_equiv:Equivalence eqA
x:A
l, l':list A
H:Permutation l l'
IHPermutation:permutation eqA eqA_dec l l'
permutation eqA eqA_dec (x :: l) (x :: l')
A:Type
eqA:relation A
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
eqA_equiv:Equivalence eqA
x, y:A
l:list A
permutation eqA eqA_dec (y :: x :: l) (x :: y :: l)
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:permutation eqA eqA_dec l l'
IHPermutation2:permutation eqA eqA_dec l' l''
permutation eqA eqA_dec l l''
    apply permut_refl.A:Type
eqA:relation A
eqA_dec:forall x0 y : A, {eqA x0 y} + {~ eqA x0 y}
eqA_equiv:Equivalence eqA
x:A
l, l':list A
H:Permutation l l'
IHPermutation:permutation eqA eqA_dec l l'
permutation eqA eqA_dec (x :: l) (x :: l')
A:Type
eqA:relation A
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
eqA_equiv:Equivalence eqA
x, y:A
l:list A
permutation eqA eqA_dec (y :: x :: l) (x :: y :: l)
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:permutation eqA eqA_dec l l'
IHPermutation2:permutation eqA eqA_dec l' l''
permutation eqA eqA_dec l l''
    apply permut_cons; auto using Equivalence_Reflexive.A:Type
eqA:relation A
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
eqA_equiv:Equivalence eqA
x, y:A
l:list A
permutation eqA eqA_dec (y :: x :: l) (x :: y :: l)
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:permutation eqA eqA_dec l l'
IHPermutation2:permutation eqA eqA_dec l' l''
permutation eqA eqA_dec l l''
    change (x :: y :: l) with ([x] ++ y :: l);
      apply permut_add_cons_inside; simpl;
      apply permut_cons_eq; auto using Equivalence_Reflexive, permut_refl.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:permutation eqA eqA_dec l l'
IHPermutation2:permutation eqA eqA_dec l' l''
permutation eqA eqA_dec l l''
    apply permut_trans with l'; trivial.
Qed.

Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
forall l l' : list A,
Forall2 eqA l l' -> permutation eqA eqA_dec l l'
Proof.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
forall l l' : list A,
Forall2 eqA l l' -> permutation eqA eqA_dec l l'
  induction 1.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
permutation eqA eqA_dec [ ] [ ]
A:Type
eqA:relation A
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
eqA_equiv:Equivalence eqA
x, y:A
l, l':list A
H:eqA x y
H0:Forall2 eqA l l'
IHForall2:permutation eqA eqA_dec l l'
permutation eqA eqA_dec (x :: l) (y :: l')
    apply permut_refl.A:Type
eqA:relation A
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
eqA_equiv:Equivalence eqA
x, y:A
l, l':list A
H:eqA x y
H0:Forall2 eqA l l'
IHForall2:permutation eqA eqA_dec l l'
permutation eqA eqA_dec (x :: l) (y :: l')
    apply permut_cons_eq; trivial.
Qed.

Lemma permutation_Permutation : forall l l',
  permutation _ eqA_dec l l' <->
  exists l'', Permutation l l'' /\ Forall2 eqA l'' l'.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
forall l l' : list A,
permutation eqA eqA_dec l l' <->
(exists l'' : list A,
   Permutation l l'' /\ Forall2 eqA l'' l')
Proof.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
forall l l' : list A,
permutation eqA eqA_dec l l' <->
(exists l'' : list A,
   Permutation l l'' /\ Forall2 eqA l'' l')
  split; intro H.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:permutation eqA eqA_dec l l'
exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
  (* -> *)
  induction l in l', H |- *.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l':list A
H:permutation eqA eqA_dec [ ] l'
exists l'' : list A,
  Permutation [ ] l'' /\ Forall2 eqA l'' l'
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
a:A
l, l':list A
H:permutation eqA eqA_dec (a :: l) l'
IHl:forall l'0 : list A,
permutation eqA eqA_dec l l'0 ->
exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'0
exists l'' : list A,
  Permutation (a :: l) l'' /\ Forall2 eqA l'' l'
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
    exists []; apply permut_sym, permut_nil in H as ->; auto using Forall2.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
a:A
l, l':list A
H:permutation eqA eqA_dec (a :: l) l'
IHl:forall l'0 : list A,
permutation eqA eqA_dec l l'0 ->
exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'0
exists l'' : list A,
  Permutation (a :: l) l'' /\ Forall2 eqA l'' l'
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
    pose proof H as H'.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
a:A
l, l':list A
H:permutation eqA eqA_dec (a :: l) l'
IHl:forall l'0 : list A,
permutation eqA eqA_dec l l'0 ->
exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'0
H':permutation eqA eqA_dec (a :: l) l'
exists l'' : list A,
  Permutation (a :: l) l'' /\ Forall2 eqA l'' l'
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
    apply permut_cons_InA, InA_split in H
      as (l1 & y & l2 & Heq & ->); trivial.A:Type
eqA:relation A
eqA_dec:forall x y0 : A, {eqA x y0} + {~ eqA x y0}
eqA_equiv:Equivalence eqA
a:A
l, l1:list A
y:A
l2:list A
Heq:eqA a y
IHl:forall l' : list A,
permutation eqA eqA_dec l l' ->
exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
H':permutation eqA eqA_dec (a :: l) (l1 ++ y :: l2)
exists l'' : list A,
  Permutation (a :: l) l'' /\
  Forall2 eqA l'' (l1 ++ y :: l2)
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
    apply permut_remove_hd_eq, IHl in H'
      as (l'' & IHP & IHA); clear IHl; trivial.A:Type
eqA:relation A
eqA_dec:forall x y0 : A, {eqA x y0} + {~ eqA x y0}
eqA_equiv:Equivalence eqA
a:A
l, l1:list A
y:A
l2:list A
Heq:eqA a y
l'':list A
IHP:Permutation l l''
IHA:Forall2 eqA l'' (l1 ++ l2)
exists l''0 : list A,
  Permutation (a :: l) l''0 /\
  Forall2 eqA l''0 (l1 ++ y :: l2)
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
    apply Forall2_app_inv_r in IHA as (l1'' & l2'' & Hl1 & Hl2 & ->).A:Type
eqA:relation A
eqA_dec:forall x y0 : A, {eqA x y0} + {~ eqA x y0}
eqA_equiv:Equivalence eqA
a:A
l, l1:list A
y:A
l2:list A
Heq:eqA a y
l1'', l2'':list A
IHP:Permutation l (l1'' ++ l2'')
Hl1:Forall2 eqA l1'' l1
Hl2:Forall2 eqA l2'' l2
exists l'' : list A,
  Permutation (a :: l) l'' /\
  Forall2 eqA l'' (l1 ++ y :: l2)
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
    exists (l1'' ++ a :: l2''); split.A:Type
eqA:relation A
eqA_dec:forall x y0 : A, {eqA x y0} + {~ eqA x y0}
eqA_equiv:Equivalence eqA
a:A
l, l1:list A
y:A
l2:list A
Heq:eqA a y
l1'', l2'':list A
IHP:Permutation l (l1'' ++ l2'')
Hl1:Forall2 eqA l1'' l1
Hl2:Forall2 eqA l2'' l2
Permutation (a :: l) (l1'' ++ a :: l2'')
A:Type
eqA:relation A
eqA_dec:forall x y0 : A, {eqA x y0} + {~ eqA x y0}
eqA_equiv:Equivalence eqA
a:A
l, l1:list A
y:A
l2:list A
Heq:eqA a y
l1'', l2'':list A
IHP:Permutation l (l1'' ++ l2'')
Hl1:Forall2 eqA l1'' l1
Hl2:Forall2 eqA l2'' l2
Forall2 eqA (l1'' ++ a :: l2'') (l1 ++ y :: l2)
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
      apply Permutation_cons_app; trivial.A:Type
eqA:relation A
eqA_dec:forall x y0 : A, {eqA x y0} + {~ eqA x y0}
eqA_equiv:Equivalence eqA
a:A
l, l1:list A
y:A
l2:list A
Heq:eqA a y
l1'', l2'':list A
IHP:Permutation l (l1'' ++ l2'')
Hl1:Forall2 eqA l1'' l1
Hl2:Forall2 eqA l2'' l2
Forall2 eqA (l1'' ++ a :: l2'') (l1 ++ y :: l2)
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
      apply Forall2_app, Forall2_cons; trivial.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l':list A
H:exists l'' : list A,
  Permutation l l'' /\ Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
  (* <- *)
  destruct H as (l'' & H & Heq).A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l', l'':list A
H:Permutation l l''
Heq:Forall2 eqA l'' l'
permutation eqA eqA_dec l l'
  apply permut_trans with l''.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l', l'':list A
H:Permutation l l''
Heq:Forall2 eqA l'' l'
permutation eqA eqA_dec l l''
A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l', l'':list A
H:Permutation l l''
Heq:Forall2 eqA l'' l'
permutation eqA eqA_dec l'' l'
    apply Permutation_impl_permutation; trivial.A:Type
eqA:relation A
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
eqA_equiv:Equivalence eqA
l, l', l'':list A
H:Permutation l l''
Heq:Forall2 eqA l'' l'
permutation eqA eqA_dec l'' l'
    apply permut_eqA; trivial.
Qed.

End Permut_permut.

(* begin hide *)

For compatibility

Notation permut_right := permut_cons (only parsing).
Notation permut_tran := permut_trans (only parsing).
(* end hide *)