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
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(* $Id: Wf.v 11709 2008-12-20 11:42:15Z msozeau $ *)
(** Reformulation of the Wf module using subsets where possible, providing
the support for [Program]'s treatment of well-founded definitions. *)
Require Import Coq.Init.Wf.
Require Import Coq.Program.Utils.
Require Import ProofIrrelevance.
Open Local Scope program_scope.
Implicit Arguments Acc_inv [A R x y].
Section Well_founded.
Variable A : Type.
Variable R : A -> A -> Prop.
Hypothesis Rwf : well_founded R.
Section Acc.
Variable P : A -> Type.
Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y)
(Acc_inv r (proj2_sig y))).
Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
End Acc.
Section FixPoint.
Variable P : A -> Type.
Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *)
Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x).
Hypothesis
F_ext :
forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
(forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g.
Lemma Fix_F_eq :
forall (x:A) (r:Acc R x),
F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r.
Proof.
destruct r using Acc_inv_dep; auto.
Qed.
Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s.
Proof.
intro x; induction (Rwf x); intros.
rewrite (proof_irrelevance (Acc R x) r s) ; auto.
Qed.
Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:A|R y x) => Fix (proj1_sig y)).
Proof.
intro x; unfold Fix in |- *.
rewrite <- (Fix_F_eq ).
apply F_ext; intros.
apply Fix_F_inv.
Qed.
Lemma fix_sub_eq :
forall x : A,
Fix_sub P F_sub x =
let f_sub := F_sub in
f_sub x (fun (y : A | R y x) => Fix (`y)).
exact Fix_eq.
Qed.
End FixPoint.
End Well_founded.
Extraction Inline Fix_F_sub Fix_sub.
Require Import Wf_nat.
Require Import Lt.
Section Well_founded_measure.
Variable A : Type.
Variable m : A -> nat.
Section Acc.
Variable P : A -> Type.
Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
Program Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
F_sub x (fun (y : A | m y < m x) => Fix_measure_F_sub y
(@Acc_inv _ _ _ r (m y) (proj2_sig y))).
Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
End Acc.
Section FixPoint.
Variable P : A -> Type.
Program Variable F_sub : forall x:A, (forall (y : A | m y < m x), P y) -> P x.
Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)).
Hypothesis
F_ext :
forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)),
(forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
Program Lemma Fix_measure_F_eq :
forall (x:A) (r:Acc lt (m x)),
F_sub x (fun (y:A | m y < m x) => Fix_F y (Acc_inv r (proj2_sig y))) = Fix_F x r.
Proof.
intros x.
set (y := m x).
unfold Fix_measure_F_sub.
intros r ; case r ; auto.
Qed.
Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s.
Proof.
intros x r s.
rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto.
Qed.
Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)).
Proof.
intro x; unfold Fix_measure in |- *.
rewrite <- (Fix_measure_F_eq ).
apply F_ext; intros.
apply Fix_measure_F_inv.
Qed.
Lemma fix_measure_sub_eq : forall x : A,
Fix_measure_sub P F_sub x =
let f_sub := F_sub in
f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)).
exact Fix_measure_eq.
Qed.
End FixPoint.
End Well_founded_measure.
Extraction Inline Fix_measure_F_sub Fix_measure_sub.
Set Implicit Arguments.
(** Reasoning about well-founded fixpoints on measures. *)
Section Measure_well_founded.
(* Measure relations are well-founded if the underlying relation is well-founded. *)
Variables T M: Set.
Variable R: M -> M -> Prop.
Hypothesis wf: well_founded R.
Variable m: T -> M.
Definition MR (x y: T): Prop := R (m x) (m y).
Lemma measure_wf: well_founded MR.
Proof with auto.
unfold well_founded.
cut (forall a: M, (fun mm: M => forall a0: T, m a0 = mm -> Acc MR a0) a).
intros.
apply (H (m a))...
apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
intros.
apply Acc_intro.
intros.
unfold MR in H1.
rewrite H0 in H1.
apply (H (m y))...
Defined.
End Measure_well_founded.
Section Fix_measure_rects.
Variable A: Set.
Variable m: A -> nat.
Variable P: A -> Type.
Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x.
Lemma F_unfold x r:
Fix_measure_F_sub A m P f x r =
f (fun y => Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv r (proj2_sig y))).
Proof. intros. case r; auto. Qed.
(* Fix_measure_F_sub_rect lets one prove a property of
functions defined using Fix_measure_F_sub by showing
that property to be invariant over single application of the
function body (f in our case). *)
Lemma Fix_measure_F_sub_rect
(Q: forall x, P x -> Type)
(inv: forall x: A,
(forall (y: A) (H: MR lt m y x) (a: Acc lt (m y)),
Q y (Fix_measure_F_sub A m P f y a)) ->
forall (a: Acc lt (m x)),
Q x (f (fun y: {y: A | m y < m x} =>
Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv a (proj2_sig y)))))
: forall x a, Q _ (Fix_measure_F_sub A m P f x a).
Proof with auto.
intros Q inv.
set (R := fun (x: A) => forall a, Q _ (Fix_measure_F_sub A m P f x a)).
cut (forall x, R x)...
apply (well_founded_induction_type (measure_wf lt_wf m)).
subst R.
simpl.
intros.
rewrite F_unfold...
Qed.
(* Let's call f's second parameter its "lowers" function, since it
provides it access to results for inputs with a lower measure.
In preparation of lemma similar to Fix_measure_F_sub_rect, but
for Fix_measure_sub, we first
need an extra hypothesis stating that the function body has the
same result for different "lowers" functions (g and h below) as long
as those produce the same results for lower inputs, regardless
of the lt proofs. *)
Hypothesis equiv_lowers:
forall x0 (g h: forall x: {y: A | m y < m x0}, P (proj1_sig x)),
(forall x p p', g (exist (fun y: A => m y < m x0) x p) = h (exist _ x p')) ->
f g = f h.
(* From equiv_lowers, it follows that
[Fix_measure_F_sub A m P f x] applications do not not
depend on the Acc proofs. *)
Lemma eq_Fix_measure_F_sub x (a a': Acc lt (m x)):
Fix_measure_F_sub A m P f x a =
Fix_measure_F_sub A m P f x a'.
Proof.
intros x a.
pattern x, (Fix_measure_F_sub A m P f x a).
apply Fix_measure_F_sub_rect.
intros.
rewrite F_unfold.
apply equiv_lowers.
intros.
apply H.
assumption.
Qed.
(* Finally, Fix_measure_F_rect lets one prove a property of
functions defined using Fix_measure_F by showing that
property to be invariant over single application of the function
body (f). *)
Lemma Fix_measure_sub_rect
(Q: forall x, P x -> Type)
(inv: forall
(x: A)
(H: forall (y: A), MR lt m y x -> Q y (Fix_measure_sub A m P f y))
(a: Acc lt (m x)),
Q x (f (fun y: {y: A | m y < m x} => Fix_measure_sub A m P f (proj1_sig y))))
: forall x, Q _ (Fix_measure_sub A m P f x).
Proof with auto.
unfold Fix_measure_sub.
intros.
apply Fix_measure_F_sub_rect.
intros.
assert (forall y: A, MR lt m y x0 -> Q y (Fix_measure_F_sub A m P f y (lt_wf (m y))))...
set (inv x0 X0 a). clearbody q.
rewrite <- (equiv_lowers (fun y: {y: A | m y < m x0} => Fix_measure_F_sub A m P f (proj1_sig y) (lt_wf (m (proj1_sig y)))) (fun y: {y: A | m y < m x0} => Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv a (proj2_sig y))))...
intros.
apply eq_Fix_measure_F_sub.
Qed.
End Fix_measure_rects.
(** Tactic to fold a definitions based on [Fix_measure_sub]. *)
Ltac fold_sub f :=
match goal with
| [ |- ?T ] =>
match T with
appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] =>
let app := context C [ f arg ] in
change app
end
end.
(** This module provides the fixpoint equation provided one assumes
functional extensionality. *)
Module WfExtensionality.
Require Import FunctionalExtensionality.
(** The two following lemmas allow to unfold a well-founded fixpoint definition without
restriction using the functional extensionality axiom. *)
(** For a function defined with Program using a well-founded order. *)
Program Lemma fix_sub_eq_ext :
forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
(P : A -> Set)
(F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x),
forall x : A,
Fix_sub A R Rwf P F_sub x =
F_sub x (fun (y : A | R y x) => Fix A R Rwf P F_sub y).
Proof.
intros ; apply Fix_eq ; auto.
intros.
assert(f = g).
extensionality y ; apply H.
rewrite H0 ; auto.
Qed.
(** For a function defined with Program using a measure. *)
Program Lemma fix_sub_measure_eq_ext :
forall (A : Type) (f : A -> nat) (P : A -> Type)
(F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x),
forall x : A,
Fix_measure_sub A f P F_sub x =
F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y).
Proof.
intros ; apply Fix_measure_eq ; auto.
intros.
assert(f0 = g).
extensionality y ; apply H.
rewrite H0 ; auto.
Qed.
(** Tactic to unfold once a definition based on [Fix_measure_sub]. *)
Ltac unfold_sub f fargs :=
set (call:=fargs) ; unfold f in call ; unfold call ; clear call ;
rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
End WfExtensionality.
|
