Mercurial > cpdt > repo

comparison src/Generic.v @ 196:b4ea71b6bf94

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
size_positive
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 13:38:34 -0500
parents 3676acc40ce1
children f6293ba66559
comparison
equal deleted inserted replaced
195:3676acc40ce1 196:b4ea71b6bf94
161 ::: hnil) (@list_fix A). 161 ::: hnil) (@list_fix A).
162 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) => 162 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
163 print (^ "Leaf" pr 163 print (^ "Leaf" pr
164 ::: ^ "Node" (fun _ => "") 164 ::: ^ "Node" (fun _ => "")
165 ::: hnil) (@tree_fix A). 165 ::: hnil) (@tree_fix A).
166
167
168 (** ** Mapping *)
169
170 Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T) : T -> T :=
171 fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T)
172 (fun _ c x r => f (c x r)) dd).
173
174 Eval compute in map Empty_set_den Empty_set_fix.
175 Eval compute in map unit_den unit_fix.
176 Eval compute in map bool_den bool_fix.
177 Eval compute in map nat_den nat_fix.
178 Eval compute in fun A => map (list_den A) (@list_fix A).
179 Eval compute in fun A => map (tree_den A) (@tree_fix A).
180
181 Definition map_nat := map nat_den nat_fix.
182 Eval simpl in map_nat S 0.
183 Eval simpl in map_nat S 1.
184 Eval simpl in map_nat S 2.
185
186
187 (** * Proving Theorems about Recursive Definitions *)
188
189 Section ok.
190 Variable T : Type.
191 Variable dt : datatype.
192
193 Variable dd : datatypeDenote T dt.
194 Variable fx : fixDenote T dt.
195
196 Definition datatypeDenoteOk :=
197 forall P : T -> Prop,
198 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
199 (forall i : index (recursive c), P (get r i))
200 -> P ((hget dd m) x r))
201 -> forall v, P v.
202
203 Definition fixDenoteOk :=
204 forall (R : Type) (cases : datatypeDenote R dt)
205 c (m : member c dt)
206 (x : nonrecursive c) (r : ilist T (recursive c)),
207 fx R cases ((hget dd m) x r)
208 = (hget cases m) x (imap (fx R cases) r).
209
210 Section ind.
211 Hypothesis dok : datatypeDenoteOk.
212 Hypothesis fok : fixDenoteOk.
213
214 Variable R : Type.
215 Variable cases : datatypeDenote R dt.
216
217 Variable P : R -> Prop.
218
219 Variable ind_case : forall c (m : member c dt)
220 (x : nonrecursive c) (r : ilist T (recursive c)),
221 (forall i : index (recursive c),
222 P (fx R cases (get r i)))
223 -> P ((hget cases m) x (imap (fx R cases) r)).
224
225 Theorem ind : forall v, P (fx R cases v).
226 intro; apply (dok (fun v => P (fx R cases v))); intros.
227 rewrite fok.
228 auto.
229 Qed.
230 End ind.
231
232 End ok.
233
234 Implicit Arguments datatypeDenoteOk [T dt].
235
236 Lemma foldr_plus : forall n (ils : ilist nat n),
237 foldr plus 1 ils > 0.
238 induction n; crush.
239 generalize (IHn b); crush.
240 Qed.
241
242 Theorem size_positive : forall T dt (fx : fixDenote T dt)
243 (dd : datatypeDenote T dt) (dok : datatypeDenoteOk dd)
244 (fok : fixDenoteOk dd fx)
245 (v : T),
246 size fx v > 0.
247 Hint Rewrite hget_hmake : cpdt.
248 Hint Resolve foldr_plus.
249
250 unfold size; intros; apply (ind dok fok); crush.
251 Qed.