diff src/MoreDep.v @ 98:696726af9530

Prettify rbtree a bit more
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 22:14:39 -0400
parents e579e1e64bde
children 070f4de92311
line wrap: on
line diff
--- a/src/MoreDep.v	Tue Oct 07 22:05:37 2008 -0400
+++ b/src/MoreDep.v	Tue Oct 07 22:14:39 2008 -0400
@@ -495,40 +495,31 @@
   Section present.
     Variable z : nat.
 
+    Ltac present_balance :=
+      crush;
+      repeat (match goal with
+                | [ H : context[match ?T with
+                                  | Leaf => _
+                                  | RedNode _ _ _ _ => _
+                                  | BlackNode _ _ _ _ _ _ => _
+                                end] |- _ ] => dep_destruct T
+                | [ |- context[match ?T with
+                                 | Leaf => _
+                                 | RedNode _ _ _ _ => _
+                                 | BlackNode _ _ _ _ _ _ => _
+                                 end] ] => dep_destruct T
+              end; crush).
+
     Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) ,
       present z (projT2 (balance1 a y b))
       <-> rpresent z a \/ z = y \/ present z b.
-      destruct a; crush;
-        repeat match goal with
-                 | [ H : context[match ?T with
-                                   | Leaf => _
-                                   | RedNode _ _ _ _ => _
-                                   | BlackNode _ _ _ _ _ _ => _
-                                 end] |- _ ] => pose T; dep_destruct T; crush
-                 | [ |- context[match ?T with
-                                  | Leaf => _
-                                  | RedNode _ _ _ _ => _
-                                  | BlackNode _ _ _ _ _ _ => _
-                                end] ] => pose T; dep_destruct T; crush
-               end.
+      destruct a; present_balance.
     Qed.
 
     Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) ,
       present z (projT2 (balance2 a y b))
       <-> rpresent z a \/ z = y \/ present z b.
-      destruct a; crush;
-        repeat match goal with
-                 | [ H : context[match ?T with
-                                   | Leaf => _
-                                   | RedNode _ _ _ _ => _
-                                   | BlackNode _ _ _ _ _ _ => _
-                                 end] |- _ ] => pose T; dep_destruct T; crush
-                 | [ |- context[match ?T with
-                                  | Leaf => _
-                                  | RedNode _ _ _ _ => _
-                                  | BlackNode _ _ _ _ _ _ => _
-                                end] ] => pose T; dep_destruct T; crush
-               end.
+      destruct a; present_balance.
     Qed.
 
     Definition present_insResult c n :=