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