Library Coq.Lists.SetoidPermutation

Require Import Permutation SetoidList.

Set Implicit Arguments.

Local Ltac Tauto.intuition_solver ::= auto with relations.

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 : core.

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.