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?

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 [2])
: Permutation [1; 2; 3] [3; 1; 2]
```

Oh.. Okay.

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

The apply, constructor and econstructor tactics can help.

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

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

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 ([1] ++ [2]) ([2] ++ [1]).
aac_reflexivity.
Qed.
```

In purely abstract proofs, `perm_swap`

and friends could still be useful, though.

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.

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 ([1] ++ l) (l ++ [1]).
aac_reflexivity.
Qed.
```

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

but the caveat with `perm_eq`

is that the element type must have decidable equality (pretty common that this holds, though)

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. (* ... *)
```

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: Jan 29 2023 at 01:02 UTC