CoRN.util.SetoidPermutation
The standard Permutation property is not setoid-aware, so we
introduce a variant that is.
Section def.
Context {A: Type} (e: relation A) `{!Equivalence e}.
Inductive SetoidPermutation: list A → list A → Prop :=
| s_perm_nil : SetoidPermutation nil nil
| s_perm_skip x y: e x y → ∀ l l', SetoidPermutation l l' → SetoidPermutation (x :: l) (y :: l')
| s_perm_swap x y l: SetoidPermutation (y :: x :: l) (x :: y :: l)
| s_perm_trans l l' l'': SetoidPermutation l l' → SetoidPermutation l' l'' → SetoidPermutation l l''.
Hint Constructors SetoidPermutation.
Global Instance: Equivalence SetoidPermutation.
Proof with eauto; intuition.
constructor...
intro l.
induction l...
intros x y H.
induction H...
Qed.
Global Instance: Proper (list_eq e ==> list_eq e ==> iff) SetoidPermutation.
Proof with eauto.
assert (∀ a b, list_eq e a b → SetoidPermutation a b).
intros ?? E. apply (@list_eq_rect _ e SetoidPermutation); auto.
intros ?? E ?? F.
split; intro.
symmetry in E...
symmetry in F...
Qed.
End def.
Hint Constructors SetoidPermutation Permutation.
Lemma SetoidPermutation_stronger {A} (R U: relation A):
(∀ x y: A, R x y → U x y) →
∀ a b, SetoidPermutation R a b → SetoidPermutation U a b.
Proof. intros ??? P. induction P; eauto. Qed.
With eq for the element relation, SetoidPermutation is directly equivalent to Permutation:
Lemma SetoidPermutation_eq {A} (a b: list A): SetoidPermutation eq a b ↔ Permutation a b.
Proof. split; intro; induction H; eauto. subst; eauto. Qed.
And since eq is stronger than any other equivalence, SetoidPermutation always follows from Permutation:
Lemma SetoidPermutation_from_Permutation {A} (e: relation A) `{!Reflexive e} (a b: list A):
Permutation a b → SetoidPermutation e a b.
Proof.
intro.
apply SetoidPermutation_stronger with eq.
intros. subst. reflexivity.
apply SetoidPermutation_eq.
assumption.
Qed.
In general, SetoidPermutation is equivalent to Permutation modulo setoid list equivalence:
Lemma SetoidPermutation_meaning {A} (R: relation A) `{!Equivalence R} (x y: list A):
SetoidPermutation R x y ↔ ∃ y', list_eq R x y' ∧ Permutation y y'.
Proof with auto.
split.
intro H. induction H.
∃ nil. intuition.
destruct IHSetoidPermutation as [?[??]].
∃ (y :: x0).
repeat split...
∃ (y :: x :: l).
split... reflexivity.
destruct IHSetoidPermutation1 as [x [H1 H3]].
destruct IHSetoidPermutation2 as [x0 [H2 H4]].
symmetry in H3.
destruct (Perm_list_eq_commute R x l' x0 H3 H2).
∃ x1.
split.
transitivity x; intuition.
transitivity x0; intuition.
intros [?[E?]]. rewrite E.
symmetry. apply SetoidPermutation_from_Permutation...
apply _.
Qed.
Instance map_perm_proper {A B} (Ra: relation A) (Rb: relation B):
Equivalence Ra →
Equivalence Rb →
Proper ((Ra ==> Rb) ==> SetoidPermutation Ra ==> SetoidPermutation Rb) (@map A B).
Proof with simpl; auto; try reflexivity.
intros ??????? X.
induction X; simpl...
apply s_perm_trans with (x y0 :: x x0 :: map y l).
apply s_perm_skip...
apply s_perm_skip...
induction l... intuition.
apply s_perm_trans with (y y0 :: y x0 :: map y l)...
unfold respectful in ×.
apply s_perm_skip. intuition.
apply s_perm_skip... intuition.
apply s_perm_trans with (map y l')...
apply s_perm_trans with (map x l')...
clear IHX1 IHX2 X1 X2.
induction l'... constructor. now symmetry; apply H1. easy.
Qed.