wip19

1 files changed, 144 insertions, 25 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index bd55e69..335c653 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -342,9 +342,31 @@
     => (cut substitute <> (rule-rhs rl)))
    (else #f)))
 
-;; (system? x) -> boolean?
-;; system is alist
+
 (define (system? x)
+  (and (list? x)
+       (= 3 (length x))
+       (eq? 'system (list-ref x 0))
+       (system-definitions? (system-definitions x))
+       (system-proofs? (system-proofs x))))
+
+(define (system defs prfs)
+  (list 'system defs prfs))
+
+(define (system-definitions sys)
+  (list-ref sys 1))
+
+(define (system-proofs sys)
+  (list-ref sys 2))
+
+(define (lookup x sys)
+  (assoc x (system-definitions sys)))
+
+(define (find-proof x sys)
+  (assoc x (system-proofs sys)))
+
+;; (system-definitions? x) -> boolean?
+(define (system-definitions? x)
   (cond ((null? x) #t)
         ((pair? x)
          (and (pair? (car x))
@@ -352,7 +374,16 @@
                   (primitive-function? (car x))
                   (macro? (car x))
                   (function? (car x)))
-              (system? (cdr x))))
+              (system-definitions? (cdr x))))
+        (else #f)))
+
+;; (system-proofs? x) -> boolean?
+(define (system-proofs? x)
+  (cond ((null? x) #t)
+        ((pair? x)
+         (and (pair? (car x))
+              (proof? (car x))
+              (system-proofs? (cdr x))))
         (else #f)))
 
 (define (primitive-function? x)
@@ -751,10 +782,7 @@
                  (else
                   (fail "can't apply-primitive-function (~a)" cmd))))
                ((macro? x)
-                (cond
-                 ((apply-macro x extracted-expr) => identity)
-                 (else
-                  (fail "macro fail"))))
+                (fail "macro fail"))
                (else
                 (fail "rewrite error")))))
         (else (fail "no cmd (~a)" cmd)))))))
@@ -815,47 +843,62 @@
                      '()
                      (proposition-expression def)))
 
