From 6bd6d3734621ce747ebf4b39496f87f0b0fdea01 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 16 Jan 2021 23:08:21 +0900
Subject: wip81

---
 examples/prelude.scm | 34 +++++++++-------------------------
 1 file changed, 9 insertions(+), 25 deletions(-)

(limited to 'examples')

diff --git a/examples/prelude.scm b/examples/prelude.scm
index f171b6e..39aa67a 100644
--- a/examples/prelude.scm
+++ b/examples/prelude.scm
@@ -17,15 +17,9 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (size prelude)
+  #:export (prelude)
   #:use-module (vikalpa))
 
-(define (size x)
-  (if (pair? x)
-      (+ (size (car x))
-         (size (cdr x)))
-      1))
-
 (define-syntax-rule (define-axiom/is p1 p2)
   (define-axiom (is p1 p2) (x) (is (p1 x) (p2 x))))
 
@@ -177,7 +171,6 @@
 
   (define-theorem/is exact-zero? natural?)
   (define-theorem/is exact-positive-integer? natural?)
-
   (set-measure-predicate natural?)
   (set-measure-less-than <)
 
@@ -261,7 +254,13 @@
   (define-core-function cons (x y) cons)
   (define-core-function/guard car (x) (pair? x) car)
   (define-core-function/guard cdr (x) (pair? x) cdr)
-  (define-core-function size (x) size))
+  (define-function size (x)
+    (if (pair? x)
+        (+ (size (car x))
+           (size (cdr x)))
+        1))
+  (admit size))
+
 
 (define-system prelude (prelude/pair)
   (define-proof inexact?
@@ -369,21 +368,6 @@
      (eval (2))
      (rewrite () if-same)))
 
-  #;
-  (define-proof (natural? and not exact-zero? implies exact-positive-integer?)
-    ((rewrite (1) natural?)
-     (rewrite () if-same (set x (exact-zero? x)))
-     (rewrite (2 1) if-nest)
-     (rewrite (2) if-true)
-     (rewrite (2) if-not)
-     (rewrite (2) if-nest)
-     (rewrite (3 1) if-nest)
-     (rewrite (3 2) if-not)
-     (rewrite (3 2) if-nest)
-     (rewrite (3 2) (predicate exact-positive-integer?))
-     (rewrite (3) if-same)
-     (rewrite () if-same)))
-
   (define-proof (+ (-> natural? natural? natural?))
     ((induction (2 2) (natural-induction-+ x y))
      (rewrite (2 2 2 1) (+ natural? natural?))
@@ -408,7 +392,7 @@
     ((rewrite (1) exact-zero?)
      (rewrite (2 1 1) equal-if)
      (eval (2))
-     (rewrite ()  if-same)))
+     (rewrite () if-same)))
 
   (define-proof (is exact-positive-integer? natural?)
     ((rewrite (2 1) natural?)
-- 
cgit v1.2.3