Stream: Coq users

Topic: How to use `Permutation` type?


view this post on Zulip 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?

view this post on Zulip 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 [2])
     : Permutation [1; 2; 3] [3; 1; 2]

view this post on Zulip Julin S (Mar 06 2022 at 07:28):

Oh.. Okay.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 06 2022 at 07:54):

The apply, constructor and econstructor tactics can help.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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 ([1] ++ [2]) ([2] ++ [1]).
  aac_reflexivity.
Qed.

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

view this post on Zulip 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.

view this post on Zulip 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 ([1] ++ l) (l ++ [1]).
  aac_reflexivity.
Qed.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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 l1and 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. (* ... *)

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC