From 107ff1ce2460045e30961dd5679c9e20ec1d57a9 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Mon, 30 Nov 2020 14:13:52 +0900
Subject: wip42

---
 vikalpa.scm         | 84 +++++++++++++++++++++++++++++++++++++++--------------
 vikalpa/prelude.scm | 14 ---------
 2 files changed, 62 insertions(+), 36 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index 98a7d97..a2b4dd2 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -1040,7 +1040,8 @@
   (syntax-rules ()
     ((_ name (var ...) expr)
      (let ((t (axiom 'name '(var ...)
-                     (convert-to-expression 'expr))))
+                     (make-theorem-claim (convert-to-expression 'expr)
+                                         (current-system)))))
        (add-definition t)
        (validate-definition t)
        t))))
@@ -1049,7 +1050,8 @@
   (syntax-rules ()
     ((_ name (var ...) expr)
      (let ((t (theorem 'name '(var ...)
-                       (convert-to-expression 'expr))))
+                       (make-theorem-claim (convert-to-expression 'expr)
+                                           (current-system)))))
        (add-definition t)
        (validate-definition t)
        t))))
@@ -1170,14 +1172,15 @@
         (fail 'cdr extracted-expr))))
     ((integer?)
      (match extracted-expr
-       (('integer? `(quote ,x))
-        (expr-quote (integer? x)))
+       (('natural? `(quote ,x))
+        (expr-quote (natural? x)))
        (else
-        (fail 'integer? extracted-expr))))
+        (fail 'natural? extracted-expr))))
     ((succ)
      (match extracted-expr
        (('succ `(quote ,x))
-        (if (integer? x)
+        (if (and (natural? x)
+                 (< 0 x))
             (expr-quote (succ x))
             ''undefined))
        (else
@@ -1185,7 +1188,7 @@
     ((pred)
      (match extracted-expr
        (('pred `(quote ,x))
-        (if (integer? x)
+        (if (natural? x)
             (expr-quote (pred x))
             ''undefined))
        (else
@@ -1193,7 +1196,7 @@
     ((<)
      (match extracted-expr
        (('< `(quote ,x) `(quote ,y))
-        (if (and (integer? x) (integer? y))
+        (if (and (natural? x) (natural? y))
             (expr-quote (< x y))
             ''undefined))
        (else
@@ -1206,20 +1209,12 @@
     (define-core-function equal? (x y))
     (define-core-function pair? (x y))
     (define-core-function cons (x y))
-    (define-core-function car (x)
-      #;(pair? x)
-      )
-    (define-core-function cdr (x)
-      #;(pair? x)
-      )
-    (define-core-function integer? (x))
-    (define-core-function < (x y)
-      ;;(integer? x) (integer? y)
-      )
-    (define-core-function succ (x) ;;(integer? x)
-      )
-    (define-core-function pred (x) ;;(integer? x)
-      )
+    (define-core-function car (x) (pair? x))
+    (define-core-function cdr (x) (pair? x))
+    (define-core-function natural? (x))
+    (define-core-function < (x y) (natural? x) (natural? y))
+    (define-core-function succ (x) (natural? x))
+    (define-core-function pred (x) (natural? x))
     (current-system)))
 
 (define-syntax define-system
@@ -1371,6 +1366,51 @@
          '#t
          '#f))
 
+(define (make-theorem-claim expr sys)
+  (define (find-preconds expr)
+    (cond
+     ((app-form? expr)
+      (let ((rest (append-map find-preconds (cdr expr))))
+        (append (cond ((lookup (car expr) sys) =>
+                       (lambda (f)
+                         (let ((preconds (function-preconds f)))
+                           (map (lambda (precond)
+                                  (substitute (map cons
+                                                   (function-vars f)
+                                                   (cdr expr))
+                                              precond))
+                                preconds))))
+                      (else (error "make-theorem-claim/preconds: error")))
+                rest)))
+     ((if-form? expr)
+      (find-preconds (if-form-test expr)))
+     (else '())))
+  (define (build/find-if expr)
+    (cond
+     ((if-form? expr)
+      (if/if (build/find-if (if-form-test expr))
+             (build (if-form-then expr))
+             (build (if-form-else expr))))
+     ((app-form? expr)
+      (fold implies/if
+            expr
+            (map build/find-if (app-form-args expr))))
+     (else expr)))
+  (define (build expr)
+    (cond
+     ((if-form? expr)
+      (fold implies/if
+            (if/if (if-form-test expr)
+                   (build (if-form-then expr))
+                   (build (if-form-else expr)))
+            (find-preconds (if-form-test expr))))
+     ((app-form? expr)
+      (fold implies/if
+            (build/find-if expr)
+            (find-preconds expr)))
+     (else expr)))
+  (build expr))
+
 (define/guard (make-induction-claim (f function*?)
                                     (vars (list-of variable?))
                                     (t theorem?))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index c7ab89e..c61e459 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -102,11 +102,6 @@
   (define-function zero? (x)
     (equal? 0 x))
 
-  (define-function natural? (x)
-    (and (integer? x)
-         (or (zero? x)
-             (< 0 x))))
-
   (define-axiom pred/succ (x)
     (implies (natural? x)
              (equal? (pred (succ x)) x)))
@@ -122,8 +117,6 @@
              (equal? (< (pred x) x) #t)))
   
   (define-totality-claim natural? natural? <)
-
-  
   (define-function + (x y)
     (natural? x)
     (natural? y)
@@ -131,13 +124,6 @@
         y
         (succ (+ (pred x) y))))
 
-  (define-proof zero?
-    ()
-    ())
-
-  (define-proof natural?
-    ()
-    ())
   (define-proof +
     (natural? x)
     ())
-- 
cgit v1.2.3