From 52d0f284f3c8c26eb86c4dcd8f3f819c657e7d78 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 29 Nov 2020 02:45:39 +0900
Subject: wip36

---
 vikalpa.scm         | 362 +++++++++++++++++++++++++++++++++++-----------------
 vikalpa/prelude.scm | 355 ++++++++++++++++++++++++++++-----------------------
 2 files changed, 440 insertions(+), 277 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index 671082a..dc5b6de 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -33,16 +33,20 @@
             define-theorem
             define-primitive-function
             define-function
+            define-scheme-function
             define-proof
             define-totality-claim
             define-syntax-rules
+            system-eval
+            natural?
             succ
             pred)
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
   #:use-module (ice-9 control)
   #:use-module ((srfi srfi-1)
-                #:select (every any member lset-union fold append-map))
+                #:select (every any member lset-union fold append-map
+                                find))
   #:use-module (srfi srfi-8)
   #:use-module (srfi srfi-11)
   #:use-module (srfi srfi-26)
@@ -53,17 +57,40 @@
       (apply format #t f args)
       #t))
 
-(define-syntax-rule (define/guard (name (var pred?) ...) b b* ...)
+(define-syntax-rule (define/guard (name (var p?) ...) b b* ...)
   (define (name var ...)
-    (unless (pred? var)
+    (unless (p? var)
       (error (format #f
                      "~a:~%  expected:  ~a~%  given: "
                      'name
-                     'pred?)
+                     'p?)
              var))
     ...
     b b* ...))
 
+(define-syntax define-type
+  (syntax-rules ()
+    ((_ name
+        constractor
+        (m p?)
+        (n t? getter-name getter) ...)
+     (begin
+       (define len (+ 1 (length (list n ...))))
+       (define (constractor getter-name ...)
+         (let ((data (make-list len)))
+           (list-set! data m 'name)
+           (list-set! data n getter-name)
+           ...
+           data))
+       (define (p? x)
+         (and (list? x)
+              (= len (length x))
+              (eq? 'name (list-ref x m))
+              (t? (list-ref x n)) ...))
+       (define (getter x)
+         (list-ref x n))
+       ...))))
+
 ;; (natural? x) -> boolean?
 (define (natural? x)
   (and (exact-integer? x)
@@ -141,7 +168,7 @@
 
 (define (expression-vars expr)
   (cond
-   ((app-form? expr)
+   ((pair? expr)
     (apply lset-union eq?
            (map expression-vars (app-form-args expr))))
    ((variable? expr) (list expr))
@@ -323,7 +350,6 @@
     => (cut substitute <> (rule-rhs rl)))
    (else #f)))
 
-
 (define (system? x)
   (and (list? x)
        (= 4 (length x))
@@ -385,14 +411,16 @@
 
 (define (primitive-function? x)
   (and (list? x)
-       (= 3 (length x))
+       (= 5 (length x))
        (variable? (primitive-function-name x))
        (eq? 'primitive-function (list-ref x 1))
-       (vars? (primitive-function-vars x))))
+       (vars? (primitive-function-vars x))
+       ((option expression?) (primitive-function-expression x))
+       ((option code?) (primitive-function-code x))))
 
 ;; (primitive-function variable? vars?) -> primitive-function?
-(define (primitive-function name vs)
-  (list name 'primitive-function vs))
+(define (primitive-function name vs expr code)
+  (list name 'primitive-function vs expr code))
 
 (define (primitive-function-name pf)
   (list-ref pf 0))
@@ -400,23 +428,39 @@
 (define (primitive-function-vars pf)
   (list-ref pf 2))
 
+(define (primitive-function-expression pf)
+  (list-ref pf 3))
+
+(define (primitive-function-code pf)
+  (list-ref pf 4))
+
 (define (function? x)
   (and (list? x)
-       (= 6 (length x))
+       (= 5 (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))
-       (boolean? (function-primitive? x))))
+       ((option code?) (function-code x))))
+
+(define (code? x)
+  (and (list? x)
+       (= 2 (length x))
+       (eq? 'code (list-ref x 0))
+       ((const #t) (code-expr x))))
+
+(define (code x)
+  (list 'code x))
+
+(define (code-expr x)
+  (cadr x))
 
 ;; (function variable? vars? expression?) -> function?
 (define/guard (function (name variable?)
                         (vars vars?)
                         (expr expression?)
-                        (code (const #t))
-                        (primitive boolean?))
-  (list name 'function vars expr code primitive))
+                        (code (option code?)))
+  (list name 'function vars expr code))
 
 (define (function-name f)
   (list-ref f 0))
@@ -430,9 +474,6 @@
 (define (function-code f)
   (list-ref f 4))
 
-(define (function-primitive? f)
-  (list-ref f 5))
-
 (define (definition-name d)
   (list-ref d 0))
 
@@ -644,26 +685,10 @@
              ,(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)
-  (expand-quoted
-   (quote-all
-    (expand* (filter macro? (system-definitions (current-system)))
-             (expand-let x)))))
+  (quote-all
+   (expand* (filter macro? (system-definitions (current-system)))
+            (expand-let x))))
 
 ;; (axiom variable? vars? expression?) -> axiom?
 ;; axiom? is theorem*
@@ -719,6 +744,39 @@
                      '()
                      (theorem*-expression x)))
 
+(define (error? x)
+  (and (pair? x)
+       (eq? 'error (car x))))
+
+(define (rewrite/eval expr sys)
+  (let eval ((expr expr))
+    (cond
+     ((error? expr) expr)
+     ((expr-quoted? expr) expr)
+     ((app-form? expr)
+      (let ((args (map eval (app-form-args expr)))
+            (name (app-form-name expr)))
+        (or (find error? args)
+            (eval (rewrite1 sys
+                            `(,name ,@args)
+                            (lambda args
+                              (cons* 'error rewrite name args))
+                            (rewriter '() `(,name)))))))
+     ((if-form? expr)
+      (let ((test (eval (if-form-test expr))))
+        (if (error? test)
+            test
+            (if (expr-unquote test)
+                (eval (if-form-then expr))
+                (eval (if-form-else expr))))))
+     (else
+      `(error eval invalid-expression ,expr)))))
+
+(define/guard (system-eval (expr (const #t)) (sys system?))
+  (rewrite/eval (parameterize ((current-system sys))
+                  (convert-to-expression expr))
+                sys))
+
 ;; (rewriter path? command?) -> rewriter?
 (define (rewriter p c)
   (cons p c))
@@ -809,10 +867,10 @@
   (list (rule (function-vars x)
               '()
               (function-app-form x)
-              (function-expression x))
+              (definition-expression x))
         (rule (function-vars x)
               '()
-              (function-expression x)
+              (definition-expression x)
               (function-app-form x))))
 
 (define (apply-function f args)
@@ -854,24 +912,10 @@
         (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 'equal? extracted-expr))))
-        ((eq? 'pair? cmd/name)
-         (match extracted-expr
-           (('pair? `(quote ,x))
-            (expr-quote (pair? x)))
-           (else
-            (fail 'pair? extracted-expr))))
-        ((eq? 'not cmd/name)
-         (match extracted-expr
-           (('not `(quote ,x))
-            (expr-quote (not x)))
-           (else
-            (fail 'not extracted-expr))))
+        ((core-function-name? cmd/name)
+         (rewrite/core cmd/name extracted-expr fail))
+        ((equal? '(eval) cmd/name)
+         (rewrite/eval extracted-expr sys))
         ((eq? 'error cmd/name) (fail extracted-expr))
         ((and (symbol? cmd/name)
               (lookup cmd/name sys))
@@ -879,7 +923,9 @@
               (cond
                ((theorem*? x)
                 (rewrite/theorem cmd sys x preconds extracted-expr fail))
-               ((function? x)
+               ((or (function? x)
+                    (and (primitive-function? x)
+                         (primitive-function-expression x)))
                 (cond
                  ((any (cut apply-rule '() <> extracted-expr '())
                        (function->rules x)) => identity)
@@ -1012,23 +1058,24 @@
     ((_ name (var ...) expr)
      (let ((f (function 'name '(var ...)
                         (convert-to-expression 'expr)
-                        'expr
-                        #f)))
+                        (code 'expr))))
        (add-definition f)
        (validate-definition f)
        f))))
 
-(define-syntax define-primitive-function
+(define-syntax define-core-function
   (syntax-rules ()
     ((_ name (var ...))
-     (let ((f (primitive-function 'name '(var ...))))
+     (let ((f (primitive-function 'name '(var ...) #f #f)))
        (add-definition f)
-       f))
+       f))))
+
+(define-syntax define-primitive-function
+  (syntax-rules ()
     ((_ name (var ...) expr)
-     (let ((f (function 'name '(var ...)
-                        (convert-to-expression 'expr)
-                        'expr
-                        '#t)))
+     (let ((f (primitive-function 'name '(var ...)
+                                  (convert-to-expression 'expr)
+                                  (code 'expr))))
        (add-definition f)
        (validate-definition f)
        f))))
@@ -1070,16 +1117,90 @@
 (define-syntax-rule (define-totality-claim name nat? <)
   (add-totality-claim (totality-claim 'name 'nat? '<)))
 
+(define core-function-names
+  '(not equal? pair? cons car cdr integer? < succ pred))
+
+(define (core-function-name? x)
+  (member x core-function-names))
+
+(define (rewrite/core name extracted-expr fail)
+  (case name
+    ((not)
+     (match extracted-expr
+       (('not `(quote ,x))
+        (expr-quote (not x)))
+       (else
+        (fail 'not extracted-expr))))
+    ((equal?)
+     (match extracted-expr
+       (('equal? `(quote ,x) `(quote ,y))
+        (expr-quote (equal? x y)))
+       (else
+        (fail 'equal? extracted-expr))))
+    ((pair?)
+     (match extracted-expr
+       (('pair? `(quote ,x))
+        (expr-quote (pair? x)))
+       (else
+        (fail 'pair? extracted-expr))))
+    ((cons)
+     (match extracted-expr
+       (('cons `(quote ,x) `(quote ,y))
+        (expr-quote (cons x y)))
+       (else
+        (fail 'cons extracted-expr))))
+    ((car)
+     (match extracted-expr
+       (('car `(quote ,x))
+        (if (pair? x)
+            (expr-quote (car x))
+            ''undefined))
+       (else
+        (fail 'car extracted-expr))))
+    ((cdr)
+     (match extracted-expr
+       (('cdr `(quote ,x))
+        (if (pair? x)
+            (expr-quote (cdr x))
+            ''undefined))
+       (else
+        (fail 'cdr extracted-expr))))
+    ((integer?)
+     (match extracted-expr
+       (('integer? `(quote ,x))
+        (expr-quote (integer? x)))
+       (else
+        (fail 'integer? extracted-expr))))
+    ((succ)
+     (match extracted-expr
+       (('succ `(quote ,x))
+        (if (integer? x)
+            (expr-quote (succ x))
+            ''undefined))
+       (else
+        (fail 'succ extracted-expr))))
+    ((pred)
+     (match extracted-expr
+       (('pred `(quote ,x))
+        (if (integer? x)
+            (expr-quote (pred x))
+            ''undefined))
+       (else
+        (fail 'pred extracted-expr))))
+    (else (fail 'rewrite/core 'invalid))))
+
 (define* (core-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 y))
-    (define-primitive-function cons (x y))
-    (define-primitive-function car (x))
-    (define-primitive-function cdr (x))
-    (define-primitive-function succ (x))
-    (define-primitive-function pred (x))
+    (define-core-function not (x))
+    (define-core-function equal? (x y))
+    (define-core-function pair? (x y))
+    (define-core-function cons (x y))
+    (define-core-function car (x))
+    (define-core-function cdr (x))
+    (define-core-function integer? (x))
+    (define-core-function < (x y))
+    (define-core-function succ (x))
+    (define-core-function pred (x))
     (current-system)))
 
 (define-syntax define-system
@@ -1267,32 +1388,34 @@
   (or (function? x)
       (primitive-function? x)))
 
-(define (validate-definition d)
-  (let* ((expr (definition-expression d))
-         (vars (definition-vars d))
-         (name (definition-name d))
-         (expr-fnames (expression-functions expr))
+(define (validate-expression sys name vars expr)
+  (let* ((expr-fnames (expression-functions expr))
          (expr-vars (expression-vars expr)))
     (when (reserved? name)
       (error (format #f "(vikalpa) ~a: reserved name" name)))
     (for-each (lambda (x)
-                (unless (cond
-                         ((lookup x (current-system)) => function*?)
-                         (else #f))
+                (when (member x expr-fnames)
+                  (error (format #f "(vikalpa) ~a: invalid variable name" name)
+                         x)))
+              vars)
+    (for-each (lambda (x)
+                (unless (cond ((lookup x sys) => function*?)
+                              (else #f))
                   (error (format #f "(vikalpa) ~a: undefined function" name)
                          x)))
               expr-fnames)
     (for-each (lambda (x)
                 (unless (member x vars)
                   (error (format #f "(vikalpa) ~a: undefined variable" name)
-                         x))
-                (when (member x (if (function? d)
-                                    (cons name expr-fnames)
-                                    expr-fnames))
-                  (error (format #f "(vikalpa) ~a: invalid variable name" name)
                          x)))
               expr-vars)))
 
+(define (validate-definition d)
+  (let* ((vars (definition-vars d))
+         (name (definition-name d))
+         (expr (definition-expression d)))
+    (validate-expression (current-system) name vars expr)))
+
 (define (trivial-total? f)
   (not (member (function-name f)
                (expression-functions (function-expression f)))))
@@ -1306,25 +1429,31 @@
    (else (error "prove" def pf))))
 
 (define (prove/theorem sys t pf)
-  (match (proof-seed pf)
-    ((f . vars)
-     (cond
-      ((lookup f sys)
-       => (lambda (seed)
-            (rewrite sys
-                     (make-induction-claim seed
-                                           vars
-                                           t)
-                     (proof-sequence pf))))
-      (else (error "(vikalpa) define-proof: induction function is not found."
-                   (proof-name pf)
-                   (cons f vars)))))
-    (()
-     (rewrite sys
-              (theorem*-expression t)
-              (proof-sequence pf)))
-    (else
-     (error "prove/theorem: fail"))))
+  (let ((sys-without-self
+         (make-system (filter (lambda (d) (not (equal? t d)))
+                              (system-definitions sys))
+                      (system-proofs sys)
+                      (system-totality-claim-list sys))))
+    (match (proof-seed pf)
+      ((f . vars)
+       (cond
+        ((lookup f sys-without-self)
+         => (lambda (seed)
+              (let ((claim (make-induction-claim seed vars t)))
+                (validate-expression sys
+                                     `(claim-of ,(proof-name pf))
+                                     (theorem*-vars t)
+                                     claim)
+                (rewrite sys-without-self claim (proof-sequence pf)))))
+        (else (error "(vikalpa) define-proof: induction function is not found."
+                     (proof-name pf)
+                     (cons f vars)))))
+      (()
+       (rewrite sys-without-self
+                (theorem*-expression t)
+                (proof-sequence pf)))
+      (else
+       (error "prove/theorem: fail")))))
 
 (define (prove/function sys f pf)
   (match (proof-seed pf)
@@ -1332,9 +1461,14 @@
      (cond
       ((find-totality-claim id sys)
        => (lambda (tc)
-            (rewrite sys
-                     (make-totality-claim tc m-expr f)
-                     (proof-sequence pf))))
+            (let ((claim (make-totality-claim tc m-expr f)))
+              (validate-expression sys
+                                   `(claim-of ,(function-name f))
+                                   (function-vars f)
+                                   claim)
+              (rewrite sys
+                       claim
+                       (proof-sequence pf)))))
       (else
        (error "(vikalpa) define-proof: totality-claim is not found:"
               (proof-name pf)
@@ -1347,10 +1481,10 @@
   `(begin
      ,@(map (lambda (f)
               `(define (,(function-name f) ,@(function-vars f))
-                 ,(function-code f)))
+                 ,(code-expr (function-code f))))
             (reverse (filter (lambda (x)
-                               (and (function? x)
-                                    (not (function-primitive? x))))
+                               (and (function*? x)
+                                    (function-code x)))
                              (system-definitions sys))))))
 
 (define/guard (check (sys system?))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index d03df7e..1ee56af 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -27,10 +27,6 @@
      (if x (implies y z rest ...) #t))))
 
 (define-system prelude ()
-  (define-primitive-function < (x y))
-  (define-primitive-function natural? (x))
-  (define-totality-claim natural? natural? <)
-
   (define-syntax-rules list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
@@ -54,7 +50,18 @@
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
      (if x (implies y z . rest) #t)))
+
+  (define-function zero? (x)
+    (equal? 0 x))
+
+  (define-function natural? (x)
+    (and (integer? x)
+         (or (equal? x 0)
+             (< x 0))))
+
+  (define-totality-claim natural? natural? <)
   
+
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
 
@@ -82,222 +89,244 @@
     (equal? (if (not x) y z)
             (if x z y)))
 
-  (define-axiom pair-cons (x y)
+  (define-axiom pair/cons (x y)
     (equal? (pair? (cons x y)) '#t))
 
-  (define-axiom car-cdr-elim (x)
-    (if (pair? x)
-        (equal? (cons (car x) (cdr x)) x)
-        '#t))
+  (define-axiom cons/car+cdr (x)
+    (implies (pair? x)
+             (equal? (cons (car x) (cdr x)) x)))
 
-  (define-axiom car-cons (x y)
+  (define-axiom car/cons (x y)
     (equal? (car (cons x y)) x))
 
-  (define-axiom cdr-cons (x y)
+  (define-axiom cdr/cons (x y)
     (equal? (cdr (cons x y)) y))
-  
-  (define-axiom car-cdr-elim (x)
-    (implies (pair? x)
-             (equal? (cons (car x) (cdr x)) x)))
 
-  (define-axiom cons-equal-car (x1 y1 x2 y2)
+  (define-axiom equal-car (x1 y1 x2 y2)
     (implies (equal? (cons x1 y1) (cons x2 y2))
              (equal? x1 x2)))
 
-  (define-axiom cons-equal-cdr (x1 y1 x2 y2)
+  (define-axiom equal-cdr (x1 y1 x2 y2)
     (implies (equal? (cons x1 y1) (cons x2 y2))
              (equal? y1 y2)))
-  
-  #;
-  (define-axiom natural?/0 ()
-    (equal? (natural? '0) '#t))
 
-  #;
-  (define-theorem equal/zero-less-than (x)
+  (define-axiom pred/succ (x)
     (implies (natural? x)
-             (equal? (not (< '0 x))
-                     (equal? x '0))))
-
-  #;
-  (define-proof equal/zero-less-than
-    (natural-induction x)
-    (((2 2) if-nest)
-     ((3) if-nest)
-     ((2 2 1) if-same (set x (natural? '0)))
-     ((2 2 1 2 1) axiom-less-than)
-     ((2 2 1 1) natural/zero)
-     ((2 2 1) if-true)
-     ((2 2 1 1 1) equal-same)
-     ((2 2 1 1) if-true)
-     ((2 2 1 1 1 2) equal-if)
-     ((2 2 1 1 1) equal-same)
-     ((2 2 1 1) if-true)
-     ((2 2 1) not/false)
-     ((2 2 2 1) equal-if)
-     ((2 2 2) equal-same)
-     ((2 2) equal-same)
-     ((2 3 2 2) if-same (set x (natural? '0)))
-     ((2 3 2 2 2 1 1) axiom-less-than)
-     ((2 3 2 2 2 1 1 1) equal-same)
-     ((2 3 2 2 2 1 1) if-true)
-     ((2 3 2 2 2 1 1) if-nest)
-     ((2 3 2 2 2 1) not/true)
-     ((2 3 2 2 2 2) equal-swap)
-     ((2 3 2 2 2 2) false-if)
-     ((2 3 2 2 2) equal-same)
-     ((2 3 2 2 1) natural/zero)
-     ((2 3 2 2) if-true)
-     ((2 3 2) if-same)
-     ((2 3) if-same)
-     ((2) if-same)
-     (() if-same)))
+             (equal? (pred (succ x)) x)))
   
-  ;; (define-axiom natural/sub1 (x)
-  ;;   (implies (natural? x)
-  ;;            (if (equal? '0 x)
-  ;;                '#t
-  ;;                (equal? (natural? (sub1 x)) #t))))
+  (define-axiom succ/pred (x)
+    (implies (natural? x)
+             (not (zero? x))
+             (equal? (succ (pred x)) x)))
+
+  (define-theorem less-than/pred-1 (x)
+    (implies (not (zero? x))
+             (natural? x)
+             (natural? (pred x))
+             (not (zero? (pred x)))
+             (equal? (< (pred (pred x)) (pred x)) '#t)
+             (equal?
+              (if (zero? (pred x))
+                  '#t
+                  (< (pred (pred x)) (pred x)))
+              '#t)))
   
-;; (define-proof natural-induction
-;;     (total/natural? n)
-;;     (((2) if-nest)
-;;      ((2 3) </sub1)
-;;      ((2) if-same)
-;;      (() if-same)))
+  (define-theorem if-implies (x y z w)
+    (equal? (if (if x y #t)
+                z
+                w)
+            (if x
+                (if y
+                    z
+                    w)
+                z)))
+
+  (define-theorem less-than/pred-2 (x)
+    (implies (not (natural? x))
+             (equal? (zero? x) #f)))
+
+  (define-primitive-function natural-induction (x)
+    (if (natural? x)
+        (if (zero? x)
+            0
+            (succ (natural-induction (pred x))))
+        #f))
 
-;; (define-theorem natural/add1 (x)
-;;     (implies (natural? x)
-;;              (equal? (natural? (add1 x)) #t)))
+  (define-theorem less-than/pred (x)
+    (implies (natural? x)
+             (not (zero? x))
+             (equal? (< (pred x) x) #t)))
+
+  ;; (define-proof if-implies
+  ;;   ()
+  ;;   (((1) if-same (set x x))
+  ;;    ((1 2 1) if-nest)
+  ;;    ((1 3 1) if-nest)
+  ;;    ((1 3) if-true)
+  ;;    (() equal-same)))
+
+  ;; (define-proof less-than/pred
+  ;;   (natural-induction x)
+  ;;   (((2 2) if-nest)
+  ;;    ((2 2) if-not)
+  ;;    ((2 2) if-nest)
+  ;;    ((2 3 2) if-nest)
+  ;;    ((2 3 2) if-nest)
+  ;;    ((2 3) if-implies)
+  ;;    ((2 3 2) if-implies)
+     
+  ;;    (() error)
+  ;;    (() error)))
+
+  ;; (define-proof less-than/pred-1
+  ;;   ()
+  ;;   (((2 2) if-same (set x (natural? (pred x))))
+  ;;    ((2 2 2) if-same (set x (not (zero? (pred x)))))
+  ;;    ((2 2 2) if-same (set x (not (zero? (pred x)))))
+  ;;    ;; ((2 2 3 1 1) zero?)
+  ;;    ;; ((2 2 3 1 1) if-nest)
+  ;;    ;; ((2 2 3 1) if-false)
+  ;;    ;; ((2 2 3 1) if-false)
+  ;;    ))
+  
+  (define-function + (x y)
+    (if (equal? 0 x)
+        y
+        (succ (+ (pred x) y))))
+
+  ;; (define-theorem natural/add1 (x)
+  ;;     (implies (natural? x)
+  ;;              (equal? (natural? (add1 x)) #t)))
 
   #;
   (define-axiom natural/sub1 (x)
-    (if (natural? x)
-        (if (< '0 x)
-            (equal? (natural? (sub1 x)) '#t)
-            '#t)
-        '#t))
+  (if (natural? x)
+  (if (< '0 x)
+  (equal? (natural? (sub1 x)) '#t)
+  '#t)
+  '#t))
 
   #;
   (define-theorem less-than/sub1 (x)
-    (implies (natural? x)
-             (< '0 x)
-             (equal? (< (sub1 x) x) '#t)))
+  (implies (natural? x)
+  (< '0 x)
+  (equal? (< (sub1 x) x) '#t)))
 
   #;
   (define-axiom add1/sub1 (x)
-    (if (natural? x)
-        (if (equal? '0 x)
-            '#t
-            (equal? (add1 (sub1 x)) x))
-        '#t))
+  (if (natural? x)
+  (if (equal? '0 x)
+  '#t
+  (equal? (add1 (sub1 x)) x))
+  '#t))
 
   #;
   (define-built-in-function + (x y)
-    (if (natural? x)
-        (if (equal? '0 x)
-            y
-            (add1 (+ (sub1 x) y)))
-        'undefined))
+  (if (natural? x)
+  (if (equal? '0 x)
+  y
+  (add1 (+ (sub1 x) y)))
+  'undefined))
 
-#;
+  #;
   (define-axiom natural/size (x)
-    (equal? (natural? (size x))
-            '#t))
+  (equal? (natural? (size x))
+  '#t))
 
   #;
   (define-axiom size/car (x)
-    (if (pair? x)
-        (equal? (< (size (car x)) (size x))
-                '#t)
-        '#t))
+  (if (pair? x)
+  (equal? (< (size (car x)) (size x))
+  '#t)
+  '#t))
 
   #;
   (define-axiom size/cdr (x)
-    (if (pair? x)
-        (equal? (< (size (cdr x)) (size x))
-                '#t)
-        '#t))
+  (if (pair? x)
+  (equal? (< (size (cdr x)) (size x))
+  '#t)
+  '#t))
   
   #;
   (define-proof +
-    (total/natural? x)
-    (((2) if-nest)
-     ((2 3) </sub1)
-     ((2) if-same)
-     (() if-same)))
+  (total/natural? x)
+  (((2) if-nest)
+  ((2 3) </sub1)
+  ((2) if-same)
+  (() if-same)))
 
   #;
   (define-theorem thm-1+1=2 ()
-    (equal? (+ 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))
+  (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)))
+  (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))
+  (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)))
+  (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-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