From 48886fc939749cd834a72a4c386b851150859cfa Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Wed, 16 Dec 2020 23:43:25 +0900
Subject: wip57

---
 vikalpa.scm         | 155 +++-------------------------------------------------
 vikalpa/prelude.scm |   1 +
 2 files changed, 9 insertions(+), 147 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index 771c623..ab87b7d 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -1269,14 +1269,14 @@
                              (get-variables f)
                              seed)
         (update-definition (make <total-function>
-                                  #:name (get-name f)
-                                  #:variables (get-variables f)
-                                  #:conditions (get-conditions f)
-                                  #:expression (get-expression f)
-                                  #:code (get-code f)
-                                  #:claim (make-totality-claim* sys seed f)
-                                  #:proof seq)
-                                sys))
+                             #:name (get-name f)
+                             #:variables (get-variables f)
+                             #:conditions (get-conditions f)
+                             #:expression (get-expression f)
+                             #:code (get-code f)
+                             #:claim (make-totality-claim* sys seed f)
+                             #:proof seq)
+                           sys))
       (raise-exception
        (make-exception
         (make-exception-with-origin 'define-proof)
@@ -1510,142 +1510,3 @@
 
 (define/guard (system-load (sys system?))
   (primitive-eval (system-code sys)))
-
-(define-system prelude ()
-  (define-core-function natural? (x) (lambda (x)
-                                       (and (integer? x)
-                                            (< 0 x))))
-  (define-core-function < (x y) (natural? x) (natural? y) <)
-  (define-core-function pair? (x) pair?)
-  (define-core-function cons (x y) cons)
-  (define-core-function car (x) (pair? x)
-    (lambda (x) (if (pair? x) (car x) '())))
-  (define-core-function cdr (x) (pair? x)
-    (lambda (x) (if (pair? x) (cdr x) '())))
-  (define-core-function + (x y)
-    (lambda (x y)
-      (if (number? x)
-          (if (number? y)
-              (+ x y)
-              x)
-          (if (number? y)
-              y
-              0))))
-  (set-measure-predicate natural?)
-  (set-measure-less-than <)
-  (define-trivial-total-function list-induction (x)
-    (if (not (pair? x))
-        x
-        (cons (car x)
-              (list-induction (cdr x)))))
-  (define-trivial-total-function size (x)
-    (if (not (pair? x))
-        0
-        (+ 1
-           (+ (size (car x))
-              (size (cdr x))))))
-
-  (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-syntax-rules implies ()
-    ((implies x y) (if x y #t))
-    ((implies x y z . rest)
-     (if x (implies y z . rest) #t)))
-  
-  (define-axiom if-nest (x y z)
-    (if x
-        (equal? (if x y z) y)
-        (equal? (if x y z) z)))
-
-  (define-axiom if-true (x 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 if-not (x y z)
-    (equal? (if (not x) y z)
-            (if x z y)))
-
-  (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)
-    (implies (equal? x y) (equal? x y)))
-  
-  (define-axiom pair/cons (x y)
-    (equal? (pair? (cons x y)) '#t))
-
-  (define-axiom cons/car+cdr (x)
-    (implies (pair? x)
-             (equal? (cons (car x) (cdr x)) x)))
-
-  (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 natural/size (x)
-    (equal? (natural? (size x)) #t))
-
-  (define-axiom size/car (x)
-    (equal? (< (size (car x)) (size x)) #t))
-
-  (define-axiom size/cdr (x)
-    (equal? (< (size (cdr x)) (size x)) #t))
-
-  (define-axiom equal-car (x1 y1 x2 y2)
-    (implies (equal? (cons x1 y1) (cons x2 y2))
-             (equal? x1 x2)))
-
-  (define-theorem caar-cons2 (x y z)
-    (equal? (car (car (cons (cons x y) z))) x))
-
-  (define-function double (x)
-    (+ x x))
-  
-  (define-function app (x y)
-    (if (not (pair? x))
-        y
-        (cons (car x)
-              (app (cdr x) y))))
-  
-  (define-theorem assoc-app (x y z)
-    (equal? (app x (app y z))
-            (app (app x y) z)))
-
-  (define-proof caar-cons2
-    (((1 1)  car/cons)
-     ((1) car/cons)
-     (() equal-same)))
-
-  (define-proof app
-    (size x)
-    (((2 3) size/cdr)
-     ((2) if-same)
-     ((1) natural/size)
-     (() if-true)))
-
-  (define-proof assoc-app
-    (list-induction x)
-    ()))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 17d1db8..bd8b409 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -156,3 +156,4 @@
     (list-induction x)
     ()))
 
+
-- 
cgit v1.2.3