On permutations
Define the following relationships on (list A):
- The list l' is obtained from l by transposing two consecutive
items.
- The list l' is obtained from l by a finite number of such transpositions. We say that l' is a permutation of l.
Show that the second one is an equivalence relation.
Solution
Look at this file
Notes
You could also define directly the relation perm as
the reflexive-rtransitive closure of transpose. In this case, you first have to load the module Operators_Properties of the library Relations.
See also the development in this file , that contains some lemmas on permutations.
Additionnally, it uses the library Relation_Classes.
Follow this link