### changeset 97:e579e1e64bde

Prettify rbtree a bit
author Adam Chlipala Tue, 07 Oct 2008 22:05:37 -0400 b78a55b30f4a 696726af9530 src/MoreDep.v 1 files changed, 10 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
```--- a/src/MoreDep.v	Tue Oct 07 21:58:45 2008 -0400
+++ b/src/MoreDep.v	Tue Oct 07 22:05:37 2008 -0400
@@ -478,7 +478,7 @@
| Black => { c' : color & rbtree c' n }
end.

-  Definition makeBlack c n : insResult c n -> insertResult c n :=
+  Definition makeRbtree c n : insResult c n -> insertResult c n :=
match c return insResult c n -> insertResult c n with
| Red => fun r =>
match r in rtree n return insertResult Red n with
@@ -487,16 +487,10 @@
| Black => fun r => r
end.

-  Implicit Arguments makeBlack [c n].
+  Implicit Arguments makeRbtree [c n].

Definition insert c n (t : rbtree c n) : insertResult c n :=
-    makeBlack (ins t).
-
-  Record rbtree' : Set := Rbtree' {
-    rtC : color;
-    rtN : nat;
-    rtT : rbtree rtC rtN
-  }.
+    makeRbtree (ins t).

Section present.
Variable z : nat.
@@ -577,20 +571,21 @@
tauto.
Qed.

+    Ltac present_insert t :=
+      unfold insert; inversion t;
+        generalize (present_ins t); simpl;
+          dep_destruct (ins t); tauto.
+
Theorem present_insert_Red : forall n (t : rbtree Red n),
present z (insert t)
<-> (z = x \/ present z t).
-      unfold insert; inversion t;
-        generalize (present_ins t); simpl;
-          dep_destruct (ins t); tauto.
+      intros; present_insert t.
Qed.

Theorem present_insert_Black : forall n (t : rbtree Black n),
present z (projT2 (insert t))
<-> (z = x \/ present z t).
-      unfold insert; inversion t;
-        generalize (present_ins t); simpl;
-          dep_destruct (ins t); tauto.
+      intros; present_insert t.
Qed.
End present.
End insert.```