Equivalence between two definitions of permutations of lists
There are (at least) two ways of defining permutations between lists:
Show that both definitions are logically equivalent.
- 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)
Look also at the following exercises on permutations :
and this one .
Exercise proposed by Houda Anoun