Equivalence between two definitions of permutations of lists

There are (at least) two ways of defining permutations between lists:

Comparing the numbter of occurrences of items in both lists (see Coq.Sorting.Permutation in Standard Library )

Using an inductive definition (quoted from the Reference Manual)

Inductive permI  :list A ->list A ->Prop:=
|permI_refl:forall l, permI l l
|permI_cons:forall a l0 l1, permI l0 l1-> permI (a::l0)(a::l1)
|permI_app:forall a l, permI (a::l) (l++(a::nil))
|permI_trans:forall l1 l2 l3,
              permI l1 l2 -> permI l2 l3 -> permI l1 l3.

Show that both definitions are logically equivalent.
Use this equivalence to prove easily the following fact:

Lemma counterexample : ~ permI (2::3::5::5::8::7::4::nil) 
                               (3::2::8::7::4::3::5::nil).

Solution

This file
Look also at the following exercises on permutations : this one and this one .

Going home

Exercise proposed by Houda Anoun