Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse code

Added a basic standard library path

Including nat, logic, john major equality etc.

darcs-hash:20061215161913-974a0-9fb142162870df48d10fce99c00abf8e21ee8c4b.gz
  • Loading branch information...
commit e45dc0ee77932191f028f6f3343ceba2c8ef1477 1 parent 67502b1
authored December 15, 2006
7  Ivor/Shell.lhs
@@ -12,7 +12,7 @@
12 12
 > -- Shell interface to theorem prover
13 13
 
14 14
 > module Ivor.Shell(ShellState,
15  
->                     runShell, importFile, addModulePath,
  15
+>                     runShell, importFile, addModulePath, prefix,
16 16
 >                     getContext, newShell, 
17 17
 >                     sendCommand, sendCommandIO, addTactic,
18 18
 >                     extendParser, configureEq,
@@ -25,6 +25,7 @@
25 25
 > import Ivor.Equality
26 26
 > import Ivor.Gadgets
27 27
 > import Ivor.Primitives
  28
+> import qualified Ivor.Prefix
28 29
 > -- import Ivor.Plugin
29 30
 
30 31
 > import IO
@@ -339,6 +340,10 @@ Special case for importFile. Grr.
339 340
 > gettacs :: [(String, String -> Goal -> Context -> IO Context)] -> [String]
340 341
 > gettacs = map fst
341 342
 
  343
+> -- | Get the install prefix of the library
  344
+> prefix :: FilePath
  345
+> prefix = Ivor.Prefix.prefix
  346
+
342 347
 If the given file is already loaded, do nothing.
343 348
 
344 349
 > -- | Import a file of shell commands; fails if the module does not exist 
3  Jones/Main.lhs
@@ -7,6 +7,7 @@ Simple program for starting up an interactive shell with Ivor library.
7 7
 > import Ivor.Shell
8 8
 
9 9
 > main :: IO ()
10  
-> main = do let shell = newShell emptyContext
  10
+> main = do let shell = addModulePath (newShell emptyContext) 
  11
+>                          (prefix ++ "/lib/ivor")
11 12
 >           ctxt <- runShell "> " shell
12 13
 >           putStrLn "Finished"
3  Makefile
@@ -6,11 +6,14 @@ PROFILE =
6 6
 GHCOPTS = 
7 7
 
8 8
 package:
  9
+	echo "module Ivor.Prefix where prefix = \"$(PREFIX)\"" > Ivor/Prefix.hs
9 10
 	runhaskell Setup.lhs configure --user --ghc --prefix=$(PREFIX) $(PROFILE)
10 11
 	runhaskell Setup.lhs build
11 12
 
12 13
 install: .PHONY
13 14
 	runhaskell Setup.lhs install $(DB)
  15
+	mkdir -p $(PREFIX)/lib/ivor
  16
+	install lib/* $(PREFIX)/lib/ivor
14 17
 
15 18
 unregister:
16 19
 	runhaskell Setup.lhs unregister $(DB)
8  TODO
... ...
@@ -1,5 +1,6 @@
1 1
 Short term things to do:
2 2
 
  3
+* Either String better rhan Monad m?
3 4
 * Fix naming bug --- terms of form t1 -> t2 automatically give t1 the
4 5
   name X, which can clash. Particularly a problem in data type declarations.
5 6
 * Current naive proof state representation is far too slow. Come up
@@ -29,12 +30,13 @@ Things which could be done to the library, in no particular order
29 30
 * Namespace management.
30 31
 * Some useful error messages from the Parsec parsers would be nice.
31 32
 * Proper type universes, of some form.
32  
-* Generate DRec as well as DElim/DCase.
33  
-* Build in Sigma types?
  33
+* Generate DRec and DNoConfusion as well as DElim/DCase.
  34
+* Build in Sigma types? (At least a nicer syntax?)
  35
+* Infix operators, especially = would be nice.
34 36
 
35 37
 Tactics:
36 38
 
37 39
 * Injectivity.
38 40
 * Discriminate.
39  
-* Inversion, likewise.
  41
+* Inversion.
40 42
 
2  ivor.cabal
@@ -20,5 +20,5 @@ Other-modules:	Ivor.Nobby, Ivor.TTCore, Ivor.State,
20 20
 		Ivor.CodegenC, Ivor.Datatype, Ivor.Display,
21 21
 		Ivor.ICompile, Ivor.MakeData, Ivor.Unify,
22 22
 		Ivor.Grouper, Ivor.ShellParser, Ivor.Constant,
23  
-		Ivor.RunTT, Ivor.Compiler
  23
+		Ivor.RunTT, Ivor.Compiler, Ivor.Prefix
24 24
 
31  lib/eq.tt
... ...
@@ -0,0 +1,31 @@
  1
+Equality Eq refl;
  2
+
  3
+repl : (A:*)(x:A)(y:A)(q:Eq _ _ x y)(P:(m:A)*)(p:P x)(P y);
  4
+intros;
  5
+by EqElim _ _ _ q;
  6
+fill p;
  7
+Qed;
  8
+Freeze repl;
  9
+
  10
+trans : (A:*)(a:A)(b:A)(c:A)(p:Eq _ _ a b)(q:Eq _ _ b c)(Eq _ _ a c);
  11
+intros;
  12
+by EqElim _ _ _ q;
  13
+fill p;
  14
+Qed;
  15
+Freeze trans;
  16
+
  17
+sym : (A:*)(a:A)(b:A)(p:Eq _ _ a b)(Eq _ _ b a);
  18
+intros;
  19
+by EqElim _ _ _ p;
  20
+refine refl;
  21
+Qed;
  22
+Freeze sym;
  23
+
  24
+Repl Eq repl sym;
  25
+
  26
+eq_resp_f:(A,B:*)(f:(a:A)B)(x:A)(y:A)(q:Eq _ _ x y)(Eq _ _ (f x) (f y));
  27
+intros;
  28
+by EqElim _ _ _ q;
  29
+refine refl;
  30
+Qed;
  31
+Freeze eq_resp_f;
5  lib/list.tt
... ...
@@ -0,0 +1,5 @@
  1
+Load "nat.tt";
  2
+
  3
+Data List (A:*) : *
  4
+  = nil : List A
  5
+  | cons : (x:A)->(xs:List A)->(List A);
39  lib/logic.tt
... ...
@@ -0,0 +1,39 @@
  1
+Data And (A:*)(B:*) : * = and_intro : (a:A)(b:B)(And A B);
  2
+
  3
+Data Or (A:*)(B:*) : * 
  4
+     = or_intro_l : (a:A)(Or A B)
  5
+     | or_intro_r : (b:B)(Or A B);
  6
+
  7
+Data Ex (A:*)(P:(a:A)*) : * = ex_intro : (x:A)(p:P x)(Ex A P);
  8
+
  9
+Data False : * = ;
  10
+
  11
+Data True : * = II : True ;
  12
+
  13
+not = [A:*](a:A)False;
  14
+
  15
+notElim = [A:*][p:not A][pp:A](p pp);
  16
+
  17
+Axiom classical:(P:*)(Or P (not P));
  18
+
  19
+and_commutes : (A:*)(B:*)(p:And A B)(And B A);
  20
+intros;
  21
+induction p;
  22
+intros;
  23
+refine and_intro;
  24
+fill b;
  25
+fill a;
  26
+Qed;
  27
+Freeze and_commutes;
  28
+
  29
+or_commutes : (A:*)(B:*)(p:Or A B)(Or B A);
  30
+intros;
  31
+induction p;
  32
+intros;
  33
+refine or_intro_r;
  34
+fill a;
  35
+intros;
  36
+refine or_intro_l;
  37
+fill b;
  38
+Qed;
  39
+Freeze or_commutes;
85  lib/lt.tt
... ...
@@ -0,0 +1,85 @@
  1
+Data le : (m,n:Nat)* =
  2
+    leO : (n:Nat)(le O n)
  3
+  | leS : (m,n:Nat)(p:le m n)(le (S m) (S n));
  4
+
  5
+leSuc : (m,n:Nat)(p:le m n)(le m (S n));
  6
+intros;
  7
+induction p;
  8
+intros;
  9
+refine leO;
  10
+intros;
  11
+refine leS;
  12
+refine p_IH;
  13
+Qed;
  14
+
  15
+leSym : (m:Nat)(le m m);
  16
+intros;
  17
+induction m;
  18
+refine leO;
  19
+intros;
  20
+refine leS;
  21
+refine k_IH;
  22
+Qed;
  23
+
  24
+lePlus : (m,n:Nat)(le m (plus m n));
  25
+intros;
  26
+induction m;
  27
+refine leO;
  28
+intros;
  29
+refine leS;
  30
+fill k_IH;
  31
+Qed;
  32
+
  33
+Data Compare : (m,n:Nat)* =
  34
+    cmpLT : (k,m:Nat)(Compare m (plus m (S k)))
  35
+  | cmpEQ : (n:Nat)(Compare n n)
  36
+  | cmpGT : (k,n:Nat)(Compare (plus n (S k)) n);
  37
+
  38
+compare : (m,n:Nat)(Compare m n);
  39
+intro;
  40
+induction m;
  41
+intro;
  42
+induction n;
  43
+refine cmpEQ;
  44
+intros;
  45
+fill cmpLT k O;
  46
+intros;
  47
+induction n0;
  48
+fill cmpGT k O;
  49
+intros;
  50
+induction (k_IH k0);
  51
+intros;
  52
+fill cmpLT k1 (S m1);
  53
+intros;
  54
+refine cmpEQ;
  55
+intros;
  56
+fill cmpGT k2 (S n2);
  57
+Qed;
  58
+
  59
+mkLT : (m,n:Nat)(Maybe (le m n));
  60
+intros;
  61
+induction (compare m n);
  62
+intros;
  63
+refine just;
  64
+refine lePlus;
  65
+intros;
  66
+refine just;
  67
+refine leSym;
  68
+intros;
  69
+refine nothing;
  70
+Qed;
  71
+
  72
+isBounded : (n,min,max:Nat)(Maybe (And (le min n) (le n max)));
  73
+intros;
  74
+induction mkLT min n;
  75
+refine nothing;
  76
+intros;
  77
+induction mkLT n max;
  78
+refine nothing;
  79
+intros;
  80
+refine just;
  81
+refine and_intro;
  82
+refine a;
  83
+refine a0;
  84
+Qed;
  85
+
182  lib/nat.tt
... ...
@@ -0,0 +1,182 @@
  1
+Load "eq.tt";
  2
+Load "logic.tt";
  3
+
  4
+Data Nat:* = O:Nat | S:(k:Nat)Nat;
  5
+
  6
+plus : (m:Nat)(n:Nat)Nat;
  7
+intro m;
  8
+induction m;
  9
+intros;
  10
+fill n;
  11
+intros;
  12
+fill S (k_IH n0);
  13
+Qed;
  14
+
  15
+mult : (m:Nat)(n:Nat)Nat;
  16
+intro m;
  17
+induction m;
  18
+intros;
  19
+fill O;
  20
+intros;
  21
+fill (plus n0 (k_IH n0));
  22
+Qed;
  23
+
  24
+simplifyO:(n:Nat)(Eq _ _ (plus O n) n);
  25
+intros;
  26
+refine refl;
  27
+Qed;
  28
+
  29
+simplifyS:(m,n:Nat)(Eq _ _ (plus (S m) n) (S (plus m n)));
  30
+intros;
  31
+refine refl;
  32
+Qed;
  33
+
  34
+eq_resp_S:(n:Nat)(m:Nat)(q:Eq _ _ n m)(Eq _ _ (S n) (S m));
  35
+intros;
  36
+fill (eq_resp_f _ _ S n m q);
  37
+Qed;
  38
+Freeze eq_resp_S;
  39
+
  40
+s_injective:(n:Nat)(m:Nat)(q:Eq _ _ (S n) (S m))(Eq _ _ n m);
  41
+intros;
  42
+local unS:(m:Nat)Nat;
  43
+intros;
  44
+induction m0;
  45
+fill n;
  46
+intros;
  47
+fill k;
  48
+fill eq_resp_f _ _ unS _ _ q;
  49
+Qed;
  50
+Freeze s_injective;
  51
+
  52
+notO_S:(k:Nat)(not (Eq _ _ O (S k)));
  53
+intros;
  54
+compute;
  55
+intro q;
  56
+local dmotive : (x:Nat)(q:Eq _ _ O x)*;
  57
+intros;
  58
+induction x;
  59
+fill True;
  60
+intros;
  61
+fill False;
  62
+fill EqElim _ _ _ q dmotive II;
  63
+Qed;
  64
+Freeze notO_S;
  65
+
  66
+notn_S:(n:Nat)(not (Eq _ _ n (S n)));
  67
+intro;
  68
+induction n;
  69
+fill notO_S O;
  70
+intros;
  71
+unfold not;
  72
+intros;
  73
+claim q:Eq _ _ k (S k);
  74
+fill k_IH q;
  75
+refine s_injective;
  76
+fill a;
  77
+Qed;
  78
+Freeze notn_S;
  79
+
  80
+discriminate_Nat:(A:*)(k:Nat)(q:Eq _ _ O (S k))A;
  81
+intros;
  82
+local false:False;
  83
+fill notO_S k q;
  84
+induction false;
  85
+Qed;
  86
+Freeze discriminate_Nat;
  87
+
  88
+plusnO:(n:Nat)(Eq _ _ (plus n O) n);
  89
+intro;
  90
+induction n;
  91
+refine refl;
  92
+intros;
  93
+equiv Eq _ _ (S (plus k O)) (S k);
  94
+refine eq_resp_S;
  95
+fill k_IH;
  96
+Qed;
  97
+Freeze plusnO;
  98
+
  99
+plusnSm:(n:Nat)(m:Nat)(Eq _ _ (plus n (S m)) (S (plus n m)));
  100
+intros;
  101
+induction n;
  102
+refine refl;
  103
+intros;
  104
+refine eq_resp_S;
  105
+fill k_IH;
  106
+Qed;
  107
+Freeze plusnSm;
  108
+
  109
+plus_comm:(n:Nat)(m:Nat)(Eq _ _ (plus n m) (plus m n));
  110
+intros;
  111
+induction n;
  112
+refine sym;
  113
+refine plusnO;
  114
+intros;
  115
+equiv Eq _ _ (S (plus k m)) (plus m (S k));
  116
+replace k_IH;
  117
+refine sym;
  118
+refine plusnSm;
  119
+Qed;
  120
+Freeze plus_comm;
  121
+
  122
+plus_assoc:(m,n,p:Nat)(Eq _ _ (plus m (plus n p)) (plus (plus m n) p));
  123
+intros;
  124
+induction m;
  125
+refine refl;
  126
+intros;
  127
+equiv Eq _ _ (S (plus k (plus n p))) (plus (S (plus k n)) p);
  128
+replace k_IH;
  129
+refine refl;
  130
+Qed;
  131
+Freeze plus_assoc;
  132
+
  133
+plus_eq_fst : (m,n,p:Nat)(q:Eq _ _ (plus p m) (plus p n))(Eq _ _ m n);
  134
+intro m n p;
  135
+induction p;
  136
+intros;
  137
+fill q;
  138
+intros;
  139
+refine k_IH;
  140
+refine s_injective;
  141
+refine q0;
  142
+Qed;
  143
+Freeze plus_eq_fst;
  144
+
  145
+plus_eq_fst_sym : (m,n,p:Nat)(q:Eq _ _ (plus m p) (plus n p))(Eq _ _ m n);
  146
+intro m n p;
  147
+replace plus_comm m p;
  148
+replace plus_comm n p;
  149
+fill plus_eq_fst m n p;
  150
+Qed;
  151
+Freeze plus_eq_fst_sym;
  152
+
  153
+multnO:(n:Nat)(Eq _ _ (mult n O) O);
  154
+intro;
  155
+induction n;
  156
+refine refl;
  157
+intros;
  158
+equiv Eq _ _ (plus O (mult k O)) O;
  159
+replace k_IH;
  160
+refine refl;
  161
+Qed;
  162
+Freeze multnO;
  163
+
  164
+multnSm:(n:Nat)(m:Nat)(Eq _ _ (mult n (S m)) (plus n (mult n m)));
  165
+intro;
  166
+induction n;
  167
+intros;
  168
+refine refl;
  169
+intros;
  170
+equiv Eq _ _ (S (plus m0 (mult k (S m0))))
  171
+             (S (plus k (plus m0 (mult k m0))));
  172
+refine eq_resp_S;
  173
+replace (k_IH m0);
  174
+generalise mult k m0;
  175
+intros;
  176
+replace (plus_comm m0 x);
  177
+replace (plus_assoc k x m0);
  178
+replace (plus_comm m0 (plus k x));
  179
+refine refl;
  180
+Qed;
  181
+Freeze multnSm;
  182
+
36  lib/vect.tt
... ...
@@ -0,0 +1,36 @@
  1
+Load "nat.tt";
  2
+
  3
+Data Vect (A:*):(n:Nat)* 
  4
+    = vnil:Vect A O
  5
+    | vcons:(k:Nat)(x:A)(xs:Vect A k)Vect A (S k);
  6
+
  7
+Data Fin : (n:Nat)*
  8
+    = fz : (k:Nat)(Fin (S k))
  9
+    | fs : (k:Nat)(i:Fin k)(Fin (S k));
  10
+
  11
+lookup:(A:*)(n:Nat)(i:Fin n)(xs:Vect A n)A;
  12
+local lookupAux:(A:*)(n:Nat)(i:Fin n)(n':Nat)(xs:Vect A n')(p:Eq _ n n')A;
  13
+intro A n i;
  14
+induction i;
  15
+intro k n' xs;
  16
+induction xs;
  17
+intros;
  18
+fill (discriminate_Nat _ _ (sym _ _ _ p));
  19
+intros;
  20
+fill x; {- fz (x::xs) -}
  21
+intro k i i_IH n' xs;
  22
+induction xs;
  23
+intros;
  24
+fill (discriminate_Nat _ _ (sym _ _ _ p0));
  25
+intros;
  26
+refine (i_IH k0);
  27
+fill xs0;
  28
+refine s_injective;
  29
+trivial;
  30
+intros;
  31
+refine (lookupAux _ _ i _ xs);
  32
+refine refl;
  33
+Qed;
  34
+
  35
+testvect = vcons _ _ O (vcons _ _ (S O) (vcons _ _ (S (S O)) (vnil Nat)));
  36
+testfin = fs _ (fz (S O));

0 notes on commit e45dc0e

Please sign in to comment.
Something went wrong with that request. Please try again.