Mercurial > cpdt > repo

comparison src/MoreDep.v @ 97:e579e1e64bde

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prettify rbtree a bit
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 22:05:37 -0400
parents b78a55b30f4a
children 696726af9530
comparison
equal deleted inserted replaced
96:b78a55b30f4a 97:e579e1e64bde
476 match c with 476 match c with
477 | Red => rbtree Black (S n) 477 | Red => rbtree Black (S n)
478 | Black => { c' : color & rbtree c' n } 478 | Black => { c' : color & rbtree c' n }
479 end. 479 end.
480 480
481 Definition makeBlack c n : insResult c n -> insertResult c n := 481 Definition makeRbtree c n : insResult c n -> insertResult c n :=
482 match c return insResult c n -> insertResult c n with 482 match c return insResult c n -> insertResult c n with
483 | Red => fun r => 483 | Red => fun r =>
484 match r in rtree n return insertResult Red n with 484 match r in rtree n return insertResult Red n with
485 | RedNode' _ _ _ a x b => BlackNode a x b 485 | RedNode' _ _ _ a x b => BlackNode a x b
486 end 486 end
487 | Black => fun r => r 487 | Black => fun r => r
488 end. 488 end.
489 489
490 Implicit Arguments makeBlack [c n]. 490 Implicit Arguments makeRbtree [c n].
491 491
492 Definition insert c n (t : rbtree c n) : insertResult c n := 492 Definition insert c n (t : rbtree c n) : insertResult c n :=
493 makeBlack (ins t). 493 makeRbtree (ins t).
494
495 Record rbtree' : Set := Rbtree' {
496 rtC : color;
497 rtN : nat;
498 rtT : rbtree rtC rtN
499 }.
500 494
501 Section present. 495 Section present.
502 Variable z : nat. 496 Variable z : nat.
503 497
504 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) , 498 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) ,
575 end 569 end
576 end; 570 end;
577 tauto. 571 tauto.
578 Qed. 572 Qed.
579 573
574 Ltac present_insert t :=
575 unfold insert; inversion t;
576 generalize (present_ins t); simpl;
577 dep_destruct (ins t); tauto.
578
580 Theorem present_insert_Red : forall n (t : rbtree Red n), 579 Theorem present_insert_Red : forall n (t : rbtree Red n),
581 present z (insert t) 580 present z (insert t)
582 <-> (z = x \/ present z t). 581 <-> (z = x \/ present z t).
583 unfold insert; inversion t; 582 intros; present_insert t.
584 generalize (present_ins t); simpl;
585 dep_destruct (ins t); tauto.
586 Qed. 583 Qed.
587 584
588 Theorem present_insert_Black : forall n (t : rbtree Black n), 585 Theorem present_insert_Black : forall n (t : rbtree Black n),
589 present z (projT2 (insert t)) 586 present z (projT2 (insert t))
590 <-> (z = x \/ present z t). 587 <-> (z = x \/ present z t).
591 unfold insert; inversion t; 588 intros; present_insert t.
592 generalize (present_ins t); simpl;
593 dep_destruct (ins t); tauto.
594 Qed. 589 Qed.
595 End present. 590 End present.
596 End insert. 591 End insert.
597 592
598 593