Library Coq.Lists.SetoidPermutation
Require
Import
SetoidList
.
Set Implicit Arguments
.
Permutations of list modulo a setoid equality.
Contribution by Robbert Krebbers (Nijmegen University).
Section
Permutation
.
Context
{
A
:
Type
} (
eqA
:
relation
A
) (
e
:
Equivalence
eqA
).
Inductive
PermutationA
:
list
A
->
list
A
->
Prop
:=
|
permA_nil
:
PermutationA
nil
nil
|
permA_skip
x₁
x₂
l₁
l₂
:
eqA
x₁
x₂
->
PermutationA
l₁
l₂
->
PermutationA
(
x₁
::
l₁
) (
x₂
::
l₂
)
|
permA_swap
x
y
l
:
PermutationA
(
y
::
x
::
l
) (
x
::
y
::
l
)
|
permA_trans
l₁
l₂
l₃
:
PermutationA
l₁
l₂
->
PermutationA
l₂
l₃
->
PermutationA
l₁
l₃
.
Local
Hint Constructors
PermutationA
.
Global Instance
:
Equivalence
PermutationA
.
Global Instance
PermutationA_cons
:
Proper
(
eqA
==>
PermutationA
==>
PermutationA
) (@
cons
A
).
Lemma
PermutationA_app_head
l₁
l₂
l
:
PermutationA
l₁
l₂
->
PermutationA
(
l
++
l₁
) (
l
++
l₂
).
Global Instance
PermutationA_app
:
Proper
(
PermutationA
==>
PermutationA
==>
PermutationA
) (@
app
A
).
Lemma
PermutationA_app_tail
l₁
l₂
l
:
PermutationA
l₁
l₂
->
PermutationA
(
l₁
++
l
) (
l₂
++
l
).
Lemma
PermutationA_cons_append
l
x
:
PermutationA
(
x
::
l
) (
l
++
x
::
nil
).
Lemma
PermutationA_app_comm
l₁
l₂
:
PermutationA
(
l₁
++
l₂
) (
l₂
++
l₁
).
Lemma
PermutationA_cons_app
l
l₁
l₂
x
:
PermutationA
l
(
l₁
++
l₂
) ->
PermutationA
(
x
::
l
) (
l₁
++
x
::
l₂
).
Lemma
PermutationA_middle
l₁
l₂
x
:
PermutationA
(
x
::
l₁
++
l₂
) (
l₁
++
x
::
l₂
).
Lemma
PermutationA_equivlistA
l₁
l₂
:
PermutationA
l₁
l₂
->
equivlistA
eqA
l₁
l₂
.
Lemma
NoDupA_equivlistA_PermutationA
l₁
l₂
:
NoDupA
eqA
l₁
->
NoDupA
eqA
l₂
->
equivlistA
eqA
l₁
l₂
->
PermutationA
l₁
l₂
.
End
Permutation
.