wip21

4 files changed, 203 insertions, 212 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index 7007be4..4454e52 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -1,4 +1,4 @@
-;;; Vikalpa --- Prove S-expression
+;;; Vikalpa --- Proof Assistant
 ;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
 ;;;
 ;;; This file is part of Vikalpa.
@@ -18,8 +18,6 @@
 
 (define-module (vikalpa)
   #:export (rewrite)
-  #:use-module (vikalpa syntax)
-  #:use-module (vikalpa primitive)
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
   #:use-module (ice-9 control)
@@ -33,6 +31,22 @@
       (apply format #t f args)
       #t))
 
+(define-syntax-rule (define/guard (name (var pred?) ...) b b* ...)
+  (define (name var ...)
+    (unless (pred? var)
+      (error (format #f
+                     "~a:~%  expected:  ~a~%  given: "
+                     'name
+                     'pred?)
+             var))
+    ...
+    b b* ...))
+
+;; (natural? x) -> boolean?
+(define (natural? x)
+  (and (integer? x)
+       (not (negative? x))))
+
 (define (option p?)
   (lambda (x)
     (or (p? x) (not x))))
@@ -350,7 +364,7 @@
        (system-definitions? (system-definitions x))
        (system-proofs? (system-proofs x))))
 
-(define (system defs prfs)
+(define (make-system defs prfs)
   (list 'system defs prfs))
 
 (define (system-definitions sys)
@@ -370,7 +384,7 @@
   (cond ((null? x) #t)
         ((pair? x)
          (and (pair? (car x))
-              (or (proposition? (car x))
+              (or (theorem*? (car x))
                   (primitive-function? (car x))
                   (macro? (car x))
                   (function? (car x)))
@@ -567,7 +581,7 @@
           (expand* ms new-expr)))))
 
 ;; (axiom variable? vars? expression?) -> axiom?
-;; axiom? is proposition
+;; axiom? is theorem*
 (define/guard (axiom (name variable?) (vars vars?) (expr expression?))
   (list name 'axiom vars expr))
 
@@ -589,7 +603,7 @@
   (list name 'theorem vars expr))
 
 ;; (theorem? x) -> boolean?
-;; theorem? is proposition
+;; theorem? is theorem*
 (define (theorem? x)
   (and (list? x)
        (= 4 (length x))
@@ -601,24 +615,24 @@
 (define (theorem-name x)
   (list-ref x 0))
 
-;; (proposition? x) -> boolean?
-(define (proposition? x)
+;; (theorem*? x) -> boolean?
+(define (theorem*? x)
   (or (axiom? x)
       (theorem? x)))
 
-(define (proposition-name x)
+(define (theorem*-name x)
   (list-ref x 0))
 
-(define (proposition-vars x)
+(define (theorem*-vars x)
   (list-ref x 2))
 
-(define (proposition-expression x)
+(define (theorem*-expression x)
   (list-ref x 3))
 
-(define (proposition-rules x)
-  (expression->rules (proposition-vars x)
+(define (theorem*-rules x)
+  (expression->rules (theorem*-vars x)
                      '()
-                     (proposition-expression x)))
+                     (theorem*-expression x)))
 
 ;; (rewriter path? command?) -> rewriter?
 (define (rewriter p c)
@@ -724,11 +738,11 @@
               (cons (function-name f) args)
               '()))
 
-(define (parse-options/prop ops)
+(define (parse-options/theorem ops)
   (if (null? ops)
       (values '())
       (receive (env)
-          (parse-options/prop (cdr ops))
+          (parse-options/theorem (cdr ops))
         (case (caar ops)
           ((set) (let ((op (car ops)))
                    (cons (cons (list-ref op 1)
@@ -737,18 +751,17 @@
           (else
            (error "invalid option:" (car ops)))))))
 
-(define (rewrite/prop cmd b prop preconds expr fail)
+(define (rewrite/theorem cmd b thm preconds expr fail)
   (receive (env)
-      (parse-options/prop (command-options cmd))
+      (parse-options/theorem (command-options cmd))
     (cond
      ((any (cut apply-rule preconds <> expr env)
-           (proposition-rules prop)) => identity)
+           (theorem*-rules thm)) => identity)
      (else
       (fail (format #f "no match-rule (~a)" cmd))))))
 
-
 ;; (rewrite system? rewriter? expression? procedure?) -> expr
-(define (rewrite1 b expr fail r)
+(define (rewrite1 sys expr fail r)
   (let* ((cmd (rewriter-command r))
          (cmd/name (command-name cmd)))
     (debug "~%~%cmd: ~a~%" cmd)
@@ -757,19 +770,14 @@
         (extract (rewriter-path r) expr fail)
       (builder
        (cond
-        ((equal? cmd/name '(look))
-         (format #t "~y" extracted-expr)
-         (error "look"))
-        ((equal? cmd/name '(expand))
-         (expand (filter macro? b) extracted-expr))
-        ((equal? cmd/name '(expand*))
-         (expand* (filter macro? b) extracted-expr))
         ((and (symbol? cmd/name)
-              (assoc cmd/name b))
+              (lookup cmd/name sys))
          => (lambda (x)
               (cond
-               ((proposition? x) (rewrite/prop cmd b x preconds extracted-expr fail))
+               ((theorem*? x)
+                (rewrite/theorem cmd sys x preconds extracted-expr fail))
                ((function? x)
+                (debug "FUNCTION: ~y" x)
                 (cond
                  ((any (cut apply-rule '() <> extracted-expr '())
                        (function->rules x)) => identity)
@@ -787,14 +795,15 @@
                 (fail "rewrite error")))))
         (else (fail "no cmd (~a)" cmd)))))))
 
-(define/guard (rewrite (b system?) (expr expression?) (seq sequence?))
+(define/guard (rewrite (sys system?) (expr expression?) (seq sequence?))
+  (debug "rewrite ~y~%" expr)
   (let loop ((expr expr)
              (seq seq))
     (debug "~y~%" expr)
     #;(format #t "~y~%" expr)
     (if (null? seq)
         expr
-        (loop (rewrite1 b
+        (loop (rewrite1 sys
                         expr
                         (lambda (x . args)
                           (apply error
@@ -838,23 +847,23 @@
                       (expr-equal-lhs expr)))
           '())))
 
-(define (proposition->rules def)
-  (expression->rules (proposition-vars def)
+(define (theorem*->rules def)
+  (expression->rules (theorem*-vars def)
                      '()
-                     (proposition-expression def)))
+                     (theorem*-expression def)))
 
-(define current-system (make-parameter (system '() '())))
+(define current-system (make-parameter (make-system '() '())))
 
 (define (add-definition x)
   (let ((sys (current-system)))
     (current-system
-     (cond ((lookup (proposition-name x) sys)
-            => (lambda (prop)
-                 (if (equal? x prop)
+     (cond ((lookup (theorem*-name x) sys)
+            => (lambda (thm)
+                 (if (equal? x thm)
                      sys
                      (error "add-definition: error"))))
-           (else (system (cons x (system-definitions sys))
-                         (system-proofs sys)))))
+           (else (make-system (cons x (system-definitions sys))
+                              (system-proofs sys)))))
     x))
 
 (define (add-proof x)
@@ -865,38 +874,54 @@
                  (if (equal? x prf)
                      sys
                      (error "add-proof: error"))))
-           (else (system (system-definitions sys)
-                         (cons x (system-proofs sys))))))
+           (else (make-system (system-definitions sys)
+                              (cons x (system-proofs sys))))))
     x))
 
 (define-syntax define-axiom
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (add-definition (axiom 'name '(var ...) 'expr)))))
+     (let ((t (axiom 'name '(var ...) 'expr)))
+       (validate-theorem t)
+       (add-definition t)
+       t))))
 
 (define-syntax define-theorem
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (add-definition (theorem 'name '(var ...) 'expr)))))
+     (let ((t (theorem 'name '(var ...) 'expr)))
+       (validate-theorem t)
+       (add-definition t)
+       t))))
 
 (define-syntax define-function
   (syntax-rules ()
     ((_ name (var ...) expr)
      (let ((f (function 'name '(var ...) 'expr)))
+       (validate-function f)
+       (add-definition f)
+       f))))
+
+(define-syntax define-primitivge-function
+  (syntax-rules ()
+    ((_ name (p? ...) proc)
+     (let ((f (primitive-function 'name (list p? ...) proc)))
        (add-definition f)
        f))))
 
 (define-syntax define-macro
   (syntax-rules ()
     ((_ name () ((lhs1 . lhs2) rhs) ...)
-     (add-definition (macro 'name
-                   (list (mrule '(lhs1 . lhs2) 'rhs)
-                         ...))))))
+     (let ((m (macro 'name
+                (list (mrule '(lhs1 . lhs2) 'rhs)
+                      ...))))
+       (add-definition m)
+       m))))
 
 (define-syntax define-system
   (syntax-rules ()
     ((_ name (systems ...) expr ...)
-     (define* (name #:optional (parent (system '() '())))
+     (define* (name #:optional (parent (make-system '() '())))
        (parameterize ([current-system
                        ((compose systems ... identity) parent)])
          expr
@@ -908,7 +933,37 @@
 (define (atom? x)
   (not (pair? x)))
 
+(define (any? x) #t)
+
 (define-system prelude ()
+  (define-primitivge-function natural?
+    (any?)
+    natural?)
+
+  (define-primitivge-function equal?
+    (any? any?)
+    equal?)
+
+  (define-primitivge-function atom?
+    (any?)
+    (lambda (x) (not (pair? x))))
+
+  (define-primitivge-function cons
+    (any? any?)
+    cons)
+
+  (define-primitivge-function car
+    (pair?)
+    car)
+
+  (define-primitivge-function cdr
+    (pair?)
+    cdr)
+
+  (define-primitivge-function size
+    (any?)
+    size)
+  
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
 
@@ -1048,22 +1103,11 @@
    (else
     (if/if x y ''#t))))
 
-(define (make-totality-claim/natural m vars f)
+(define (make-total-claim/natural m vars f)
   (let ((name (function-name f))
-        (m-expr (cons (function-name m) vars)))
-    (define (convert app-form)
-      (cond
-       ((apply-rule '()
-                    (rule vars
-                          '()
-                          (cons (function-name f) vars)
-                          m-expr)
-                    app-form
-                    '())
-        => identity)
-       (else
-        (error "make-totality-claim/natural: fail<p>"))))
-    (if/if `(natural? ,(cons (function-name m) vars))
+        (m-expr (list (function-name m)
+                      (function-app-form f))))
+    (if/if `(natural? ,m-expr)
            (let loop ((expr (function-expression f)))
              (cond
               ((expr-quoted? expr) ''#t)
@@ -1084,13 +1128,15 @@
                               (else (and/if (loop (car args))
                                             (f (cdr args))))))))
                  (if (eq? name (app-form-name expr))
-                     (and/if `(< ,(convert expr) ,m-expr)
+                     (and/if `(< ,(list (function-name m) expr) ,m-expr)
                              rest)
                      rest)))
-              (else (error "(vikalpa) make-totality-claim: error"))))
+              (else (error "(vikalpa) make-total-claim: error"))))
            ''#t)))
 
-(define (make-induction-claim f vars t)
+(define/guard (make-induction-claim (f function*?)
+                                    (vars (list-of variable?))
+                                    (t theorem?))
   (define (find-app-forms expr)
     (cond
      ((app-form? expr)
@@ -1101,7 +1147,7 @@
      ((if-form? expr)
       (error "make-induction-claim: FAILED m(- -)m"))
      (else '())))
-  (let ((c (proposition-expression t)))
+  (let ((c (theorem*-expression t)))
     (define (prop app-form)
       (cond
        ((apply-rule '()
@@ -1130,7 +1176,8 @@
               (else
                (let ((app-forms (find-app-forms expr)))
                  (fold implies/if c (map prop app-forms))))))))
-     (else (error "make-induction-claim: fail<3>")))))
+     (else (error "make-induction-claim: invalid"
+                  f vars t)))))
 
 (define (proof? x)
   (and (list? x)
@@ -1175,6 +1222,81 @@
                        '()
                        '(((n ...) cmd ...) ...))))))
 
+(define (function*? x)
+  (or (function? x)
+      (primitive-function? x)))
+
+(define (validate-function f)
+  (let ((fexpr (function-expression f))
+        (fvars (function-vars f))
+        (fname (function-name f)))
+    (for-each (lambda (x)
+                (unless (cond
+                         ((lookup x (current-system)) => function*?)
+                         (else (eq? fname x)))
+                  (error (format #f "(vikalpa) ~a: undefined function" fname)
+                         x)))
+              (expression-functions fexpr))
+    (for-each (lambda (x)
+                (unless (member x fvars)
+                  (error (format #f "(vikalpa) ~a: undefined variable" fname)
+                         x)))
+              (expression-vars fexpr))))
+
+(define (validate-theorem t)
+  (let ((texpr (function-expression t))
+        (tvars (function-vars t))
+        (tname (function-name t)))
+    (for-each (lambda (x)
+                (unless (cond ((lookup x (current-system)) => function*?)
+                              (else #f))
+                  (error (format #f "~a: undefined function" tname)
+                         x)))
+              (expression-functions texpr))
+    (for-each (lambda (x)
+                (unless (member x tvars)
+                  (error (format #f "~a: undefined variable" tname)
+                         x)))
+              (expression-vars texpr))))
+
+(define (trivial-total? f)
+  (not (member (function-name f)
+               (expression-functions (function-expression f)))))
+
+(define (prove sys def pf)
+  (cond
+   ((theorem? def)
+    (prove/theorem sys def pf))
+   ((function? def)
+    (prove/function sys def pf))
+   (else (error "prove" def pf))))
+
+(define (prove/theorem sys t pf)
+  (match (proof-seed pf)
+    (('induction (f . vars))
+     (rewrite sys
+              (make-induction-claim (lookup f sys)
+                                    vars
+                                    t)
+              (proof-sequence pf)))
+    (()
+     (rewrite sys
+              (theorem*-expression pf)
+              (proof-sequence pf)))
+    (else
+     (error "prove/theorem: fail"))))
+
+(define (prove/function sys f pf)
+  (match (proof-seed pf)
+    (('total 'natural? (m . vars))
+     (rewrite sys
+              (make-total-claim/natural (lookup m sys)
+                                        vars
+                                        f)
+              (proof-sequence pf)))
+    (else
+     (error "prove/function: fail"))))
+
 (define-system app/system (prelude)
   (define-function app (x y)
     (if (atom? x)
@@ -1189,16 +1311,17 @@
     (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 1 1) cdr/cons (set x (car x)))
+     ((2 3) if-same (set x (atom? (cons (car x) (app (cdr x) y)))))
      ((2 3 3) size/cdr)
      ((2 3 1) atom/cons)
      ((2 3) if-false)
      ((2) if-same)
-     (() if-same)))
+     (() if-same)
+     ))
 
   (define-proof associate-app
-    (induction (list-induction x))
+    (induction (app x y))
     (((2 2) app)
      ((2 2) if-nest-t)
      ((2 1 1) app)
@@ -1226,6 +1349,9 @@
       0))
 
 (define (app x y)
-    (if (atom? x)
-        y
-        (cons (car x) (app (cdr x) y))))
+  (if (atom? x)
+      y
+      (cons (car x) (app (cdr x) y))))
+
+;; (define (review sys)
+;;   )
diff --git a/vikalpa/ord.scm b/vikalpa/ord.scm
deleted file mode 100644
index 9715979..0000000
--- a/vikalpa/ord.scm
+++ /dev/null
@@ -1,79 +0,0 @@
-;;; Vikalpa --- Prove S-expression
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
-;;;
-;;; This file is part of Vikalpa.
-;;;
-;;; Vikalpa is free software; you can redistribute it and/or modify it
-;;; under the terms of the GNU General Public License as published by
-;;; the Free Software Foundation; either version 3 of the License, or
-;;; (at your option) any later version.
-;;;
-;;; Vikalpa is distributed in the hope that it will be useful, but
-;;; WITHOUT ANY WARRANTY; without even the implied warranty of
-;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-;;; General Public License for more details.
-;;;
-;;; You should have received a copy of the GNU General Public License
-;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
-
-(define-module (vikalpa ord)
-  #:export (ord?
-            ord-fin?
-            ord-inf?
-            ord-first-expt
-            ord-first-coeff
-            ord-rest
-            ord<)
-  #:use-module (vikalpa syntax)
-  #:use-module (vikalpa primitive))
-
-;;; ACL2's O-p
-;; https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____O-P?path=3574/6842/3819/225/243
-(define (ord? x)
-  (if (ord-fin? x)
-      (natural? x)
-      (and (pair? (car x))
-           (ord? (ord-first-expt x))
-           (not (eqv? 0 (ord-first-expt x)))
-           (positive? (ord-first-coeff x))
-           (ord< (ord-first-expt (ord-rest x))
-                 (ord-first-expt x)))))
-
-(define/guard (ord (first-expt ord?) (first-coeff positive?) (rest ord?))
-  (cons (cons first-expt first-coeff) rest))
-
-(define (ord-fin? x)
-  (not (pair? x)))
-
-(define (ord-inf? x)
-  (pair? x))
-
-(define (ord-first-expt x)
-  (if (ord-fin? x)
-      0
-      (caar x)))
-
-(define (ord-first-coeff x)
-  (if (ord-fin? x)
-      x
-      (cdar x)))
-
-(define (ord-rest x)
-  (cdr x))
-
-(define (ord< x y)
-  (cond ((ord-fin? x)
-         (or (ord-inf? y)
-             (< x y)))
-        ((ord-fin? y) #f)
-        ((not (equal? (ord-first-expt x)
-                      (ord-first-expt y)))
-         (ord< (ord-first-expt x)
-               (ord-first-expt y)))
-        ((not (= (ord-first-coeff x)
-                 (ord-first-coeff y)))
-         (< (ord-first-coeff x)
-            (ord-first-coeff y)))
-        (else
-         (ord< (ord-rest x)
-               (ord-rest y)))))
diff --git a/vikalpa/primitive.scm b/vikalpa/primitive.scm
deleted file mode 100644
index bcbced5..0000000
--- a/vikalpa/primitive.scm
+++ /dev/null
@@ -1,25 +0,0 @@
-;;; Vikalpa --- Proof Assistant
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
-;;;
-;;; This file is part of Vikalpa.
-;;;
-;;; Vikalpa is free software; you can redistribute it and/or modify it
-;;; under the terms of the GNU General Public License as published by
-;;; the Free Software Foundation; either version 3 of the License, or
-;;; (at your option) any later version.
-;;;
-;;; Vikalpa is distributed in the hope that it will be useful, but
-;;; WITHOUT ANY WARRANTY; without even the implied warranty of
-;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-;;; General Public License for more details.
-;;;
-;;; You should have received a copy of the GNU General Public License
-;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
-
-(define-module (vikalpa primitive)
-  #:export (natural?))
-
-;; (natural? x) -> boolean?
-(define (natural? x)
-  (and (integer? x)
-       (not (negative? x))))
diff --git a/vikalpa/syntax.scm b/vikalpa/syntax.scm
deleted file mode 100644
index 046c13a..0000000
--- a/vikalpa/syntax.scm
+++ /dev/null
@@ -1,31 +0,0 @@
-;;; Vikalpa --- Prove S-expression
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
-;;;
-;;; This file is part of Vikalpa.
-;;;
-;;; Vikalpa is free software; you can redistribute it and/or modify it
-;;; under the terms of the GNU General Public License as published by
-;;; the Free Software Foundation; either version 3 of the License, or
-;;; (at your option) any later version.
-;;;
-;;; Vikalpa is distributed in the hope that it will be useful, but
-;;; WITHOUT ANY WARRANTY; without even the implied warranty of
-;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-;;; General Public License for more details.
-;;;
-;;; You should have received a copy of the GNU General Public License
-;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
-
-(define-module (vikalpa syntax)
-  #:export (define/guard))
-
-(define-syntax-rule (define/guard (name (var pred?) ...) b b* ...)
-  (define (name var ...)
-    (unless (pred? var)
-      (error (format #f
-                     "~a:~%  expected:  ~a~%  given: "
-                     'name
-                     'pred?)
-             var))
-    ...
-    b b* ...))