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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(*i $Id$ i*)
(** Well-founded relations and natural numbers *)
Require Import Lt.
Open Local Scope nat_scope.
Implicit Types m n p : nat.
Section Well_founded_Nat.
Variable A : Type.
Variable f : A -> nat.
Definition ltof (a b:A) := f a < f b.
Definition gtof (a b:A) := f b > f a.
Theorem well_founded_ltof : well_founded ltof.
Proof.
red in |- *.
cut (forall n (a:A), f a < n -> Acc ltof a).
intros H a; apply (H (S (f a))); auto with arith.
induction n.
intros; absurd (f a < 0); auto with arith.
intros a ltSma.
apply Acc_intro.
unfold ltof in |- *; intros b ltfafb.
apply IHn.
apply lt_le_trans with (f a); auto with arith.
Defined.
Theorem well_founded_gtof : well_founded gtof.
Proof.
exact well_founded_ltof.
Defined.
(** It is possible to directly prove the induction principle going
back to primitive recursion on natural numbers ([induction_ltof1])
or to use the previous lemmas to extract a program with a fixpoint
([induction_ltof2])
the ML-like program for [induction_ltof1] is :
[[
let induction_ltof1 F a = indrec ((f a)+1) a
where rec indrec =
function 0 -> (function a -> error)
|(S m) -> (function a -> (F a (function y -> indrec y m)));;
]]
the ML-like program for [induction_ltof2] is :
[[
let induction_ltof2 F a = indrec a
where rec indrec a = F a indrec;;
]]
*)
Theorem induction_ltof1 :
forall P:A -> Set,
(forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
intros P F; cut (forall n (a:A), f a < n -> P a).
intros H a; apply (H (S (f a))); auto with arith.
induction n.
intros; absurd (f a < 0); auto with arith.
intros a ltSma.
apply F.
unfold ltof in |- *; intros b ltfafb.
apply IHn.
apply lt_le_trans with (f a); auto with arith.
Defined.
Theorem induction_gtof1 :
forall P:A -> Set,
(forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
exact induction_ltof1.
Defined.
Theorem induction_ltof2 :
forall P:A -> Set,
(forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
exact (well_founded_induction well_founded_ltof).
Defined.
Theorem induction_gtof2 :
forall P:A -> Set,
(forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
exact induction_ltof2.
Defined.
(** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)]
then [R] is well-founded. *)
Variable R : A -> A -> Prop.
Hypothesis H_compat : forall x y:A, R x y -> f x < f y.
Theorem well_founded_lt_compat : well_founded R.
Proof.
red in |- *.
cut (forall n (a:A), f a < n -> Acc R a).
intros H a; apply (H (S (f a))); auto with arith.
induction n.
intros; absurd (f a < 0); auto with arith.
intros a ltSma.
apply Acc_intro.
intros b ltfafb.
apply IHn.
apply lt_le_trans with (f a); auto with arith.
Defined.
End Well_founded_Nat.
Lemma lt_wf : well_founded lt.
Proof.
exact (well_founded_ltof nat (fun m => m)).
Defined.
Lemma lt_wf_rec1 :
forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof.
exact (fun p P F => induction_ltof1 nat (fun m => m) P F p).
Defined.
Lemma lt_wf_rec :
forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof.
exact (fun p P F => induction_ltof2 nat (fun m => m) P F p).
Defined.
Lemma lt_wf_ind :
forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof.
intro p; intros; elim (lt_wf p); auto with arith.
Qed.
Lemma gt_wf_rec :
forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
Proof.
exact lt_wf_rec.
Defined.
Lemma gt_wf_ind :
forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
Proof lt_wf_ind.
Lemma lt_wf_double_rec :
forall P:nat -> nat -> Set,
(forall n m,
(forall p q, p < n -> P p q) ->
(forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
Proof.
intros P Hrec p; pattern p in |- *; apply lt_wf_rec.
intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith.
Defined.
Lemma lt_wf_double_ind :
forall P:nat -> nat -> Prop,
(forall n m,
(forall p (q:nat), p < n -> P p q) ->
(forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
Proof.
intros P Hrec p; pattern p in |- *; apply lt_wf_ind.
intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith.
Qed.
Hint Resolve lt_wf: arith.
Hint Resolve well_founded_lt_compat: arith.
Section LT_WF_REL.
Variable A : Set.
Variable R : A -> A -> Prop.
(* Relational form of inversion *)
Variable F : A -> nat -> Prop.
Definition inv_lt_rel x y := exists2 n, F x n & (forall m, F y m -> n < m).
Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y.
Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x.
Proof.
intros x [n fxn]; generalize dependent x.
pattern n in |- *; apply lt_wf_ind; intros.
constructor; intros.
destruct (F_compat y x) as (x0,H1,H2); trivial.
apply (H x0); auto.
Qed.
Theorem well_founded_inv_lt_rel_compat : well_founded R.
Proof.
constructor; intros.
case (F_compat y a); trivial; intros.
apply acc_lt_rel; trivial.
exists x; trivial.
Qed.
End LT_WF_REL.
Lemma well_founded_inv_rel_inv_lt_rel :
forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F).
intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
Qed.
|
