1
<html xmlns="http://www.w3.org/1999/xhtml">
3
<meta http-equiv="Content-Type" content="text/html; charset="><link rel="stylesheet" href="style.css" type="text/css"><title>Coq.Arith.Wf_nat</title>
8
<h1>Library Coq.Arith.Wf_nat</h1>
13
<table width="100%"><tr class="doc"><td>
14
Well-founded relations and natural numbers
19
<code class="keyword">Require</code> <code class="keyword">Import</code> Lt.<br/>
22
Open <code class="keyword">Local</code> Scope nat_scope.<br/>
25
<code class="keyword">Implicit</code> Types m n p : <a href="Coq.Init.Datatypes.html#nat">nat</a>.<br/>
28
<code class="keyword">Section</code> Well_founded_Nat.<br/>
31
<code class="keyword">Variable</code> A : Set.<br/>
34
<code class="keyword">Variable</code> f : A -> <a href="Coq.Init.Datatypes.html#nat">nat</a>.<br/>
35
<code class="keyword">Definition</code> <a name="ltof"></a>ltof (a b:A) := f a < f b.<br/>
36
<code class="keyword">Definition</code> <a name="gtof"></a>gtof (a b:A) := f b > f a.<br/>
39
<code class="keyword">Theorem</code> <a name="well_founded_ltof"></a>well_founded_ltof : <a href="Coq.Init.Wf.html#well_founded">well_founded</a> <a href="Coq.Arith.Wf_nat.html#ltof">ltof</a>.<br/>
40
<code class="keyword">Proof</code>.<br/>
42
cut (forall n (a:A), f a < n -> <a href="Coq.Init.Wf.html#Acc">Acc</a> <a href="Coq.Arith.Wf_nat.html#ltof">ltof</a> a).<br/>
43
intros H a; apply (H (<a href="Coq.Init.Datatypes.html#S">S</a> (f a))); auto with arith.<br/>
45
intros; absurd (f a < 0); auto with arith.<br/>
47
apply <a href="Coq.Init.Wf.html#Acc_intro">Acc_intro</a>.<br/>
48
unfold ltof in |- *; intros b ltfafb.<br/>
50
apply <a href="Coq.Arith.Lt.html#lt_le_trans">lt_le_trans</a> with (f a); auto with arith.<br/>
51
<code class="keyword">Qed</code>.<br/>
54
<code class="keyword">Theorem</code> <a name="well_founded_gtof"></a>well_founded_gtof : <a href="Coq.Init.Wf.html#well_founded">well_founded</a> <a href="Coq.Arith.Wf_nat.html#gtof">gtof</a>.<br/>
55
<code class="keyword">Proof</code> <a href="Coq.Arith.Wf_nat.html#well_founded_ltof">well_founded_ltof</a>.<br/>
60
<table width="100%"><tr class="doc"><td>
61
It is possible to directly prove the induction principle going
62
back to primitive recursion on natural numbers (<code>induction_ltof1</code>)
63
or to use the previous lemmas to extract a program with a fixpoint
64
(<code>induction_ltof2</code>)
67
the ML-like program for <code>induction_ltof1</code> is :
70
let induction_ltof1 F a = indrec ((f a)+1) a <br/>
71
where rec indrec = <br/>
72
function 0 -> (function a -> error)<br/>
73
|(S m) -> (function a -> (F a (function y -> indrec y m)));;</code>
75
<table width="100%"><tr class="doc"><td>
79
the ML-like program for <code>induction_ltof2</code> is :
82
let induction_ltof2 F a = indrec a<br/>
83
where rec indrec a = F a indrec;;</code>
85
<table width="100%"><tr class="doc"><td>
91
<code class="keyword">Theorem</code> <a name="induction_ltof1"></a>induction_ltof1 :<br/>
92
forall P:A -> Set,<br/>
93
(forall x:A, (forall y:A, <a href="Coq.Arith.Wf_nat.html#ltof">ltof</a> y x -> P y) -> P x) -> forall a:A, P a.<br/>
94
<code class="keyword">Proof</code>.<br/>
95
intros P F; cut (forall n (a:A), f a < n -> P a).<br/>
96
intros H a; apply (H (<a href="Coq.Init.Datatypes.html#S">S</a> (f a))); auto with arith.<br/>
98
intros; absurd (f a < 0); auto with arith.<br/>
101
unfold ltof in |- *; intros b ltfafb.<br/>
103
apply <a href="Coq.Arith.Lt.html#lt_le_trans">lt_le_trans</a> with (f a); auto with arith.<br/>
104
<code class="keyword">Defined</code>. <br/>
107
<code class="keyword">Theorem</code> <a name="induction_gtof1"></a>induction_gtof1 :<br/>
108
forall P:A -> Set,<br/>
109
(forall x:A, (forall y:A, <a href="Coq.Arith.Wf_nat.html#gtof">gtof</a> y x -> P y) -> P x) -> forall a:A, P a.<br/>
110
<code class="keyword">Proof</code>.<br/>
111
exact <a href="Coq.Arith.Wf_nat.html#induction_ltof1">induction_ltof1</a>.<br/>
112
<code class="keyword">Defined</code>.<br/>
115
<code class="keyword">Theorem</code> <a name="induction_ltof2"></a>induction_ltof2 :<br/>
116
forall P:A -> Set,<br/>
117
(forall x:A, (forall y:A, <a href="Coq.Arith.Wf_nat.html#ltof">ltof</a> y x -> P y) -> P x) -> forall a:A, P a.<br/>
118
<code class="keyword">Proof</code>.<br/>
119
exact (<a href="Coq.Init.Wf.html#well_founded_induction">well_founded_induction</a> <a href="Coq.Arith.Wf_nat.html#well_founded_ltof">well_founded_ltof</a>).<br/>
120
<code class="keyword">Defined</code>.<br/>
123
<code class="keyword">Theorem</code> <a name="induction_gtof2"></a>induction_gtof2 :<br/>
124
forall P:A -> Set,<br/>
125
(forall x:A, (forall y:A, <a href="Coq.Arith.Wf_nat.html#gtof">gtof</a> y x -> P y) -> P x) -> forall a:A, P a.<br/>
126
<code class="keyword">Proof</code>.<br/>
127
exact <a href="Coq.Arith.Wf_nat.html#induction_ltof2">induction_ltof2</a>.<br/>
128
<code class="keyword">Defined</code>.<br/>
133
<table width="100%"><tr class="doc"><td>
134
If a relation <code>R</code> is compatible with <code>lt</code> i.e. if <code>x R y => f(x) < f(y)</code>
135
then <code>R</code> is well-founded.
140
<code class="keyword">Variable</code> R : A -> A -> Prop.<br/>
143
<code class="keyword">Hypothesis</code> H_compat : forall x y:A, R x y -> f x < f y.<br/>
146
<code class="keyword">Theorem</code> <a name="well_founded_lt_compat"></a>well_founded_lt_compat : <a href="Coq.Init.Wf.html#well_founded">well_founded</a> R.<br/>
147
<code class="keyword">Proof</code>.<br/>
149
cut (forall n (a:A), f a < n -> <a href="Coq.Init.Wf.html#Acc">Acc</a> R a).<br/>
150
intros H a; apply (H (<a href="Coq.Init.Datatypes.html#S">S</a> (f a))); auto with arith.<br/>
152
intros; absurd (f a < 0); auto with arith.<br/>
154
apply <a href="Coq.Init.Wf.html#Acc_intro">Acc_intro</a>.<br/>
155
intros b ltfafb.<br/>
157
apply <a href="Coq.Arith.Lt.html#lt_le_trans">lt_le_trans</a> with (f a); auto with arith.<br/>
158
<code class="keyword">Qed</code>.<br/>
161
<code class="keyword">End</code> Well_founded_Nat.<br/>
164
<code class="keyword">Lemma</code> <a name="lt_wf"></a>lt_wf : <a href="Coq.Init.Wf.html#well_founded">well_founded</a> <a href="Coq.Init.Peano.html#lt">lt</a>.<br/>
165
<code class="keyword">Proof</code> <a href="Coq.Arith.Wf_nat.html#well_founded_ltof">well_founded_ltof</a> <a href="Coq.Init.Datatypes.html#nat">nat</a> (fun m => m).<br/>
168
<code class="keyword">Lemma</code> <a name="lt_wf_rec1"></a>lt_wf_rec1 :<br/>
169
forall n (P:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.<br/>
170
<code class="keyword">Proof</code>.<br/>
172
(fun p (P:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) =><br/>
173
<a href="Coq.Arith.Wf_nat.html#induction_ltof1">induction_ltof1</a> <a href="Coq.Init.Datatypes.html#nat">nat</a> (fun m => m) P F p).<br/>
174
<code class="keyword">Defined</code>.<br/>
177
<code class="keyword">Lemma</code> <a name="lt_wf_rec"></a>lt_wf_rec :<br/>
178
forall n (P:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.<br/>
179
<code class="keyword">Proof</code>.<br/>
181
(fun p (P:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) =><br/>
182
<a href="Coq.Arith.Wf_nat.html#induction_ltof2">induction_ltof2</a> <a href="Coq.Init.Datatypes.html#nat">nat</a> (fun m => m) P F p).<br/>
183
<code class="keyword">Defined</code>.<br/>
186
<code class="keyword">Lemma</code> <a name="lt_wf_ind"></a>lt_wf_ind :<br/>
187
forall n (P:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.<br/>
188
intro p; intros; elim (<a href="Coq.Arith.Wf_nat.html#lt_wf">lt_wf</a> p); auto with arith.<br/>
189
<code class="keyword">Qed</code>.<br/>
192
<code class="keyword">Lemma</code> <a name="gt_wf_rec"></a>gt_wf_rec :<br/>
193
forall n (P:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n.<br/>
194
<code class="keyword">Proof</code>.<br/>
195
exact <a href="Coq.Arith.Wf_nat.html#lt_wf_rec">lt_wf_rec</a>.<br/>
196
<code class="keyword">Defined</code>.<br/>
199
<code class="keyword">Lemma</code> <a name="gt_wf_ind"></a>gt_wf_ind :<br/>
200
forall n (P:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n.<br/>
201
<code class="keyword">Proof</code> <a href="Coq.Arith.Wf_nat.html#lt_wf_ind">lt_wf_ind</a>.<br/>
204
<code class="keyword">Lemma</code> <a name="lt_wf_double_rec"></a>lt_wf_double_rec :<br/>
205
forall P:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> <a href="Coq.Init.Datatypes.html#nat">nat</a> -> Set,<br/>
206
(forall n m,<br/>
207
(forall p (q:<a href="Coq.Init.Datatypes.html#nat">nat</a>), p < n -> P p q) -><br/>
208
(forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.<br/>
209
intros P Hrec p; pattern p in |- *; apply <a href="Coq.Arith.Wf_nat.html#lt_wf_rec">lt_wf_rec</a>.<br/>
210
intros n H q; pattern q in |- *; apply <a href="Coq.Arith.Wf_nat.html#lt_wf_rec">lt_wf_rec</a>; auto with arith.<br/>
211
<code class="keyword">Defined</code>.<br/>
214
<code class="keyword">Lemma</code> <a name="lt_wf_double_ind"></a>lt_wf_double_ind :<br/>
215
forall P:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> <a href="Coq.Init.Datatypes.html#nat">nat</a> -> Prop,<br/>
216
(forall n m,<br/>
217
(forall p (q:<a href="Coq.Init.Datatypes.html#nat">nat</a>), p < n -> P p q) -><br/>
218
(forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.<br/>
219
intros P Hrec p; pattern p in |- *; apply <a href="Coq.Arith.Wf_nat.html#lt_wf_ind">lt_wf_ind</a>.<br/>
220
intros n H q; pattern q in |- *; apply <a href="Coq.Arith.Wf_nat.html#lt_wf_ind">lt_wf_ind</a>; auto with arith.<br/>
221
<code class="keyword">Qed</code>.<br/>
224
<code class="keyword">Hint</code> Resolve <a href="Coq.Arith.Wf_nat.html#lt_wf">lt_wf</a>: arith.<br/>
225
<code class="keyword">Hint</code> Resolve <a href="Coq.Arith.Wf_nat.html#well_founded_lt_compat">well_founded_lt_compat</a>: arith.<br/>
228
<code class="keyword">Section</code> LT_WF_REL.<br/>
229
<code class="keyword">Variable</code> A : Set.<br/>
230
<code class="keyword">Variable</code> R : A -> A -> Prop.<br/>
233
<code class="keyword">Variable</code> F : A -> <a href="Coq.Init.Datatypes.html#nat">nat</a> -> Prop.<br/>
234
<code class="keyword">Definition</code> <a name="inv_lt_rel"></a>inv_lt_rel x y :=<br/>
235
exists2 n : _, F x n & (forall m, F y m -> n < m).<br/>
238
<code class="keyword">Hypothesis</code> F_compat : forall x y:A, R x y -> <a href="Coq.Arith.Wf_nat.html#inv_lt_rel">inv_lt_rel</a> x y.<br/>
239
<code class="keyword">Remark</code> acc_lt_rel : forall x:A, (exists n : _, F x n) -> <a href="Coq.Init.Wf.html#Acc">Acc</a> R x.<br/>
240
intros x [n fxn]; generalize x fxn; clear x fxn.<br/>
241
pattern n in |- *; apply <a href="Coq.Arith.Wf_nat.html#lt_wf_ind">lt_wf_ind</a>; intros.<br/>
242
constructor; intros.<br/>
243
case (F_compat y x); trivial; intros.<br/>
244
apply (H x0); auto.<br/>
245
<code class="keyword">Qed</code>.<br/>
248
<code class="keyword">Theorem</code> <a name="well_founded_inv_lt_rel_compat"></a>well_founded_inv_lt_rel_compat : <a href="Coq.Init.Wf.html#well_founded">well_founded</a> R.<br/>
249
constructor; intros.<br/>
250
case (F_compat y a); trivial; intros.<br/>
251
apply <a href="Coq.Arith.Wf_nat.html#acc_lt_rel">acc_lt_rel</a>; trivial.<br/>
252
exists x; trivial.<br/>
253
<code class="keyword">Qed</code>.<br/>
256
<code class="keyword">End</code> LT_WF_REL.<br/>
259
<code class="keyword">Lemma</code> <a name="well_founded_inv_rel_inv_lt_rel"></a>well_founded_inv_rel_inv_lt_rel :<br/>
260
forall (A:Set) (F:A -> <a href="Coq.Init.Datatypes.html#nat">nat</a> -> Prop), <a href="Coq.Init.Wf.html#well_founded">well_founded</a> (<a href="Coq.Arith.Wf_nat.html#inv_lt_rel">inv_lt_rel</a> A F).<br/>
261
intros; apply (<a href="Coq.Arith.Wf_nat.html#well_founded_inv_lt_rel_compat">well_founded_inv_lt_rel_compat</a> A (<a href="Coq.Arith.Wf_nat.html#inv_lt_rel">inv_lt_rel</a> A F) F); trivial.<br/>
262
<code class="keyword">Qed</code>.</code>
263
<hr/><a href="index.html">Index</a><hr/><font size="-1">This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a></font>
b'\\ No newline at end of file'
added
removed
library/Coq.Arith.Wf_nat.html
