Some lib changes. Added basics.tt, fin.tt, pattern matching in lt.tt

darcs-hash:20070214010022-974a0-91b3647be1d8765a7e1ab24a311ba50a8831738a.gz

lib/basics.tt

@@ -0,0 +1,15 @@
+-- Some generally useful definitions
+-- Heterogeneous equality, nats, maybe, bools, lists.
+
+Load "eq.tt";
+Load "nat.tt";
+
+Data Maybe (A:*) : * 
+  = nothing : Maybe A
+  | just : (a:A)(Maybe A);
+
+Data Bool : * = true : Bool | false : Bool;
+
+Data List (A:*) : * 
+  = nil : List A
+  | cons : (x:A)->(xs:List A)->(List A);

lib/fin.tt

@@ -0,0 +1,15 @@
+Load "basics.tt";
+Load "lt.tt";
+
+Data Fin : (n:Nat)*
+    = fz : (k:Nat)(Fin (S k))
+    | fs : (k:Nat)(i:Fin k)(Fin (S k));
+
+Match weaken : (n:Nat)(i:Fin n)->(Fin (S n)) =
+    weaken _ (fz _) = fz _
+  | weaken _ (fs _ i) = fs _ (weaken _ i);
+
+Match fin2Nat : (n:Nat)(i:Fin n)->Nat =
+    fin2Nat _ (fz _) = O
+  | fin2Nat _ (fs _ i) = S (fin2Nat _ i);
+

lib/lt.tt

@@ -1,73 +1,43 @@
+Load "basics.tt";
+
 Data le : (m,n:Nat)* =
     leO : (n:Nat)(le O n)
   | leS : (m,n:Nat)(p:le m n)(le (S m) (S n));
 
-leSuc : (m,n:Nat)(p:le m n)(le m (S n));
-intros;
-induction p;
-intros;
-refine leO;
-intros;
-refine leS;
-refine p_IH;
-Qed;
+Match leSuc : (m,n:Nat)(p:le m n)(le m (S n)) =
+    leSuc _ _ (leO _) = leO _
+  | leSuc _ _ (leS _ _ p) = leS _ _ (leSuc _ _ p);
 
-leSym : (m:Nat)(le m m);
-intros;
-induction m;
-refine leO;
-intros;
-refine leS;
-refine k_IH;
-Qed;
+Match leSym : (m:Nat)(le m m) =
+    leSym O = leO _
+  | leSym (S k) = leS _ _ (leSym k);
 
-lePlus : (m,n:Nat)(le m (plus m n));
-intros;
-induction m;
-refine leO;
-intros;
-refine leS;
-fill k_IH;
-Qed;
+Match lePlus : (m,n:Nat)(le m (plus m n)) =
+    lePlus O n = leO _
+  | lePlus (S k) n = leS _ _ (lePlus k n);
 
 Data Compare : (m,n:Nat)* =
     cmpLT : (k,m:Nat)(Compare m (plus m (S k)))
   | cmpEQ : (n:Nat)(Compare n n)
   | cmpGT : (k,n:Nat)(Compare (plus n (S k)) n);
 
-compare : (m,n:Nat)(Compare m n);
-intro;
-induction m;
-intro;
-induction n;
-refine cmpEQ;
-intros;
-fill cmpLT k O;
-intros;
-induction n0;
-fill cmpGT k O;
-intros;
-induction (k_IH k0);
-intros;
-fill cmpLT k1 (S m1);
-intros;
-refine cmpEQ;
-intros;
-fill cmpGT k2 (S n2);
-Qed;
+Match compareAux : (m,n:Nat)(Compare m n)->(Compare (S m) (S n)) =
+    compareAux _ _ (cmpLT _ m) = cmpLT _ (S m)
+  | compareAux _ _ (cmpEQ n) = cmpEQ _
+  | compareAux _ _ (cmpGT _ n) = cmpGT _ (S n);
 
-mkLT : (m,n:Nat)(Maybe (le m n));
-intros;
-induction (compare m n);
-intros;
-refine just;
-refine lePlus;
-intros;
-refine just;
-refine leSym;
-intros;
-refine nothing;
-Qed;
+Match compare : (m,n:Nat)(Compare m n) =
+    compare O (S k) = cmpLT _ O
+  | compare O O = cmpEQ _
+  | compare (S k) O = cmpGT _ O
+  | compare (S x) (S y) = compareAux _ _ (compare x y);
+
+Match mkLTaux : (m,n:Nat)(Compare m n)->(Maybe (le m n)) =
+    mkLTaux _ _ (cmpLT k m) = just _ (lePlus m (S k))
+  | mkLTaux _ _ (cmpEQ m) = just _ (leSym m)
+  | mkLTaux _ _ (cmpGT k m) = nothing _;
+
+mkLT = [m,n:Nat](mkLTaux _ _ (compare m n));
 
 isBounded : (n,min,max:Nat)(Maybe (And (le min n) (le n max)));
 intros;

lib/vect.tt

@@ -1,13 +1,10 @@
-Load "nat.tt";
+Load "basics.tt";
+Load "fin.tt";
 
 Data Vect (A:*):(n:Nat)* 
     = vnil:Vect A O
     | vcons:(k:Nat)(x:A)(xs:Vect A k)Vect A (S k);
 
-Data Fin : (n:Nat)*
-    = fz : (k:Nat)(Fin (S k))
-    | fs : (k:Nat)(i:Fin k)(Fin (S k));
-
 Match lookup : (A:*)(n:Nat)(i:Fin n)(xs:Vect A n)A =
     lookup _ _ (fz _) (vcons _ _ x xs) = x
   | lookup _ _ (fs n i) (vcons _ n x xs) = lookup _ _ i xs;

tests/patt.tt

@@ -1,3 +1,4 @@
+Load "basics.tt";
 Load "vect.tt";
 
 Env = Vect *;
@@ -15,8 +16,6 @@ Match envlookup : (n:Nat)(i:Fin n)(G:Env n)(Gv:ValEnv n G)(vlookup _ _ i G) =
     envlookup _ (fz _) _ (extend _ t _ _ r) = t
   | envlookup _ (fs _ j) _ (extend _ t _ _ r) = envlookup _ j _ r;
 
-Data Bool : * = true:Bool | false:Bool;
-
 testEnv = vcons _ _ Nat (vcons _ _ Bool (vcons _ _ Nat (vnil *)));
 
 testValEnv : ValEnv _ testEnv;
@@ -29,11 +28,7 @@ fill (S (S O));
 refine empty;
 Qed;
 
-Data Le : (n:Nat)(m:Nat)* =
-   leO : (n:Nat)(Le O n)
- | leS : (n,m:Nat)(Le n m)->(Le (S n) (S m)); 
-
-Match minus : (m,n:Nat)(Le n m)->Nat =
+Match minus : (m,n:Nat)(le n m)->Nat =
     minus m O (leO m) = m
   | minus (S m) (S n) (leS n m p) = minus m n p;