Mercurial > cpdt > repo

comparison src/MoreDep.v @ 98:696726af9530

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prettify rbtree a bit more
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 22:14:39 -0400
parents e579e1e64bde
children 070f4de92311
comparison
equal deleted inserted replaced
97:e579e1e64bde 98:696726af9530
493 makeRbtree (ins t). 493 makeRbtree (ins t).
494 494
495 Section present. 495 Section present.
496 Variable z : nat. 496 Variable z : nat.
497 497
498 Ltac present_balance :=
499 crush;
500 repeat (match goal with
501 | [ H : context[match ?T with
502 | Leaf => _
503 | RedNode _ _ _ _ => _
504 | BlackNode _ _ _ _ _ _ => _
505 end] |- _ ] => dep_destruct T
506 | [ |- context[match ?T with
507 | Leaf => _
508 | RedNode _ _ _ _ => _
509 | BlackNode _ _ _ _ _ _ => _
510 end] ] => dep_destruct T
511 end; crush).
512
498 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) , 513 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) ,
499 present z (projT2 (balance1 a y b)) 514 present z (projT2 (balance1 a y b))
500 <-> rpresent z a \/ z = y \/ present z b. 515 <-> rpresent z a \/ z = y \/ present z b.
501 destruct a; crush; 516 destruct a; present_balance.
502 repeat match goal with
503 | [ H : context[match ?T with
504 | Leaf => _
505 | RedNode _ _ _ _ => _
506 | BlackNode _ _ _ _ _ _ => _
507 end] |- _ ] => pose T; dep_destruct T; crush
508 | [ |- context[match ?T with
509 | Leaf => _
510 | RedNode _ _ _ _ => _
511 | BlackNode _ _ _ _ _ _ => _
512 end] ] => pose T; dep_destruct T; crush
513 end.
514 Qed. 517 Qed.
515 518
516 Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) , 519 Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) ,
517 present z (projT2 (balance2 a y b)) 520 present z (projT2 (balance2 a y b))
518 <-> rpresent z a \/ z = y \/ present z b. 521 <-> rpresent z a \/ z = y \/ present z b.
519 destruct a; crush; 522 destruct a; present_balance.
520 repeat match goal with
521 | [ H : context[match ?T with
522 | Leaf => _
523 | RedNode _ _ _ _ => _
524 | BlackNode _ _ _ _ _ _ => _
525 end] |- _ ] => pose T; dep_destruct T; crush
526 | [ |- context[match ?T with
527 | Leaf => _
528 | RedNode _ _ _ _ => _
529 | BlackNode _ _ _ _ _ _ => _
530 end] ] => pose T; dep_destruct T; crush
531 end.
532 Qed. 523 Qed.
533 524
534 Definition present_insResult c n := 525 Definition present_insResult c n :=
535 match c return (rbtree c n -> insResult c n -> Prop) with 526 match c return (rbtree c n -> insResult c n -> Prop) with
536 | Red => fun t r => rpresent z r <-> z = x \/ present z t 527 | Red => fun t r => rpresent z r <-> z = x \/ present z t