blob: b0c715c8bce7c487fa279bdb13eb071aee115ef6 (
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
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
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(*i $Id$ i*)
(** Well-founded relations and natural numbers *)
Require Lt.
Import nat_scope.
Chapter Well_founded_Nat.
Variable A : Set.
Variable f : A -> nat.
Definition ltof := [a,b:A](lt (f a) (f b)).
Definition gtof := [a,b:A](gt (f b) (f a)).
Theorem well_founded_ltof : (well_founded A ltof).
Proof.
Red.
Cut (n:nat)(a:A)(lt (f a) n)->(Acc A ltof a).
Intros H a; Apply (H (S (f a))); Auto with arith.
NewInduction n.
Intros; Absurd (lt (f a) O); Auto with arith.
Intros a ltSma.
Apply Acc_intro.
Unfold ltof; Intros b ltfafb.
Apply IHn.
Apply lt_le_trans with (f a); Auto with arith.
Qed.
Theorem well_founded_gtof : (well_founded A gtof).
Proof well_founded_ltof.
(** 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
: (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
Proof.
Intros P F; Cut (n:nat)(a:A)(lt (f a) n)->(P a).
Intros H a; Apply (H (S (f a))); Auto with arith.
NewInduction n.
Intros; Absurd (lt (f a) O); Auto with arith.
Intros a ltSma.
Apply F.
Unfold ltof; Intros b ltfafb.
Apply IHn.
Apply lt_le_trans with (f a); Auto with arith.
Defined.
Theorem induction_gtof1
: (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
Proof.
Exact induction_ltof1.
Defined.
Theorem induction_ltof2
: (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
Proof.
Exact (well_founded_induction A ltof well_founded_ltof).
Defined.
Theorem induction_gtof2
: (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(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 : (x,y:A) (R x y) -> (lt (f x) (f y)).
Theorem well_founded_lt_compat : (well_founded A R).
Proof.
Red.
Cut (n:nat)(a:A)(lt (f a) n)->(Acc A R a).
Intros H a; Apply (H (S (f a))); Auto with arith.
NewInduction n.
Intros; Absurd (lt (f a) O); Auto with arith.
Intros a ltSma.
Apply Acc_intro.
Intros b ltfafb.
Apply IHn.
Apply lt_le_trans with (f a); Auto with arith.
Qed.
End Well_founded_Nat.
Lemma lt_wf : (well_founded nat lt).
Proof (well_founded_ltof nat [m:nat]m).
Lemma lt_wf_rec1 : (p:nat)(P:nat->Set)
((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
Proof.
Exact [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)]
(induction_ltof1 nat [m:nat]m P F p).
Defined.
Lemma lt_wf_rec : (p:nat)(P:nat->Set)
((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
Proof.
Exact [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)]
(induction_ltof2 nat [m:nat]m P F p).
Defined.
Lemma lt_wf_ind : (p:nat)(P:nat->Prop)
((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
Intros; Elim (lt_wf p); Auto with arith.
Qed.
Lemma gt_wf_rec : (p:nat)(P:nat->Set)
((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p).
Proof.
Exact lt_wf_rec.
Defined.
Lemma gt_wf_ind : (p:nat)(P:nat->Prop)
((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p).
Proof lt_wf_ind.
Lemma lt_wf_double_rec :
(P:nat->nat->Set)
((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m))
-> (p,q:nat)(P p q).
Intros P Hrec p; Pattern p; Apply lt_wf_rec.
Intros; Pattern q; Apply lt_wf_rec; Auto with arith.
Defined.
Lemma lt_wf_double_ind :
(P:nat->nat->Prop)
((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m))
-> (p,q:nat)(P p q).
Intros P Hrec p; Pattern p; Apply lt_wf_ind.
Intros; Pattern q; Apply lt_wf_ind; Auto with arith.
Qed.
Hints Resolve lt_wf : arith.
Hints Resolve well_founded_lt_compat : arith.
|
