- 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.

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).

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

Going home

Exercise proposed by Houda Anoun