Library Coq.Lists.SetoidPermutation
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₂.
Lemma Permutation_eqlistA_commute l₁ l₂ l₃ :
eqlistA eqA l₁ l₂ -> Permutation l₂ l₃ ->
exists l₂', Permutation l₁ l₂' /\ eqlistA eqA l₂' l₃.
Lemma PermutationA_decompose l₁ l₂ :
PermutationA l₁ l₂ ->
exists l, Permutation l₁ l /\ eqlistA eqA l l₂.
Lemma Permutation_PermutationA l₁ l₂ :
Permutation l₁ l₂ -> PermutationA l₁ l₂.
Lemma eqlistA_PermutationA l₁ l₂ :
eqlistA eqA l₁ l₂ -> PermutationA l₁ l₂.
Lemma NoDupA_equivlistA_decompose l1 l2 :
NoDupA eqA l1 -> NoDupA eqA l2 -> equivlistA eqA l1 l2 ->
exists l, Permutation l1 l /\ eqlistA eqA l l2.
Lemma PermutationA_preserves_NoDupA l₁ l₂ :
PermutationA l₁ l₂ -> NoDupA eqA l₁ -> NoDupA eqA l₂.
End Permutation.