Mercurial > cpdt > repo

comparison src/MoreDep.v @ 94:affdf00759d8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Red-black insert
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 20:15:12 -0400
parents a08e82c646a5
children 7804f9d5249f
comparison
equal deleted inserted replaced
93:a08e82c646a5 94:affdf00759d8
339 induction e; crush; 339 induction e; crush;
340 repeat (match goal with 340 repeat (match goal with
341 | [ |- context[cfold ?E] ] => dep_destruct (cfold E) 341 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
342 | [ |- (if ?E then _ else _) = _ ] => destruct E 342 | [ |- (if ?E then _ else _) = _ ] => destruct E
343 end; crush). 343 end; crush).
344 Qed.
345
346
347 (** Dependently-Typed Red-Black Trees *)
348
349 Inductive color : Set := Red | Black.
350
351 Inductive rbtree : color -> nat -> Set :=
352 | Leaf : rbtree Black 0
353 | RedNode : forall n, rbtree Black n -> nat-> rbtree Black n -> rbtree Red n
354 | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n).
355
356 Inductive rtree : nat -> Set :=
357 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
358
359 Notation "{< x >}" := (existT _ _ x).
360
361 Definition balance1 n (a : rtree n) (data : nat) c2 :=
362 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
363 | RedNode' _ _ _ t1 y t2 =>
364 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
365 | RedNode _ a x b => fun c d => {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
366 | t1' => fun t2 =>
367 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
368 | RedNode _ b x c => fun a d => {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
369 | b => fun a t => {<BlackNode a data b>}
370 end t1'
371 end t2
372 end.
373
374 Definition balance2 n (a : rtree n) (data : nat) c2 :=
375 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
376 | RedNode' _ _ _ t1 z t2 =>
377 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
378 | RedNode _ b y c => fun d a => {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
379 | t1' => fun t2 =>
380 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
381 | RedNode _ c z' d => fun b a => {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
382 | b => fun t a => {<BlackNode a data b>}
383 end t1'
384 end t2
385 end.
386
387 Section insert.
388 Variable x : nat.
389
390 Definition insResult c n :=
391 match c with
392 | Red => rtree n
393 | Black => { c' : color & rbtree c' n }
394 end.
395
396 Fixpoint ins c n (t : rbtree c n) {struct t} : insResult c n :=
397 match t in (rbtree c n) return (insResult c n) with
398 | Leaf => {< RedNode Leaf x Leaf >}
399 | RedNode _ a y b =>
400 if le_lt_dec x y
401 then RedNode' (projT2 (ins a)) y b
402 else RedNode' a y (projT2 (ins b))
403 | BlackNode c1 c2 _ a y b =>
404 if le_lt_dec x y
405 then
406 match c1 return insResult c1 _ -> _ with
407 | Red => fun ins_a => balance1 ins_a y b
408 | _ => fun ins_a => {< BlackNode (projT2 ins_a) y b >}
409 end (ins a)
410 else
411 match c2 return insResult c2 _ -> _ with
412 | Red => fun ins_b => balance2 ins_b y a
413 | _ => fun ins_b => {< BlackNode a y (projT2 ins_b) >}
414 end (ins b)
415 end.
416
417 Definition insertResult c n :=
418 match c with
419 | Red => rbtree Black (S n)
420 | Black => { c' : color & rbtree c' n }
421 end.
422
423 Definition makeBlack c n : insResult c n -> insertResult c n :=
424 match c return insResult c n -> insertResult c n with
425 | Red => fun r =>
426 match r in rtree n return insertResult Red n with
427 | RedNode' _ _ _ a x b => BlackNode a x b
428 end
429 | Black => fun r => r
430 end.
431
432 Implicit Arguments makeBlack [c n].
433
434 Definition insert c n (t : rbtree c n) : insertResult c n :=
435 makeBlack (ins t).
436
437 Fixpoint present c n (t : rbtree c n) {struct t} : bool :=
438 match t with
439 | Leaf => false
440 | RedNode _ a y b =>
441 if eq_nat_dec x y
442 then true
443 else if le_lt_dec x y
444 then present a
445 else present b
446 | BlackNode _ _ _ a y b =>
447 if eq_nat_dec x y
448 then true
449 else if le_lt_dec x y
450 then present a
451 else present b
452 end.
453
454 Definition rpresent n (t : rtree n) : bool :=
455 match t with
456 | RedNode' _ _ _ a y b =>
457 if eq_nat_dec x y
458 then true
459 else if le_lt_dec x y
460 then present a
461 else present b
462 end.
463 End insert.
464
465
466 Require Import Max Min.
467
468 Section depth.
469 Variable f : nat -> nat -> nat.
470
471 Fixpoint depth c n (t : rbtree c n) {struct t} : nat :=
472 match t with
473 | Leaf => 0
474 | RedNode _ t1 _ t2 => S (f (depth t1) (depth t2))
475 | BlackNode _ _ _ t1 _ t2 => S (f (depth t1) (depth t2))
476 end.
477 End depth.
478
479 Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
480 induction t; crush;
481 match goal with
482 | [ |- context[min ?X ?Y] ] => destruct (min_dec X Y)
483 end; crush.
484 Qed.
485
486 Lemma depth_max' : forall c n (t : rbtree c n), match c with
487 | Red => depth max t <= 2 * n + 1
488 | Black => depth max t <= 2 * n
489 end.
490 induction t; crush;
491 match goal with
492 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
493 end; crush.
494
495 destruct c1; crush.
496 destruct c2; crush.
497 Qed.
498
499 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
500 intros; generalize (depth_max' t); destruct c; crush.
501 Qed.
502
503 Theorem balanced : forall c n (t : rbtree c n), 2 * depth min t + 1 >= depth max t.
504 intros; generalize (depth_min t); generalize (depth_max t); crush.
344 Qed. 505 Qed.
345 506
346 507
347 (** * A Certified Regular Expression Matcher *) 508 (** * A Certified Regular Expression Matcher *)
348 509