Mercurial > cpdt > repo

comparison src/Generic.v @ 197:f6293ba66559

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
map_id
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 14:10:23 -0500
parents b4ea71b6bf94
children a35eaec19781
comparison
equal deleted inserted replaced
196:b4ea71b6bf94 197:f6293ba66559
204 forall (R : Type) (cases : datatypeDenote R dt) 204 forall (R : Type) (cases : datatypeDenote R dt)
205 c (m : member c dt) 205 c (m : member c dt)
206 (x : nonrecursive c) (r : ilist T (recursive c)), 206 (x : nonrecursive c) (r : ilist T (recursive c)),
207 fx R cases ((hget dd m) x r) 207 fx R cases ((hget dd m) x r)
208 = (hget cases m) x (imap (fx R cases) 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. 209 End ok.
233 210
234 Implicit Arguments datatypeDenoteOk [T dt]. 211 Implicit Arguments datatypeDenoteOk [T dt].
235 212
236 Lemma foldr_plus : forall n (ils : ilist nat n), 213 Lemma foldr_plus : forall n (ils : ilist nat n),
237 foldr plus 1 ils > 0. 214 foldr plus 1 ils > 0.
238 induction n; crush. 215 induction n; crush.
239 generalize (IHn b); crush. 216 generalize (IHn b); crush.
240 Qed. 217 Qed.
241 218
242 Theorem size_positive : forall T dt (fx : fixDenote T dt) 219 Theorem size_positive : forall T dt
243 (dd : datatypeDenote T dt) (dok : datatypeDenoteOk dd) 220 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
244 (fok : fixDenoteOk dd fx) 221 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
245 (v : T), 222 (v : T),
246 size fx v > 0. 223 size fx v > 0.
247 Hint Rewrite hget_hmake : cpdt. 224 Hint Rewrite hget_hmake : cpdt.
248 Hint Resolve foldr_plus. 225 Hint Resolve foldr_plus.
249 226
250 unfold size; intros; apply (ind dok fok); crush. 227 unfold size; intros; pattern v; apply dok; crush.
251 Qed. 228 Qed.
229
230 Theorem map_id : forall T dt
231 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
232 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
233 (v : T),
234 map dd fx (fun x => x) v = v.
235 Hint Rewrite hget_hmap : cpdt.
236
237 unfold map; intros; pattern v; apply dok; crush.
238 match goal with
239 | [ |- hget _ _ _ ?R1 = hget _ _ _ ?R2 ] => replace R1 with R2
240 end; crush.
241
242 induction (recursive c); crush.
243 destruct r; reflexivity.
244 destruct r; crush.
245 rewrite (H None).
246 unfold icons.
247 f_equal.
248 apply IHn; crush.
249 apply (H (Some i0)).
250 Qed.