summaryrefslogtreecommitdiff
path: root/vikalpa/prelude.scm
diff options
context:
space:
mode:
Diffstat (limited to 'vikalpa/prelude.scm')
-rw-r--r--vikalpa/prelude.scm208
1 files changed, 148 insertions, 60 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 8816131..c55ea48 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -17,23 +17,9 @@
;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>.
(define-module (vikalpa prelude)
- #:export (atom? size implies natural? prelude)
+ #:export (implies prelude)
#:use-module (vikalpa))
-(define (atom? x)
- (not (pair? x)))
-
-(define (natural? x)
- (and (integer? x)
- (not (negative? x))))
-
-(define (size x)
- (if (pair? x)
- (+ 1
- (size (car x))
- (size (cdr x)))
- 0))
-
(define-syntax implies
(syntax-rules ()
((_ x y) (if x y #t))
@@ -41,8 +27,16 @@
(if x (implies y z rest ...) #t))))
(define-system prelude ()
- (define-function atom? (x)
- (not (pair? x)))
+ (define-primitive-function pair? (x y))
+ (define-primitive-function cons (x y))
+ (define-primitive-function car (x))
+ (define-primitive-function cdr (x))
+ (define-primitive-function sub1 (x))
+ (define-primitive-function add1 (x))
+ (define-primitive-function < (x y))
+ (define-primitive-function natural? (x))
+ (define-totality-claim natural? natural? <)
+
(define-syntax-rules list ()
((list) '())
((list x . y) (cons x (list . y))))
@@ -62,23 +56,23 @@
((implies x y) (if x y #t))
((implies x y z . rest)
(if x (implies y z . rest) #t)))
-
+
(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 atom/cons (x y)
- (equal? (atom? (cons x y)) '#f))
+ (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)
- (if (atom? x)
- '#t
- (equal? (cons (car x) (cdr x)) x)))
+ (if (pair? x)
+ (equal? (cons (car x) (cdr x)) x)
+ '#t))
(define-axiom if-nest (x y z)
(if x
(equal? (if x y z) y)
@@ -89,65 +83,153 @@
(equal? (if '#f x y) y))
(define-axiom if-same (x y)
(equal? (if x y y) y))
- (define-axiom natural?/size (x)
- (equal? (natural? (size x))
- '#t))
- (define-axiom </size/car (x)
- (if (atom? x)
- '#t
- (equal? (< (size (car x)) (size x))
- '#t)))
- (define-axiom </size/cdr (x)
- (if (atom? x)
- '#t
- (equal? (< (size (cdr x)) (size x))
- '#t)))
(define-axiom if-not (x y z)
(equal? (if (not x) y z)
(if x z y)))
+
+ (define-axiom axiom-less-than (x y)
+ (implies (natural? x)
+ (natural? y)
+ (equal? (< x y)
+ (if (equal? '0 x)
+ (if (equal? '0 y)
+ #f
+ #t)
+ (if (equal? '0 y)
+ #f
+ (< (sub1 x) (sub1 y)))))))
+ (define-function natural-induction (n)
+ (if (natural? n)
+ (if (equal? '0 n)
+ '0
+ (add1 (natural-induction (sub1 n))))
+ 'undefined))
+
+ (define-proof natural-induction
+ (natural? n)
+ ())
+
+ (define-axiom false-if (x)
+ (if x #t (equal? #f x)))
+
(define-axiom sub1/add1 (x)
(implies (natural? x)
(equal? (sub1 (add1 x)) x)))
- (define-axiom natural?/0 (x)
+
+ (define-axiom natural/zero ()
(equal? (natural? '0) '#t))
- (define-axiom natural?/add1 (x)
- (implies (natural? x)
- (equal? (natural? (add1 x)) '#t)))
- (define-axiom sub1/add1 (x)
+
+ (define-axiom not/true ()
+ (equal? (not #t) #f))
+
+ (define-axiom not/false ()
+ (equal? (not #f) #t))
+
+ (define-theorem equal/zero-less-than (x)
(implies (natural? x)
- (equal? (sub1 (add1 x)) x)))
- (define-axiom </sub1 (x)
+ (equal? (not (< '0 x))
+ (equal? x '0))))
+
+ (define-proof equal/zero-less-than
+ (natural-induction x)
+ (((2 2) if-nest)
+ ((3) if-nest)
+ ((2 2 1) if-same (set x (natural? '0)))
+ ((2 2 1 2 1) axiom-less-than)
+ ((2 2 1 1) natural/zero)
+ ((2 2 1) if-true)
+ ((2 2 1 1 1) equal-same)
+ ((2 2 1 1) if-true)
+ ((2 2 1 1 1 2) equal-if)
+ ((2 2 1 1 1) equal-same)
+ ((2 2 1 1) if-true)
+ ((2 2 1) not/false)
+ ((2 2 2 1) equal-if)
+ ((2 2 2) equal-same)
+ ((2 2) equal-same)
+ ((2 3 2 2) if-same (set x (natural? '0)))
+ ((2 3 2 2 2 1 1) axiom-less-than)
+ ((2 3 2 2 2 1 1 1) equal-same)
+ ((2 3 2 2 2 1 1) if-true)
+ ((2 3 2 2 2 1 1) if-nest)
+ ((2 3 2 2 2 1) not/true)
+ ((2 3 2 2 2 2) equal-swap)
+ ((2 3 2 2 2 2) false-if)
+ ((2 3 2 2 2) equal-same)
+ ((2 3 2 2 1) natural/zero)
+ ((2 3 2 2) if-true)
+ ((2 3 2) if-same)
+ ((2 3) if-same)
+ ((2) if-same)
+ (() if-same)))
+
+ (define-axiom natural/sub1 (x)
(implies (natural? x)
- (equal? (< (sub1 x) x) '#t)))
- (define-theorem common-add1 (x y)
+ (if (equal? '0 x)
+ '#t
+ (equal? (natural? (sub1 x)) #t))))
+
+;; (define-proof natural-induction
+;; (total/natural? n)
+;; (((2) if-nest)
+;; ((2 3) </sub1)
+;; ((2) if-same)
+;; (() if-same)))
+
+(define-theorem natural/add1 (x)
(implies (natural? x)
- (natural? y)
- (equal? (equal? (add1 x) (add1 y))
- (equal? x y))))
- (define-axiom false-if (x)
- (if x '#t (equal? x '#f)))
- (define-axiom equal?/01 (x)
- (equal? (equal? '0 '1) #f))
- (define-axiom natural?/sub1 (x)
+ (equal? (natural? (add1 x)) #t)))
+
+ #;
+ (define-axiom natural/sub1 (x)
(if (natural? x)
- (if (equal? '0 x)
- '#t
- (equal? (natural? (sub1 x)) '#t))
+ (if (< '0 x)
+ (equal? (natural? (sub1 x)) '#t)
+ '#t)
'#t))
+
+ #;
+ (define-theorem less-than/sub1 (x)
+ (implies (natural? x)
+ (< '0 x)
+ (equal? (< (sub1 x) x) '#t)))
+
+ #;
(define-axiom add1/sub1 (x)
(if (natural? x)
(if (equal? '0 x)
'#t
(equal? (add1 (sub1 x)) x))
'#t))
-
+
+ #;
(define-primitive-function + (x y)
(if (natural? x)
(if (equal? '0 x)
y
(add1 (+ (sub1 x) y)))
'undefined))
+
+ #;
+ (define-axiom natural/size (x)
+ (equal? (natural? (size x))
+ '#t))
+ #;
+ (define-axiom size/car (x)
+ (if (pair? x)
+ (equal? (< (size (car x)) (size x))
+ '#t)
+ '#t))
+
+ #;
+ (define-axiom size/cdr (x)
+ (if (pair? x)
+ (equal? (< (size (cdr x)) (size x))
+ '#t)
+ '#t))
+
+ #;
(define-proof +
(total/natural? x)
(((2) if-nest)
@@ -155,9 +237,11 @@
((2) if-same)
(() if-same)))
+ #;
(define-theorem thm-1+1=2 ()
(equal? (+ 1 1) 2))
-
+
+ #;
(define-function natural-induction (n)
(if (natural? n)
(if (equal? '0 n)
@@ -165,6 +249,7 @@
(add1 (natural-induction (sub1 n))))
'undefined))
+ #;
(define-proof natural-induction
(total/natural? n)
(((2) if-nest)
@@ -172,11 +257,13 @@
((2) if-same)
(() if-same)))
+ #;
(define-theorem equal?/add1 (n)
(if (natural? n)
(equal? (equal? n (add1 n)) #f)
#t))
-
+
+ #;
(define-proof equal?/add1
(induction (natural-induction n))
(((2 2 2 1 1) equal-if)
@@ -205,7 +292,8 @@
((2) if-same)
((3) if-nest)
(() if-same)))
-
+
+ #;
(define-proof thm-1+1=2
()
((() if-same (set x (natural? '0)))
generated by cgit v1.2.3 (git 2.44.0) at 2024-05-18 18:59:22 +0000