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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
(* $Id: ArrayPermut.v 5920 2004-07-16 20:01:26Z herbelin $ *)
(****************************************************************************)
(* Permutations of elements in arrays *)
(* Definition and properties *)
(****************************************************************************)
Require Import ProgInt.
Require Import Arrays.
Require Export Exchange.
Require Import Omega.
Set Implicit Arguments.
(* We define "permut" as the smallest equivalence relation which contains
* transpositions i.e. exchange of two elements.
*)
Inductive permut (n:Z) (A:Set) : array n A -> array n A -> Prop :=
| exchange_is_permut :
forall (t t':array n A) (i j:Z), exchange t t' i j -> permut t t'
| permut_refl : forall t:array n A, permut t t
| permut_sym : forall t t':array n A, permut t t' -> permut t' t
| permut_trans :
forall t t' t'':array n A, permut t t' -> permut t' t'' -> permut t t''.
Hint Resolve exchange_is_permut permut_refl permut_sym permut_trans: v62
datatypes.
(* We also define the permutation on a segment of an array, "sub_permut",
* the other parts of the array being unchanged
*
* One again we define it as the smallest equivalence relation containing
* transpositions on the given segment.
*)
Inductive sub_permut (n:Z) (A:Set) (g d:Z) :
array n A -> array n A -> Prop :=
| exchange_is_sub_permut :
forall (t t':array n A) (i j:Z),
(g <= i <= d)%Z ->
(g <= j <= d)%Z -> exchange t t' i j -> sub_permut g d t t'
| sub_permut_refl : forall t:array n A, sub_permut g d t t
| sub_permut_sym :
forall t t':array n A, sub_permut g d t t' -> sub_permut g d t' t
| sub_permut_trans :
forall t t' t'':array n A,
sub_permut g d t t' -> sub_permut g d t' t'' -> sub_permut g d t t''.
Hint Resolve exchange_is_sub_permut sub_permut_refl sub_permut_sym
sub_permut_trans: v62 datatypes.
(* To express that some parts of arrays are equal we introduce the
* property "array_id" which says that a segment is the same on two
* arrays.
*)
Definition array_id (n:Z) (A:Set) (t t':array n A)
(g d:Z) := forall i:Z, (g <= i <= d)%Z -> #t [i] = #t' [i].
(* array_id is an equivalence relation *)
Lemma array_id_refl :
forall (n:Z) (A:Set) (t:array n A) (g d:Z), array_id t t g d.
Proof.
unfold array_id in |- *.
auto with datatypes.
Qed.
Hint Resolve array_id_refl: v62 datatypes.
Lemma array_id_sym :
forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
array_id t t' g d -> array_id t' t g d.
Proof.
unfold array_id in |- *. intros.
symmetry in |- *; auto with datatypes.
Qed.
Hint Resolve array_id_sym: v62 datatypes.
Lemma array_id_trans :
forall (n:Z) (A:Set) (t t' t'':array n A) (g d:Z),
array_id t t' g d -> array_id t' t'' g d -> array_id t t'' g d.
Proof.
unfold array_id in |- *. intros.
apply trans_eq with (y := #t' [i]); auto with datatypes.
Qed.
Hint Resolve array_id_trans: v62 datatypes.
(* Outside the segment [g,d] the elements are equal *)
Lemma sub_permut_id :
forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
sub_permut g d t t' ->
array_id t t' 0 (g - 1) /\ array_id t t' (d + 1) (n - 1).
Proof.
intros n A t t' g d. simple induction 1; intros.
elim H2; intros.
unfold array_id in |- *; split; intros.
apply H7; omega.
apply H7; omega.
auto with datatypes.
decompose [and] H1; auto with datatypes.
decompose [and] H1; decompose [and] H3; eauto with datatypes.
Qed.
Hint Resolve sub_permut_id.
Lemma sub_permut_eq :
forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
sub_permut g d t t' ->
forall i:Z, (0 <= i < g)%Z \/ (d < i < n)%Z -> #t [i] = #t' [i].
Proof.
intros n A t t' g d Htt' i Hi.
elim (sub_permut_id Htt'). unfold array_id in |- *.
intros.
elim Hi; [ intro; apply H; omega | intro; apply H0; omega ].
Qed.
(* sub_permut is a particular case of permutation *)
Lemma sub_permut_is_permut :
forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
sub_permut g d t t' -> permut t t'.
Proof.
intros n A t t' g d. simple induction 1; intros; eauto with datatypes.
Qed.
Hint Resolve sub_permut_is_permut.
(* If we have a sub-permutation on an empty segment, then we have a
* sub-permutation on any segment.
*)
Lemma sub_permut_void :
forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z),
(d < g)%Z -> sub_permut g d t t' -> sub_permut g' d' t t'.
Proof.
intros N A t t' g g' d d' Hdg.
simple induction 1; intros.
absurd (g <= d)%Z; omega.
auto with datatypes.
auto with datatypes.
eauto with datatypes.
Qed.
(* A sub-permutation on a segment may be extended to any segment that
* contains the first one.
*)
Lemma sub_permut_extension :
forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z),
(g' <= g)%Z -> (d <= d')%Z -> sub_permut g d t t' -> sub_permut g' d' t t'.
Proof.
intros N A t t' g g' d d' Hgg' Hdd'.
simple induction 1; intros.
apply exchange_is_sub_permut with (i := i) (j := j);
[ omega | omega | assumption ].
auto with datatypes.
auto with datatypes.
eauto with datatypes.
Qed.
|
