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
|
(************************************************************************)
(* 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*)
Require Import Le.
Require Import Lt.
Open Local Scope nat_scope.
Implicit Types k l p q r : nat.
Section Between.
Variables P Q : nat -> Prop.
Inductive between k : nat -> Prop :=
| bet_emp : between k k
| bet_S : forall l, between k l -> P l -> between k (S l).
Hint Constructors between: arith v62.
Lemma bet_eq : forall k l, l = k -> between k l.
Proof.
induction 1; auto with arith.
Qed.
Hint Resolve bet_eq: arith v62.
Lemma between_le : forall k l, between k l -> k <= l.
Proof.
induction 1; auto with arith.
Qed.
Hint Immediate between_le: arith v62.
Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
Proof.
intros k l H; induction H as [|l H].
intros; absurd (S k <= k); auto with arith.
destruct H; auto with arith.
Qed.
Hint Resolve between_Sk_l: arith v62.
Lemma between_restr :
forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m.
Proof.
induction 1; auto with arith.
Qed.
Inductive exists_between k : nat -> Prop :=
| exists_S : forall l, exists_between k l -> exists_between k (S l)
| exists_le : forall l, k <= l -> Q l -> exists_between k (S l).
Hint Constructors exists_between: arith v62.
Lemma exists_le_S : forall k l, exists_between k l -> S k <= l.
Proof.
induction 1; auto with arith.
Qed.
Lemma exists_lt : forall k l, exists_between k l -> k < l.
Proof exists_le_S.
Hint Immediate exists_le_S exists_lt: arith v62.
Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
Proof.
intros; apply le_S_n; auto with arith.
Qed.
Hint Immediate exists_S_le: arith v62.
Definition in_int p q r := p <= r /\ r < q.
Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r.
Proof.
red in |- *; auto with arith.
Qed.
Hint Resolve in_int_intro: arith v62.
Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
Proof.
induction 1; intros.
apply le_lt_trans with r; auto with arith.
Qed.
Lemma in_int_p_Sq :
forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat.
Proof.
induction 1; intros.
elim (le_lt_or_eq r q); auto with arith.
Qed.
Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r.
Proof.
induction 1; auto with arith.
Qed.
Hint Resolve in_int_S: arith v62.
Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
Proof.
induction 1; auto with arith.
Qed.
Hint Immediate in_int_Sp_q: arith v62.
Lemma between_in_int :
forall k l, between k l -> forall r, in_int k l r -> P r.
Proof.
induction 1; intros.
absurd (k < k); auto with arith.
apply in_int_lt with r; auto with arith.
elim (in_int_p_Sq k l r); intros; auto with arith.
rewrite H2; trivial with arith.
Qed.
Lemma in_int_between :
forall k l, k <= l -> (forall r, in_int k l r -> P r) -> between k l.
Proof.
induction 1; auto with arith.
Qed.
Lemma exists_in_int :
forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m.
Proof.
induction 1.
case IHexists_between; intros p inp Qp; exists p; auto with arith.
exists l; auto with arith.
Qed.
Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l.
Proof.
destruct 1; intros.
elim H0; auto with arith.
Qed.
Lemma between_or_exists :
forall k l,
k <= l ->
(forall n:nat, in_int k l n -> P n \/ Q n) ->
between k l \/ exists_between k l.
Proof.
induction 1; intros; auto with arith.
elim IHle; intro; auto with arith.
elim (H0 m); auto with arith.
Qed.
Lemma between_not_exists :
forall k l,
between k l ->
(forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l.
Proof.
induction 1; red in |- *; intros.
absurd (k < k); auto with arith.
absurd (Q l); auto with arith.
elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'.
replace l with l'; auto with arith.
elim inl'; intros.
elim (le_lt_or_eq l' l); auto with arith; intros.
absurd (exists_between k l); auto with arith.
apply in_int_exists with l'; auto with arith.
Qed.
Inductive P_nth (init:nat) : nat -> nat -> Prop :=
| nth_O : P_nth init init 0
| nth_S :
forall k l (n:nat),
P_nth init k n -> between (S k) l -> Q l -> P_nth init l (S n).
Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l.
Proof.
induction 1; intros; auto with arith.
apply le_trans with (S k); auto with arith.
Qed.
Definition eventually (n:nat) := exists2 k : nat, k <= n & Q k.
Lemma event_O : eventually 0 -> Q 0.
Proof.
induction 1; intros.
replace 0 with x; auto with arith.
Qed.
End Between.
Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
in_int_S in_int_intro: arith v62.
Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62.
|
