From 4d4bfc8ab6133c41d8b7ff3c281de0f4ef61e5b3 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 8 Nov 2020 07:17:12 +0900
Subject: wip6

---
 rabbit-prover.scm | 259 +++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 177 insertions(+), 82 deletions(-)

(limited to 'rabbit-prover.scm')

diff --git a/rabbit-prover.scm b/rabbit-prover.scm
index 2a12698..fde842d 100644
--- a/rabbit-prover.scm
+++ b/rabbit-prover.scm
@@ -47,6 +47,14 @@
         ((variable? expr) #t)
         (else #f)))
 
+(define (all-vars x)
+  (cond ((expr-quoted? x) '())
+        ((pair? x)
+         (append (all-vars (car x))
+                 (all-vars (cdr x))))
+        ((variable? x) (list x))
+        (else '())))
+
 ;; (expr-quoted? x) -> boolean?
 (define (expr-quoted? expr)
   (and (pair? expr)
@@ -184,7 +192,8 @@
          (and (pair? (car x))
               (or (proposition? (car x))
                   (primitive-function? (car x))
-                  (macro? (car x)))
+                  (macro? (car x))
+                  (function? (car x)))
               (book? (cdr x))))
         (else #f)))
 
@@ -228,16 +237,15 @@
 
 (define (function? x)
   (and (list? x)
-       (= 5 (length x))
-       (variable? (list-ref x 0))
+       (= 4 (length x))
+       (variable? (function-name x))
        (eq? 'function (list-ref x 1))
-       (vars? (list-ref x 2))
-       (expression? (list-ref x 3))
-       ((option proof?) (list-ref x 4))))
+       (vars? (function-vars x))
+       (expression? (function-expression x))))
 
-;; (function variable? vars? expression? (option proof?)) -> function?
-(define/guard (function (name variable?) (vars vars?) (expr expression?) (proof (option proof)))
-  (list name 'function vars expr proof))
+;; (function variable? vars? expression?) -> function?
+(define/guard (function (name variable?) (vars vars?) (expr expression?))
+  (list name 'function vars expr))
 
 (define (function-name f)
   (list-ref f 0))
@@ -248,9 +256,6 @@
 (define (function-expression f)
   (list-ref f 3))
 
-(define (function-proof f)
-  (list-ref f 4))
-
 (define (mrule? x)
   (and (list? x)
        (= 4 (length x))
@@ -341,7 +346,7 @@
 (define (apply-macro m expr)
   (cond ((and (pair? expr)
               (eq? (macro-name m) (car expr)))
-         (let loop ((rs (macro-rules m)))
+         (let loop ((rs (macro-mrules m)))
            (cond ((null? rs) expr)
                  ((apply-mrule (car rs) expr) => identity)
                  (else (loop (cdr rs))))))
@@ -386,35 +391,30 @@
        (vars? (list-ref x 2))
        (expression? (list-ref x 3))))
 
-;; (theorem name vars? expression? proof?) -> theorem?
-(define/guard (theorem (name variable?) (vars vars?) (expr expression?) (p (option proof?)))
-  (list name 'theorem vars expr p))
+;; (theorem name vars? expression?) -> theorem?
+(define/guard (theorem (name variable?) (vars vars?) (expr expression?))
+  (list name 'theorem vars expr))
 
 ;; (theorem? x) -> boolean?
 ;; theorem? is proposition
 (define (theorem? x)
   (and (list? x)
-       (= 5 (length x))
+       (= 4 (length x))
        (variable? (list-ref x 0))
        (eq? 'theorem (list-ref x 1))
        (vars? (list-ref x 2))
-       (expression? (list-ref x 3))
-       ((option proof?) (list-ref x 4))))
+       (expression? (list-ref x 3))))
 
 (define (theorem-name x)
   (list-ref x 0))
 
-(define (theorem-proof x)
-  (list-ref x 4))
-
-(define (proof seq)
-  (list 'proof seq))
-
 ;; (proposition? x) -> boolean?
 (define (proposition? x)
   (or (axiom? x)
-      (theorem? x)
-      (function? x)))
+      (theorem? x)))
+
+(define (proposition-name x)
+  (list-ref x 0))
 
 (define (proposition-vars x)
   (list-ref x 2))
@@ -427,13 +427,6 @@
                      '()
                      (proposition-expression x)))
 
-;; (proof? x) -> boolean?
-(define (proof? x)
-  (and (list? x)
-       (= 2 (length x))
-       (eq? 'proof (list-ref x 0))
-       (sequence? (list-ref x 1))))
-
 ;; (rewriter path? command?) -> rewriter?
 (define (rewriter p c)
   (list p c))
@@ -499,6 +492,18 @@
          (else
           (fail "invalid path" path))))))
 
+(define (function->rules x)
+  (list (rule (function-vars x)
+              '()
+              (cons (function-name x)
+                    (function-vars x))
+              (function-expression x))
+        (rule (function-vars x)
+              '()
+              (function-expression x)
+              (cons (function-name x)
+                    (function-vars x)))))
+
 ;; (rewrite book? rewriter? expression? procedure?) -> expr
 (define (rewrite1 b expr fail r)
   (let ((cmd (rewriter-command r)))
@@ -515,12 +520,17 @@
          => (lambda (x)
               (cond
                ((proposition? x)
-                (let ((rls (proposition-rules x)))
-                  (cond
-                   ((any (cut apply-rule preconds <> extracted-expr)
-                         rls) => identity)
-                   (else
-                    (fail (format #f "no match-rule (~a)" cmd))))))
+                (cond
+                 ((any (cut apply-rule preconds <> extracted-expr)
+                       (proposition-rules x)) => identity)
+                 (else
+                  (fail (format #f "no match-rule (~a)" cmd)))))
+               ((function? x)
+                (cond
+                 ((any (cut apply-rule '() <> extracted-expr)
+                       (function->rules x)) => identity)
+                 (else
+                  (fail (format #f "no match-rule (~a)" cmd)))))
                ((primitive-function? x)
                 (cond
                  ((match-primitive-function x extracted-expr)
@@ -595,7 +605,11 @@
           (list (rule vars
                       preconds
                       (expr-equal-lhs expr)
-                      (expr-equal-rhs expr)))
+                      (expr-equal-rhs expr))
+                (rule vars
+                      preconds
+                      (expr-equal-rhs expr)
+                      (expr-equal-lhs expr)))
           '())))
 
 (define (proposition->rules def)
@@ -603,50 +617,131 @@
                      '()
                      (proposition-expression def)))
 
+(define current-book (make-parameter '()))
+
+(define (add-book b x)
+  (cond ((assoc (proposition-name x) b)
+         => (lambda (prop)
+              (if (equal? x prop)
+                  b
+                  (error "add-book: error"))))
+        (else (cons x b))))
+
 (define-syntax define-axiom
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (axiom 'name '(var ...) 'expr))))
-
-(define prelude
-  (list (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 pair/cons (x y)
-          (equal? (pair? (cons x y)) '#t))
-        (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 y)
-          (equal? (if (pair? x)
-                      (equal? (cons (car x) (cdr y)) x)
-                      '#t)
-                  y))
-        (define-axiom cons/car+cdr (x y)
-          (equal? (if (pair? x)
-                      (equal? (cons (car x) (cdr y)) x)
-                      '#t)
-                  y))
-        (define-axiom if-same (x y)
-          (equal? (if x y y) y))
-        (define-axiom size/car (x)
-          (if (pair? x)
-              (equal? (< (size x) (size (car x)))
-                      '#t)
-              '#t))
-        (define-axiom size/cdr (x)
-          (if (pair? x)
-              (equal? (< (size x) (size (cdr x)))
-                      '#t)
-              '#t))
-        (macro 'list
-          (list (mrule '() '(list) ''())
-                (mrule '(x y) '(list x . y)
-                       '(cons x (list . y)))))))
+     (current-book
+      (add-book (current-book)
+                (axiom 'name '(var ...) 'expr))))))
+
+(define-syntax define-theorem
+  (syntax-rules ()
+    ((_ name (var ...) expr)
+     (current-book
+      (add-book (current-book)
+                (theorem 'name '(var ...) 'expr))))))
+
+(define-syntax define-function
+  (syntax-rules ()
+    ((_ name (var ...) expr)
+     (let ((f (function 'name '(var ...) 'expr)))
+       (current-book (add-book (current-book) f))
+       f))))
+
+(define-syntax define-macro
+  (syntax-rules ()
+    ((_ name () ((lhs1 . lhs2) rhs) ...)
+     (current-book
+      (add-book (current-book)
+                (macro 'name
+                  (list (mrule (all-vars 'lhs2) '(lhs1 . lhs2) 'rhs)
+                        ...)))))))
+
+(define-syntax define-book
+  (syntax-rules ()
+    ((_ name (books ...) expr ...)
+     (define* (name #:optional (parent '()))
+       (parameterize ([current-book ((compose books ... identity) parent)])
+         expr
+         ...
+         (unless (book? (current-book))
+           (error "define-book: error"))
+         (current-book))))))
+
+(define-book prelude ()
+  (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 pair/cons (x y)
+    (equal? (pair? (cons x y)) '#t))
+  (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 y)
+    (equal? (if (pair? x)
+                (equal? (cons (car x) (cdr y)) x)
+                '#t)
+            y))
+    (define-axiom cons/car+cdr (x y)
+    (equal? (if (pair? x)
+                (equal? (cons (car x) (cdr y)) x)
+                '#t)
+            y))
+  (define-axiom if-same (x y)
+    (equal? (if x y y) y))
+  (define-axiom size/car (x)
+    (if (pair? x)
+        (equal? (< (size x) (size (car x)))
+                '#t)
+        '#t))
+  (define-axiom size/cdr (x)
+    (if (pair? x)
+        (equal? (< (size x) (size (cdr x)))
+                '#t)
+        '#t))
+  (define-macro list ()
+    ((list) '())
+    ((list x . y) (cons x (list . y))))
+  (define-macro + ()
+    ((+) '0)
+    ((+ x) x)
+    ((+ x . xs) (b+ x (+ . xs))))
+  (define-macro - ()
+    ((- x) (u- x))
+    ((- x . xs) (+ x . (u- (+ . xs)))))
+  (define-macro and ()
+    ((and) '#t)
+    ((and x) x)
+    ((and x . xs) (if x (and . xs) #f)))
+  (define-macro or ()
+    ((or) '#f)
+    ((or x) x)
+    ((or x . xs) (if x x (or . xs))))
+  (define-macro atom? ()
+    ((atom? x) (not (pair? x))))
+  
+  (define-axiom if-not (x y z)
+    (equal? (if (not x)
+                y
+                z)
+            (if x
+                z
+                y))))
+
+(define-book app (prelude)
+  (define-function app (x y)
+    (if (atom? x)
+        y
+        (cons x (app x y))))
+
+  (define-theorem associate-app (x y z)
+    (equal? (app (app x y) z)
+            (app x (app y z)))))
+
 
 (define (size x)
   (if (pair? x)
-- 
cgit v1.2.3