Mercurial > cpdt > repo

comparison src/MoreDep.v @ 96:b78a55b30f4a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Move [present] section earlier
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 21:58:45 -0400
parents 7804f9d5249f
children e579e1e64bde
comparison
equal deleted inserted replaced
95:7804f9d5249f 96:b78a55b30f4a
396 396
397 397
398 Inductive rtree : nat -> Set := 398 Inductive rtree : nat -> Set :=
399 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n. 399 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
400 400
401 Section present.
402 Variable x : nat.
403
404 Fixpoint present c n (t : rbtree c n) {struct t} : Prop :=
405 match t with
406 | Leaf => False
407 | RedNode _ a y b => present a \/ x = y \/ present b
408 | BlackNode _ _ _ a y b => present a \/ x = y \/ present b
409 end.
410
411 Definition rpresent n (t : rtree n) : Prop :=
412 match t with
413 | RedNode' _ _ _ a y b => present a \/ x = y \/ present b
414 end.
415 End present.
416
401 Notation "{< x >}" := (existT _ _ x). 417 Notation "{< x >}" := (existT _ _ x).
402 418
403 Definition balance1 n (a : rtree n) (data : nat) c2 := 419 Definition balance1 n (a : rtree n) (data : nat) c2 :=
404 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with 420 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
405 | RedNode' _ _ _ t1 y t2 => 421 | RedNode' _ _ _ t1 y t2 =>
423 | RedNode _ c z' d => fun b a => {<RedNode (BlackNode a data b) z (BlackNode c z' d)>} 439 | RedNode _ c z' d => fun b a => {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
424 | b => fun a t => {<BlackNode t data (RedNode a z b)>} 440 | b => fun a t => {<BlackNode t data (RedNode a z b)>}
425 end t1' 441 end t1'
426 end t2 442 end t2
427 end. 443 end.
428
429 Section present.
430 Variable x : nat.
431
432 Fixpoint present c n (t : rbtree c n) {struct t} : Prop :=
433 match t with
434 | Leaf => False
435 | RedNode _ a y b => present a \/ x = y \/ present b
436 | BlackNode _ _ _ a y b => present a \/ x = y \/ present b
437 end.
438
439 Definition rpresent n (t : rtree n) : Prop :=
440 match t with
441 | RedNode' _ _ _ a y b => present a \/ x = y \/ present b
442 end.
443 End present.
444 444
445 Section insert. 445 Section insert.
446 Variable x : nat. 446 Variable x : nat.
447 447
448 Definition insResult c n := 448 Definition insResult c n :=