From d75c913a514c3a4299502a93d3025b03d2320109 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 20 Nov 2020 13:33:07 +0900
Subject: wip27

---
 vikalpa.scm         | 320 ++++++++++++++++++++++++++--------------------------
 vikalpa/prelude.scm | 145 +++++++++++++++++++++---
 2 files changed, 285 insertions(+), 180 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index fcb9005..74dbe6c 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -21,12 +21,22 @@
             show
             check
             system->scheme
+            load-system
+            system-primitives
+            system-functions
+            system-macros
+            system-theorems
+            system-axioms
             define-system
             define-axiom
             define-theorem
             define-primitive-function
             define-function
-            define-syntax-rules)
+            define-proof
+            define-syntax-rules
+            total/natural?
+            induction
+            size add1 sub1 natural?)
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
   #:use-module (ice-9 control)
@@ -55,7 +65,7 @@
 
 ;; (natural? x) -> boolean?
 (define (natural? x)
-  (and (integer? x)
+  (and (exact-integer? x)
        (not (negative? x))))
 
 (define (option p?)
@@ -70,7 +80,7 @@
 ;; (expression? x) -> boolean?
 (define (expression? expr)
   (cond ((expr-quoted? expr)
-         (or (integer? (expr-unquote expr))
+         (or (natural? (expr-unquote expr))
              (boolean? (expr-unquote expr))
              (symbol? (expr-unquote expr))
              (null? (expr-unquote expr))))
@@ -440,19 +450,21 @@
 
 (define (function? x)
   (and (list? x)
-       (= 5 (length x))
+       (= 6 (length x))
        (variable? (function-name x))
        (eq? 'function (list-ref x 1))
        (vars? (function-vars x))
        (expression? (function-expression x))
-       ((const #t) (function-code x))))
+       ((const #t) (function-code x))
+       (boolean? (function-primitive? x))))
 
 ;; (function variable? vars? expression?) -> function?
 (define/guard (function (name variable?)
                         (vars vars?)
                         (expr expression?)
-                        (code any?))
-  (list name 'function vars expr code))
+                        (code any?)
+                        (primitive boolean?))
+  (list name 'function vars expr code primitive))
 
 (define (function-name f)
   (list-ref f 0))
@@ -466,6 +478,9 @@
 (define (function-code f)
   (list-ref f 4))
 
+(define (function-primitive? f)
+  (list-ref f 5))
+
 (define (definition-name d)
   (list-ref d 0))
 
@@ -660,10 +675,37 @@
           (expand-let (cdr x))))
    (else x)))
 
+(define (natural->expr n)
+  (if (zero? n)
+      ''0
+      `(add1 ,(natural->expr (sub1 n)))))
+
+(define (pair->expr x)
+  (if (pair? x)
+      `(cons ,(pair->expr (car x))
+             ,(pair->expr (cdr x)))
+      (expr-quote x)))
+
+(define (expand-quoted x)
+  (cond
+   ((expr-quoted? x)
+    (let ((val (expr-unquote x)))
+      (cond
+       ((natural? val)
+        (natural->expr val))
+       ((pair? val)
+        (pair->expr val))
+       (else x))))
+   ((pair? x)
+    (cons (expand-quoted (car x))
+          (expand-quoted (cdr x))))
+   (else x)))
+
 (define (convert-to-expression x)
-  (quote-all
-   (expand* (filter macro? (system-definitions (current-system)))
-            (expand-let x))))
+  (expand-quoted
+   (quote-all
+    (expand* (filter macro? (system-definitions (current-system)))
+             (expand-let x)))))
 
 ;; (axiom variable? vars? expression?) -> axiom?
 ;; axiom? is theorem*
@@ -843,7 +885,7 @@
      ((any (cut apply-rule preconds <> expr env)
            (theorem*-rules thm)) => identity)
      (else
-      (fail (format #f "no match-rule (~a)" cmd))))))
+      (fail (format #f "no match theorem ~a: ~s" cmd expr))))))
 
 ;; (rewrite system? rewriter? expression? procedure?) -> expr
 (define (rewrite1 sys expr fail r)
@@ -854,6 +896,12 @@
         (extract (rewriter-path r) expr fail)
       (builder
        (cond
+        ((eq? 'equal? cmd/name)
+         (match extracted-expr
+           (('equal? `(quote ,x) `(quote ,y))
+            (expr-quote (equal? x y)))
+           (else
+            (fail "error: equal? ~a" extracted-expr))))
         ((and (symbol? cmd/name)
               (lookup cmd/name sys))
          => (lambda (x)
@@ -868,7 +916,7 @@
                   (fail (format #f "no match-function (~a)" cmd)))))
                (else
                 (fail "rewrite error" cmd)))))
-        (else (fail "no cmd (~a)" cmd)))))))
+        (else (fail "no cmd" cmd extracted-expr)))))))
 
 (define/guard (rewrite (sys system?) (expr expression?) (seq sequence?))
   (debug "rewrite ~y~%" expr)
@@ -953,8 +1001,9 @@
                               (cons x (system-proofs sys))))))
     x))
 
+(define reserved-symbols '(quote let if))
 (define (reserved? x)
-  (member x '(if quote let)))
+  (member x reserved-symbols))
 
 (define-syntax define-axiom
   (syntax-rules ()
@@ -979,7 +1028,8 @@
     ((_ name (var ...) expr)
      (let ((f (function 'name '(var ...)
                         (convert-to-expression 'expr)
-                        'expr)))
+                        'expr
+                        #f)))
        (add-definition f)
        (validate-definition f)
        f))))
@@ -989,6 +1039,14 @@
     ((_ name (var ...))
      (let ((f (primitive-function 'name '(var ...))))
        (add-definition f)
+       f))
+    ((_ name (var ...) expr)
+     (let ((f (function 'name '(var ...)
+                        (convert-to-expression 'expr)
+                        'expr
+                        '#t)))
+       (add-definition f)
+       (validate-definition f)
        f))))
 
 (define-syntax define-syntax-rules
@@ -1001,114 +1059,63 @@
        (add-definition m)
        m))))
 
+(define (size x)
+  (if (pair? x)
+      (+ 1
+         (size (car x))
+         (size (cdr x)))
+      0))
+(define (add1 n) (1+ n))
+(define (sub1 n) (1- n))
+
+(define (core-primitive-function)
+  (list (primitive-function 'not '(x))
+        (primitive-function 'equal? '(x y))
+        (primitive-function 'pair? '(x))
+        (primitive-function 'cons '(x y))
+        (primitive-function 'car '(x))
+        (primitive-function 'cdr '(x))
+        (primitive-function 'size '(x))
+        (primitive-function 'natural? '(x))
+        (primitive-function 'add1 '(x))
+        (primitive-function 'sub1 '(x))
+        (primitive-function '< '(x y))))
+
+(define* (empty-system #:optional (parent (make-system '() '())))
+  (parameterize ([current-system parent])
+    (define-primitive-function not (x))
+    (define-primitive-function equal? (x y))
+    (define-primitive-function pair? (x))
+    (define-primitive-function cons (x y))
+    (define-primitive-function car (x))
+    (define-primitive-function cdr (x))
+    (define-primitive-function size (x))
+    (define-primitive-function natural? (x))
+    (define-primitive-function add1 (x))
+    (define-primitive-function sub1 (x))
+    (define-primitive-function < (x y))
+    (unless (system? (current-system))
+      (error "define-system: error"))
+    (current-system)))
+
 (define-syntax define-system
   (syntax-rules ()
     ((_ name (systems ...) expr ...)
      (define* (name #:optional (parent (make-system '() '())))
        (parameterize ([current-system
-                       ((compose systems ... identity) parent)])
+                       ((compose systems ... empty-system) parent)])
          expr
          ...
          (unless (system? (current-system))
            (error "define-system: error"))
          (current-system))))))
 
-(define-syntax system
-  (syntax-rules ()
-    ((_ (systems ...) expr ...)
-     (let ()
-       (parameterize ([current-system
-                       ((compose systems ... identity) (make-system '() '()))])
-         expr
-         ...
-         (unless (system? (current-system))
-           (error "define-system: error"))
-         (current-system))))))
 
 (define (atom? x)
   (not (pair? x)))
 
 (define (any? x) #t)
 
-(define-system prelude ()
-  (define-primitive-function natural? (x))
-  (define-primitive-function equal? (x y))
-  (define-primitive-function atom? (x))
-  (define-primitive-function cons (x y))
-  (define-primitive-function car (x))
-  (define-primitive-function cdr (x))
-  (define-primitive-function size (x))
-  (define-primitive-function < (x y))
-  (define-primitive-function not (x))
-
-  (define-axiom equal-same (x)
-    (equal? (equal? x x) '#t))
-  (define-axiom equal-swap (x y)
-    (equal? (equal? x y) (equal? y x)))
-  (define-axiom equal-if (x y)
-    (if (equal? x y) (equal? x y) '#t))
-  (define-axiom atom/cons (x y)
-    (equal? (atom? (cons x y)) '#f))
-  (define-axiom car/cons (x y)
-    (equal? (car (cons x y)) x))
-  (define-axiom cdr/cons (x y)
-    (equal? (cdr (cons x y)) y))
-  (define-axiom cons/car+cdr (x)
-    (if (atom? x)
-        '#t
-        (equal? (cons (car x) (cdr x)) x)))
-  (define-axiom if-nest (x y z)
-    (if x
-        (equal? (if x y z) y)
-        (equal? (if x y z) z)))
-  (define-axiom if-nest-t (x y z)
-    (if x
-        (equal? (if x y z) y)
-        '#t))
-  (define-axiom if-nest-f (x y z)
-    (if x
-        '#t
-        (equal? (if x y z) z)))
-  (define-axiom if-false (x y)
-    (equal? (if '#f x y) y))
-  (define-axiom if-same (x y)
-    (equal? (if x y y) y))
-  (define-axiom natural/size (x)
-    (equal? (natural? (size x))
-            '#t))
-  (define-axiom size/car (x)
-    (if (atom? x)
-        '#t
-        (equal? (< (size (car x)) (size x))
-                '#t)))
-  (define-axiom size/cdr (x)
-    (if (atom? x)
-        '#t
-        (equal? (< (size (cdr x)) (size x))
-                '#t)))
-  (define-axiom if-not (x y z)
-    (equal? (if (not x) y z)
-            (if x z y)))
-
-  (define-syntax-rules list ()
-    ((list) '())
-    ((list x . y) (cons x (list . y))))
-
-  (define-syntax-rules and ()
-    ((and) '#t)
-    ((and x) x)
-    ((and x . xs) (if x (and . xs) #f)))
-
-  (define-syntax-rules or ()
-    ((or) '#f)
-    ((or x) x)
-    ((or x . xs) (if x x (or . xs))))
-
-  (define-syntax-rules cond (else)
-    ((cond (else e)) e)
-    ((cond (test then) . rest)
-     (if test then (cond . rest)))))
-
 (define (measure? x)
   (and (pair? x)
        (variable? (car x))
@@ -1157,9 +1164,8 @@
    (else
     (if/if x y ''#t))))
 
-(define (make-total-claim/natural m vars f)
-  (let ((name (function-name f))
-        (m-expr (cons (function-name m) vars)))
+(define (make-total-claim/natural m-expr f)
+  (let* ((name (function-name f)))
     (define (convert app-form)
       (cond
        ((apply-rule '()
@@ -1269,10 +1275,10 @@
 (define-syntax define-proof
   (syntax-rules (total natural? induction)
     ((_ name
-        (total natural? (measure var ...))
+        (total/natural? m-expr)
         (((n ...) cmd ...) ...))
      (add-proof (proof 'name
-                       '(total natural? (measure var ...))
+                       '(total/natural? m-expr)
                        '(((n ...) cmd ...) ...))))
     ((_ name
         (induction (f var ...))
@@ -1346,11 +1352,9 @@
 
 (define (prove/function sys f pf)
   (match (proof-seed pf)
-    (('total 'natural? (m . vars))
+    (('total/natural? m-expr)
      (rewrite sys
-              (make-total-claim/natural (lookup m sys)
-                                        vars
-                                        f)
+              (make-total-claim/natural m-expr f)
               (proof-sequence pf)))
     (else
      (error "prove/function: fail"))))
@@ -1360,52 +1364,10 @@
      ,@(map (lambda (f)
               `(define (,(function-name f) ,@(function-vars f))
                  ,(function-code f)))
-            (reverse (filter function? (system-definitions sys))))))
-
-(define-system app/system (prelude)
-  (define-function app (x y)
-    (cond
-     ((atom? x) y)
-     (else
-      (cons (car x) (app (cdr x) y)))))
-
-  (define-theorem associate-app (x y z)
-    (equal? (app (app x y) z)
-            (app x (app y z))))
-
-  (define-proof app
-    (total natural? (size x))
-    (((2 3) size/cdr)
-     ((2) if-same)
-     (() if-same)))
-    
-  (define-proof associate-app
-    (induction (app x y))
-    (((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))))
-
-(define (size x)
-  (if (pair? x)
-      (+ 1
-         (size (car x))
-         (size (cdr x)))
-      0))
+            (reverse (filter (lambda (x)
+                               (and (function? x)
+                                    (not (function-primitive? x))))
+                             (system-definitions sys))))))
 
 (define/guard (check (sys system?))
   (let loop ((sys sys)
@@ -1424,6 +1386,7 @@
         (cond
          ((and (function? (car defs))
                (trivial-total? (car defs)))
+          #;
           (format #t "`~a` is trivial total function.~%"
                   (definition-name (car defs)))
           (next))
@@ -1434,6 +1397,7 @@
                  (let ((result (prove sys (car defs) pf)))
                    (cond
                     ((equal? result ''#t)
+                     #;
                      (format #t "`~a` is ~a.~%"
                              (definition-name (car defs))
                              (if (function? (car defs))
@@ -1441,14 +1405,17 @@
                                  "true"))
                      (next))
                     (else
+                     #;
                      (format #t "`~a`'s proof is failed:~%~y"
                              (definition-name (car defs))
                              result)
-                     (next (definition-name (car defs))))))))
+                     (next (list (definition-name (car defs))
+                                 result)))))))
            (else
+            #;
             (format #t "`~a`'s proof is not found.~%"
                     (definition-name (car defs)))
-            (next (definition-name (car defs))))))))
+            (next (list (definition-name (car defs)))))))))
        (else
         (next))))))
 
@@ -1485,3 +1452,32 @@
            (error "show: error")))))
    (else
     (format #t "~a: not found~%" name))))
+
+(define/guard (load-system (sys system?))
+  (primitive-eval (system->scheme sys)))
+
+(define/guard (system-primitives (sys system?))
+  (append reserved-symbols
+          (map primitive-function-name
+               (filter primitive-function?
+                       (system-definitions sys)))))
+
+(define/guard (system-functions (sys system?))
+  (map function-name
+       (filter function?
+               (system-definitions sys))))
+
+(define/guard (system-theorems (sys system?))
+  (map theorem-name
+       (filter theorem?
+               (system-definitions sys))))
+
+(define/guard (system-axioms (sys system?))
+  (map theorem*-name
+       (filter axiom?
+               (system-definitions sys))))
+
+(define/guard (system-macros (sys system?))
+  (map macro-name
+       (filter macro?
+               (system-definitions sys))))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 874614d..264773d 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -17,7 +17,7 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (atom? natural? size implies prelude)
+  #:export (atom? size implies natural? prelude)
   #:use-module (vikalpa))
 
 (define (atom? x)
@@ -41,17 +41,8 @@
      (if x (implies y z rest ...) #t))))
 
 (define-system prelude ()
-  (define-primitive-function natural? (x))
-  (define-primitive-function equal? (x y))
-  (define-primitive-function atom? (x))
-  (define-primitive-function cons (x y))
-  (define-primitive-function car (x))
-
-  (define-primitive-function cdr (x))
-  (define-primitive-function size (x))
-  (define-primitive-function not (x))
-  (define-primitive-function < (x y))
-
+  (define-function atom? (x)
+    (not (pair? x)))
   (define-syntax-rules list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
@@ -71,7 +62,7 @@
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
      (if x (implies y z . rest) #t)))
-  
+
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
   (define-axiom equal-swap (x y)
@@ -93,24 +84,142 @@
         (equal? (if x y z) y)
         (equal? (if x y z) z)))
   (define-axiom if-true (x y)
-    (equal? (if '#f x y) y))
+    (equal? (if '#t x y) x))
   (define-axiom if-false (x y)
     (equal? (if '#f x y) y))
   (define-axiom if-same (x y)
     (equal? (if x y y) y))
-  (define-axiom natural/size (x)
+  (define-axiom natural?/size (x)
     (equal? (natural? (size x))
             '#t))
-  (define-axiom size/car (x)
+  (define-axiom </size/car (x)
     (if (atom? x)
         '#t
         (equal? (< (size (car x)) (size x))
                 '#t)))
-  (define-axiom size/cdr (x)
+  (define-axiom </size/cdr (x)
     (if (atom? x)
         '#t
         (equal? (< (size (cdr x)) (size x))
                 '#t)))
   (define-axiom if-not (x y z)
     (equal? (if (not x) y z)
-            (if x z y))))
+            (if x z y)))
+  (define-axiom sub1/add1 (x)
+    (implies (natural? x)
+             (equal? (sub1 (add1 x)) x)))
+  (define-axiom natural?/0 (x)
+    (equal? (natural? '0) '#t))
+  (define-axiom natural?/add1 (x)
+    (implies (natural? x)
+             (equal? (natural? (add1 x)) '#t)))
+  (define-axiom sub1/add1 (x)
+    (implies (natural? x)
+             (equal? (sub1 (add1 x)) x)))
+  (define-axiom </sub1 (x)
+    (implies (natural? x)
+             (equal? (< (sub1 x) x) '#t)))
+  (define-axiom common-add1 (x y)
+    (implies (natural? x)
+             (natural? y)
+             (equal? (equal? (add1 x) (add1 y))
+                     (equal? x y))))
+  (define-axiom false-if (x)
+    (if x '#t (equal? x '#f)))
+  (define-axiom equal?/01 (x)
+    (equal? (equal? '0 '1) #f))
+  (define-axiom natural?/sub1 (x)
+    (if (natural? x)
+        (if (equal? '0 x)
+            '#t
+            (equal? (natural? (sub1 x)) '#t))
+        '#t))
+  (define-axiom add1/sub1 (x)
+    (if (natural? x)
+        (if (equal? '0 x)
+            '#t
+            (equal? (add1 (sub1 x)) x))
+        '#t))
+  
+  (define-primitive-function + (x y)
+    (if (natural? x)
+        (if (equal? '0 x)
+            y
+            (add1 (+ (sub1 x) y)))
+        'undefined))
+
+  (define-proof +
+    (total/natural? x)
+    (((2) if-nest)
+     ((2 3) </sub1)
+     ((2) if-same)
+     (() if-same)))
+
+  (define-theorem thm-1+1=2 ()
+    (equal? (+ 1 1) 2))
+  
+  (define-function natural-induction (n)
+    (if (natural? n)
+        (if (equal? '0 n)
+            '0
+            (add1 (natural-induction (sub1 n))))
+        'undefined))
+
+  (define-proof natural-induction
+    (total/natural? n)
+    (((2) if-nest)
+     ((2 3) </sub1)
+     ((2) if-same)
+     (() if-same)))
+
+  (define-theorem equal?/add1 (n)
+    (if (natural? n)
+        (equal? (equal? n (add1 n)) #f)
+        #t))
+  
+  (define-proof equal?/add1
+    (induction (natural-induction n))
+    (((2 2 2 1 1) equal-if)
+     ((2 2 2 1 2 1) equal-if)
+     ((2 2 2 1) equal?/01)
+     ((2 2 2) equal-same)
+     ((2 2) if-same)
+     ((2 3 1 1) natural?/sub1)
+     ((2 3 1) if-true)
+     ((2 3 2 2 1 1) add1/sub1)
+     ((2 3 2 2 1 2 1) add1/sub1)
+     ((2 3 2 2) if-same (set x (natural? (add1 (sub1 n)))))
+     ((2 3 2 2) if-same (set x (natural? (sub1 n))))
+     ((2 3 2 2 2 2 1) common-add1
+      ;; ルール探索のアルゴリズムにバグがある
+      (set x (sub1 n))
+      (set y (add1 (sub1 n))))
+     ((2 3 2 2 2 2 1) equal-if)
+     ((2 3 2 2 2 2) equal-same)
+     ((2 3 2 2 2 1) natural?/add1)
+     ((2 3 2 2 2) if-true)
+     ((2 3 2 2 1) natural?/sub1)
+     ((2 3 2 2) if-true)
+     ((2 3 2) if-same)
+     ((2 3) if-same)
+     ((2) if-same)
+     ((3) if-nest)
+     (() if-same)))
+  
+  (define-proof thm-1+1=2
+    ()
+    ((() if-same (set x (natural? '0)))
+     ((2 1) +)
+     ((2 1 2 2 1) equal-if)
+     ((2 1 2 3 1 1) sub1/add1)
+     ((2 1 2 3 1) +)
+     ((2 1 2 3 1 2 1) equal-same)
+     ((2 1 2 3 1 2) if-true)
+     ((2 1 2 3 1 1) natural?/0)
+     ((2 1 2 3 1) if-true)
+     ((2 1 2) if-same)
+     ((2 1 1) natural?/add1)
+     ((2 1) if-true)
+     ((2) equal-same)
+     ((1) natural?/0)
+     (() if-true))))
-- 
cgit v1.2.3