From 7955016f0c6908c9d2e0578d75d4b2104f97e0a2 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 29 Nov 2020 10:26:40 +0900
Subject: wip41

---
 vikalpa.scm         | 146 +++++++++++++++++++++++++++++++++++++++++-----------
 vikalpa/prelude.scm |  65 +++++++++++++++++------
 2 files changed, 166 insertions(+), 45 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index 27d09c8..98a7d97 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -418,25 +418,27 @@
 
 (define (primitive-function? x)
   (and (list? x)
-       (= 5 (length x))
+       (= 6 (length x))
        (variable? (function-name x))
        (eq? 'primitive-function (list-ref x 1))
        (vars? (function-vars x))
        ((option expression?) (function-expression x))
-       ((option code?) (function-code x))))
+       ((option code?) (function-code x))
+       ((list-of expression?) (function-preconds x))))
 
 ;; (primitive-function variable? vars?) -> primitive-function?
-(define (primitive-function name vs expr code)
-  (list name 'primitive-function vs expr code))
+(define (primitive-function name vs expr preconds code)
+  (list name 'primitive-function vs expr preconds code))
 
 (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))
-       ((option code?) (function-code x))))
+       ((option code?) (function-code x))
+       ((list-of expression?) (function-preconds x))))
 
 (define (code? x)
   (and (list? x)
@@ -454,8 +456,9 @@
 (define/guard (function (name variable?)
                         (vars vars?)
                         (expr expression?)
+                        (preconds (list-of expression?))
                         (code (option code?)))
-  (list name 'function vars expr code))
+  (list name 'function vars expr preconds code))
 
 (define (function-name f)
   (list-ref f 0))
@@ -466,9 +469,12 @@
 (define (function-expression f)
   (list-ref f 3))
 
-(define (function-code f)
+(define (function-preconds f)
   (list-ref f 4))
 
+(define (function-code f)
+  (list-ref f 5))
+
 (define (definition-name d)
   (list-ref d 0))
 
@@ -630,7 +636,7 @@
        ((list-of (lambda (x)
                    (and (list? x)
                         (= 2 (length x))
-                        (symbol? (car x))))) 
+                        (symbol? (car x)))))
         (list-ref x 1))))
 
 (define (expand-let x)
@@ -860,11 +866,11 @@
 
 (define (function->rules x)
   (list (rule (function-vars x)
-              '()
+              (function-preconds x)
               (function-app-form x)
               (definition-expression x))
         (rule (function-vars x)
-              '()
+              (function-preconds x)
               (definition-expression x)
               (function-app-form x))))
 
@@ -1050,31 +1056,33 @@
 
 (define-syntax define-function
   (syntax-rules ()
-    ((_ name (var ...) expr)
+    ((_ name (var ...) precond ... expr)
      (let ((f (function 'name '(var ...)
                         (convert-to-expression 'expr)
+                        '(precond ...)
                         (code 'expr))))
        (add-definition f)
        (validate-definition f)
        f))))
 
-(define-syntax define-core-function
-  (syntax-rules ()
-    ((_ name (var ...))
-     (let ((f (primitive-function 'name '(var ...) #f #f)))
-       (add-definition f)
-       f))))
-
 (define-syntax define-primitive-function
   (syntax-rules ()
-    ((_ name (var ...) expr)
+    ((_ name (var ...) precond ... expr)
      (let ((f (primitive-function 'name '(var ...)
                                   (convert-to-expression 'expr)
+                                  '(precond ...)
                                   (code 'expr))))
        (add-definition f)
        (validate-definition f)
        f))))
 
+(define-syntax define-core-function
+  (syntax-rules ()
+    ((_ name (var ...) precond ...)
+     (let ((f (primitive-function 'name '(var ...) #f '(precond ...) #f)))
+       (add-definition f)
+       f))))
+
 (define-syntax define-syntax-rules
   (syntax-rules ()
     ((_ name (l ...) ((lhs1 . lhs2) rhs) ...)
@@ -1182,6 +1190,14 @@
             ''undefined))
        (else
         (fail 'pred extracted-expr))))
+    ((<)
+     (match extracted-expr
+       (('< `(quote ,x) `(quote ,y))
+        (if (and (integer? x) (integer? y))
+            (expr-quote (< x y))
+            ''undefined))
+       (else
+        (fail 'pred extracted-expr))))
     (else (fail 'rewrite/core 'invalid))))
 
 (define* (core-system #:optional (parent (make-system '() '() '())))
@@ -1190,12 +1206,20 @@
     (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 car (x)
+      #;(pair? x)
+      )
+    (define-core-function cdr (x)
+      #;(pair? x)
+      )
     (define-core-function integer? (x))
-    (define-core-function < (x y))
-    (define-core-function succ (x))
-    (define-core-function pred (x))
+    (define-core-function < (x y)
+      ;;(integer? x) (integer? y)
+      )
+    (define-core-function succ (x) ;;(integer? x)
+      )
+    (define-core-function pred (x) ;;(integer? x)
+      )
     (current-system)))
 
 (define-syntax define-system
@@ -1300,7 +1324,52 @@
               (else (error "(vikalpa) make-totality-claim: error"
                            (function-name f)
                            m-expr))))
-           ''#t)))
+           ''#f)))
+
+(define (make-totality-claim/preconds 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-totality-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)
+      (apply and/if (map build/find-if (app-form-args expr))))
+     (else ''#t)))
+  (define (build expr)
+    (cond
+     ((if-form? expr)
+      (apply and/if
+             (append (find-preconds (if-form-test expr))
+                     (list (if/if (if-form-test expr)
+                                  (build (if-form-then expr))
+                                  (build (if-form-else expr)))))))
+     ((app-form? expr)
+      (apply and/if
+             (append (find-preconds expr)
+                     (list (build/find-if expr)))))
+     (else ''#t)))
+  (if/if (build expr)
+         '#t
+         '#f))
 
 (define/guard (make-induction-claim (f function*?)
                                     (vars (list-of variable?))
@@ -1439,7 +1508,9 @@
                                      `(claim-of ,(proof-name pf))
                                      (theorem-vars t)
                                      claim)
-                (rewrite sys-without-self claim (proof-sequence pf)))))
+                (rewrite sys-without-self
+                         claim
+                         (proof-sequence pf)))))
         (else (error "(vikalpa) define-proof: induction function is not found."
                      (proof-name pf)
                      (cons f vars)))))
@@ -1452,6 +1523,16 @@
 
 (define (prove/function sys f pf)
   (match (proof-seed pf)
+    (()
+     (unless (trivial-total? f)
+       (error "prove/function"))
+     (rewrite sys
+              (fold implies/if
+                    (make-totality-claim/preconds
+                     (function-expression f)
+                     sys)
+                    (function-preconds f))
+              (proof-sequence pf)))
     ((id m-expr)
      (cond
       ((find-totality-claim id sys)
@@ -1462,7 +1543,13 @@
                                    (function-vars f)
                                    claim)
               (rewrite sys
-                       claim
+                       (fold implies/if
+                             (and/if
+                              (make-totality-claim/preconds
+                               (function-expression f)
+                               sys)
+                              claim)
+                             (function-preconds f))
                        (proof-sequence pf)))))
       (else
        (error "(vikalpa) define-proof: totality-claim is not found:"
@@ -1497,7 +1584,8 @@
        ((null? defs) fails)
        ((or (theorem? (car defs))
             (function? (car defs)))
-       (cond
+        (cond
+         #;
          ((and (function? (car defs))
                (trivial-total? (car defs)))
           (next))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 5b70a72..c7ab89e 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -51,16 +51,6 @@
     ((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 (zero? x)
-             (< 0 x))))
-
-  (define-totality-claim natural? natural? <)
-
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
 
@@ -109,10 +99,19 @@
     (implies (equal? (cons x1 y1) (cons x2 y2))
              (equal? y1 y2)))
 
+  (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)))
 
+
   (define-axiom succ/pred (x)
     (implies (natural? x)
              (not (zero? x))
@@ -121,16 +120,51 @@
   (define-axiom less/pred (x)
     (implies (natural? x)
              (equal? (< (pred x) x) #t)))
+  
+  (define-totality-claim natural? natural? <)
 
+  
   (define-function + (x y)
-    (if (natural? x)
-        (if (zero? x)
-            y
-            (succ (+ (pred x) y)))
-        'undeifned<+>))
+    (natural? x)
+    (natural? y)
+    (if (zero? x)
+        y
+        (succ (+ (pred x) y))))
+
+  (define-proof zero?
+    ()
+    ())
+
+  (define-proof natural?
+    ()
+    ())
+  (define-proof +
+    (natural? x)
+    ())
+  
+  #;
+  (define-proof natural?
+    ()
+    (((1 2 3 1) (eval))
+     ((1 2 3) if-true)
+     (() if-same (set x (zero? x)))
+     ((2 1 2) if-nest)
+     ((2 1) if-same)
+     ((2) if-true)
+     ((3 1 2) if-nest)
+     ((3) if-same (set x (integer? x)))
+     ((3 2 1) if-nest)
+     ((3 2) if-nest)
+     ((3 3 1) if-nest)
+     ((3 3) if-true)
+     ((3) if-same)
+     (() if-same)))
 
+  #;
   (define-proof +
     (natural? x)
+    ()
+    #;
     (((2) if-nest)
      ((2 3) less/pred)
      ((2) if-same)
@@ -142,7 +176,6 @@
   ;;    ((1 2 1) if-nest)
   ;;    ((1 3 1) if-nest)
   ;;    ((1 3) if-true)
-  ;;    (() equal-same)))
 
   ;; (define-proof less-than/pred
   ;;   (natural-induction x)
-- 
cgit v1.2.3