Julin S (Mar 06 2022 at 05:54): 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 [2])
: 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.
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 ([1] ++ [2]) ([2] ++ [1]).
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 ([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)
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. (* ... *)
Karl Palmskog said:
but the caveat with
perm_eqis 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