-(define current-system (make-parameter '()))
+(define current-system (make-parameter (system '() '())))
 
-(define (add-system x)
-  (let ((b (current-system)))
+(define (add-definition x)
+  (let ((sys (current-system)))
     (current-system
-     (cond ((assoc (proposition-name x) b)
+     (cond ((lookup (proposition-name x) sys)
             => (lambda (prop)
                  (if (equal? x prop)
-                     b
-                     (error "add-system: error"))))
-           (else (cons x b))))))
+                     sys
+                     (error "add-definition: error"))))
+           (else (system (cons x (system-definitions sys))
+                         (system-proofs sys)))))
+    x))
+
+(define (add-proof x)
+  (let ((sys (current-system)))
+    (current-system
+     (cond ((find-proof (proof-name x) sys)
+            => (lambda (prf)
+                 (if (equal? x prf)
+                     sys
+                     (error "add-proof: error"))))
+           (else (system (system-definitions sys)
+                         (cons x (system-proofs sys))))))
+    x))
 
 (define-syntax define-axiom
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (add-system (axiom 'name '(var ...) 'expr)))))
+     (add-definition (axiom 'name '(var ...) 'expr)))))
 
 (define-syntax define-theorem
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (add-system (theorem 'name '(var ...) 'expr)))))
+     (add-definition (theorem 'name '(var ...) 'expr)))))
 
 (define-syntax define-function
   (syntax-rules ()
     ((_ name (var ...) expr)
      (let ((f (function 'name '(var ...) 'expr)))
-       (add-system f)
+       (add-definition f)
        f))))
 
 (define-syntax define-macro
   (syntax-rules ()
     ((_ name () ((lhs1 . lhs2) rhs) ...)
-     (add-system (macro 'name
-                 (list (mrule '(lhs1 . lhs2) 'rhs)
-                       ...))))))
+     (add-definition (macro 'name
+                   (list (mrule '(lhs1 . lhs2) 'rhs)
+                         ...))))))
 
 (define-syntax define-system
   (syntax-rules ()
     ((_ name (systems ...) expr ...)
-     (define* (name #:optional (parent '()))
-       (parameterize ([current-system ((compose systems ... identity) parent)])
+     (define* (name #:optional (parent (system '() '())))
+       (parameterize ([current-system
+                       ((compose systems ... identity) parent)])
          expr
          ...
          (unless (system? (current-system))
@@ -1081,14 +1124,57 @@
                  (implies/if (if (null? app-forms)
                                  ''#t
                                  (fold implies/if c (map prop app-forms)))
-                         (if/if (if-form-test expr)
-                                (build (if-form-then expr))
-                                (build (if-form-else expr))))))
+                             (if/if (if-form-test expr)
+                                    (build (if-form-then expr))
+                                    (build (if-form-else expr))))))
               (else
                (let ((app-forms (find-app-forms expr)))
                  (fold implies/if c (map prop app-forms))))))))
      (else (error "make-induction-claim: fail<3>")))))
 
+(define (proof? x)
+  (and (list? x)
+       (= 4 (length x))
+       (symbol? (proof-name x))
+       (eq? 'proof (list-ref x 1))
+       (seed? (proof-seed x))
+       (sequence? (proof-sequence x))))
+
+(define (proof name seed sequence)
+  (list name 'proof seed sequence))
+
+(define (proof-name x)
+  (list-ref x 0))
+
+(define (proof-seed x)
+  (list-ref x 2))
+
+(define (proof-sequence x)
+  (list-ref x 3))
+
+(define seed? (const #t))
+
+(define-syntax define-proof
+  (syntax-rules (total natural? induction)
+    ((_ name
+        (total natural? (measure var ...))
+        (((n ...) cmd ...) ...))
+     (add-proof (proof 'name
+                       '(total natural? (measure var ...))
+                       '(((n ...) cmd ...) ...))))
+    ((_ name
+        (induction (f var ...))
+        (((n ...) cmd ...) ...))
+     (add-proof (proof 'name
+                       '(induction (f var ...))
+                       '(((n ...) cmd ...) ...))))
+    ((_ name
+        ()
+        (((n ...) cmd ...) ...))
+     (add-proof (proof 'name
+                       '()
+                       '(((n ...) cmd ...) ...))))))
+
 (define-system app/system (prelude)
   (define-function app (x y)
     (if (atom? x)
@@ -1099,6 +1185,39 @@
     (equal? (app (app x y) z)
             (app x (app y z))))
 
+  (define-proof app
+    (total natural? (size x))
+    (((2 3 2 1) app)
+     ((2 3 2 1) if-nest)
+     ((2 3 1 1) cdr/cons (set x (car a)))
+     ((2 3) if-same (set x (atom? (cons (car a) (app (cdr a) b)))))
+     ((2 3 3) size/cdr)
+     ((2 3 1) atom/cons)
+     ((2 3) if-false)
+     ((2) if-same)
+     (() if-same)))
+
+  (define-proof associate-app
+    (induction (list-induction x))
+    (((2 2) app)
+     ((2 2) if-nest-t)
+     ((2 1 1) app)
+     ((2 1 1) if-nest-t)
+     ((2) equal-same)
+     ((3 2 1 1) app)
+     ((3 2 1 1) if-nest-f)
+     ((3 2 2) app)
+     ((3 2 2) if-nest-f)
+     ((3 2 2 2) equal-if)
+     ((3 2 1) app)
+     ((3 2 1 3 1) car/cons)
+     ((3 2 1 3 2 1) cdr/cons)
+     ((3 2 1 1) atom/cons)
+     ((3 2 1) if-false)
+     ((3 2) equal-same)
+     ((3) if-same)
+     (() if-same)))
+
   #;
   (rewrite (app/system)
            '(if (natural? (size (app a b)))