1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
Require Import
Coq.Unicode.Utf8 Coq.Setoids.Setoid CoRN.stdlib_omissions.List Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms.
(** 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 (forall 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.
#[global]
Hint Constructors SetoidPermutation Permutation.
Lemma SetoidPermutation_stronger {A} (R U: relation A):
(forall x y: A, R x y → U x y) →
forall 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.
exists nil. intuition.
destruct IHSetoidPermutation as [?[??]].
exists (y :: x0).
repeat split...
exists (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).
exists x1.
split.
transitivity x; intuition.
transitivity x0; intuition.
intros [?[E?]]. rewrite E.
symmetry. apply SetoidPermutation_from_Permutation...
apply _.
Qed.
#[global]
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.
|
