## Stream: Coq users

### Topic: How to use `Permutation` type?

#### Julin S (Mar 06 2022 at 05:54):

I recently came across `Permutation` in the coq standard library at https://coq.inria.fr/library/Coq.Sorting.Permutation.html

The definition of the type is:

``````Inductive Permutation : list A -> list A -> Prop :=
| perm_nil: Permutation [] []
| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
| perm_swap x y l : Permutation (y::x::l) (x::y::l)
| perm_trans l l' l'' :
Permutation l l' -> Permutation l' l'' -> Permutation l l''.
``````

Does that mean that `Permutation [1;2] [2;1]` signfies that `[1;2]` and `[2;1]` are permutations of each other?

But when I tried

``````Compute Permutation [1;2] [2;1;3].
(*
= Permutation [1; 2] [2; 1; 3]
: Prop
*)
``````

it went without error even though `[1;2]` and `[2;1;3]` are of different lengths.

How is `Permutation` meant to be used?

#### Pierre Castéran (Mar 06 2022 at 06:15):

Your test just shows that `Permutation [1; 2] [2; 1; 3]` is a well-formed proposition, like `2 = 3`.
This is different from being provable. An interesting exercise is to prove `Permutation [1;2;3] [3;1;2]` and `~ Permutation [1; 2] [2; 1; 3]` using Coq's definition and/or lemmas from the library.

For instance, the following term (obtained through an interactive proof) has type `Permutation [1;2;3] [3;1;2]` , which in turn has type `Prop` ...

``````Print  p123.
= perm_trans (perm_skip 1 (perm_swap 3 2 [])) (perm_swap 3 1 )
: Permutation [1; 2; 3] [3; 1; 2]
``````

Oh.. Okay.

#### Julin S (Mar 06 2022 at 07:31):

I understood how `p123` works out.

Something like

``````1)    2 3 |   3 2  (perm_swap)
2)  1 2 3 | 1 3 2  (perm_skip 1)
3)  1 3 2 | 3 1 2  (perm_swap)
4)  1 2 3 | 3 1 2  (perm_trans 2,3)
``````

right?

But how do we prove it in the proof mode?

I got only as far stating it..

``````Lemma p123 : Permutation [1;2;3] [3;1;2].
Proof.
``````

#### Paolo Giarrusso (Mar 06 2022 at 07:54):

The apply, constructor and econstructor tactics can help.

#### Paolo Giarrusso (Mar 06 2022 at 07:58):

But if you haven't seen them before, you might benefit from learning about them on a simpler example...

#### Paolo Giarrusso (Mar 06 2022 at 08:02):

For instance, https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html covers this topic on other examples.

#### Karl Palmskog (Mar 06 2022 at 10:05):

I really wouldn't recommend doing proofs of permutation for lists with many elements using lemmas like `perm_swap`, `perm_skip`, etc. Better to use something like AAC Tactics for that: https://github.com/coq-community/aac-tactics

One can do stuff like this, assuming there are no `cons`/`::`:

``````Goal Permutation ( ++ ) ( ++ ).
aac_reflexivity.
Qed.
``````

In purely abstract proofs, `perm_swap` and friends could still be useful, though.

#### Paolo Giarrusso (Mar 06 2022 at 10:24):

I agree you want to automate this, and on concrete goals I'd probably just use some library to exploit decidability (sorting the lists takes O(n log n))...

But that doesn't seem the immediate suggestion if somebody is still learning about inductive propositions.

#### Karl Palmskog (Mar 06 2022 at 10:28):

I agree that learning about inductives fully first is a good idea, it's just that I've seen beginners kill themselves to prove arithmetic and list goals that can be solved by a single tactic.

If you're fully concrete, then sure, just decide and get it done, but with some automation you can also handle the half-abstract ones:

``````Lemma myperm l : Permutation ( ++ l) (l ++ ).
aac_reflexivity.
Qed.
``````

#### Enrico Tassi (Mar 06 2022 at 11:13):

@Julin S if you prefer computational definitions you can have a look at
https://math-comp.github.io/htmldoc/mathcomp.ssreflect.seq.html#PermSeq
Here an example:

``````From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import eqtype ssrnat seq.

Goal perm_eq [:: 1 ; 2 ] [:: 2 ; 1].
Proof.
reflexivity.
Qed.
``````

#### Karl Palmskog (Mar 06 2022 at 11:16):

but the caveat with `perm_eq` is that the element type must have decidable equality (pretty common that this holds, though)

#### Pierre Castéran (Mar 06 2022 at 12:21):

Btw, Coq's Definition of `Permutation` may make difficult the search of an interactive proof of `Permutation l1 l2` where `l1`and `l2` are given lists (because of the fourth constructor and its variable `l'`, associated with a list of the same length as `l` and `l''`).
I like the "Prolog-like" definition.

``````Inductive Remove {A} : list A -> A -> list A -> Prop:=
remove_hd : forall a l, Remove (a::l) a l
| remove_tl : forall a b l l', Remove l b l' -> Remove (a::l) b (a::l').

Inductive PPerm {A} : list A -> list A -> Prop :=
pperm_nil : PPerm nil nil
| pperm_skip: forall a l l', PPerm l l' -> PPerm(a::l) (a::l')
| pperm_swap : forall a b l l' l'', Remove l b l' -> PPerm (a::l') l'' ->  PPerm (a::l) (b::l'').
``````

You may also solve goals like:

``````Lemma p123X : {l' | PPerm [1;2;3] l'}.
eexists. (* ... *)
``````

#### Cyril Cohen (Mar 08 2022 at 12:25):

Karl Palmskog said:

but the caveat with `perm_eq` is that the element type must have decidable equality (pretty common that this holds, though)

Indeed, but you can always bring yourself back to natural numbers using `perm_map`

Last updated: Sep 23 2023 at 13:01 UTC