blob: b0657b63aab1d7351ea5cc901d4e43b6a6288593 (
plain)
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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
Require Import SetoidList.
Set Implicit Arguments.
Unset Strict Implicit.
(** 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.
Proof.
constructor.
- intro l. induction l; intuition.
- intros l₁ l₂. induction 1; eauto. apply permA_skip; intuition.
- exact permA_trans.
Qed.
Global Instance PermutationA_cons :
Proper (eqA ==> PermutationA ==> PermutationA) (@cons A).
Proof.
repeat intro. now apply permA_skip.
Qed.
Lemma PermutationA_app_head l₁ l₂ l :
PermutationA l₁ l₂ -> PermutationA (l ++ l₁) (l ++ l₂).
Proof.
induction l; trivial; intros. apply permA_skip; intuition.
Qed.
Global Instance PermutationA_app :
Proper (PermutationA ==> PermutationA ==> PermutationA) (@app A).
Proof.
intros l₁ l₂ Pl k₁ k₂ Pk.
induction Pl.
- easy.
- now apply permA_skip.
- etransitivity.
* rewrite <-!app_comm_cons. now apply permA_swap.
* rewrite !app_comm_cons. now apply PermutationA_app_head.
- do 2 (etransitivity; try eassumption).
apply PermutationA_app_head. now symmetry.
Qed.
Lemma PermutationA_app_tail l₁ l₂ l :
PermutationA l₁ l₂ -> PermutationA (l₁ ++ l) (l₂ ++ l).
Proof.
intros E. now rewrite E.
Qed.
Lemma PermutationA_cons_append l x :
PermutationA (x :: l) (l ++ x :: nil).
Proof.
induction l.
- easy.
- simpl. rewrite <-IHl. intuition.
Qed.
Lemma PermutationA_app_comm l₁ l₂ :
PermutationA (l₁ ++ l₂) (l₂ ++ l₁).
Proof.
induction l₁.
- now rewrite app_nil_r.
- rewrite <-app_comm_cons, IHl₁, app_comm_cons.
now rewrite PermutationA_cons_append, <-app_assoc.
Qed.
Lemma PermutationA_cons_app l l₁ l₂ x :
PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂).
Proof.
intros E. rewrite E.
now rewrite app_comm_cons, PermutationA_cons_append, <-app_assoc.
Qed.
Lemma PermutationA_middle l₁ l₂ x :
PermutationA (x :: l₁ ++ l₂) (l₁ ++ x :: l₂).
Proof.
now apply PermutationA_cons_app.
Qed.
Lemma PermutationA_equivlistA l₁ l₂ :
PermutationA l₁ l₂ -> equivlistA eqA l₁ l₂.
Proof.
induction 1.
- reflexivity.
- now apply equivlistA_cons_proper.
- now apply equivlistA_permute_heads.
- etransitivity; eassumption.
Qed.
Lemma NoDupA_equivlistA_PermutationA l₁ l₂ :
NoDupA eqA l₁ -> NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂.
Proof.
intros Pl₁. revert l₂. induction Pl₁ as [|x l₁ E1].
- intros l₂ _ H₂. symmetry in H₂. now rewrite (equivlistA_nil_eq eqA).
- intros l₂ Pl₂ E2.
destruct (@InA_split _ eqA l₂ x) as [l₂h [y [l₂t [E3 ?]]]].
{ rewrite <-E2. intuition. }
subst. transitivity (y :: l₁); [intuition |].
apply PermutationA_cons_app, IHPl₁.
now apply NoDupA_split with y.
apply equivlistA_NoDupA_split with x y; intuition.
Qed.
End Permutation.
|
