From 60a1d48a4afdb139caa9936895b3f1833d6a7926 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Wed, 25 Nov 2020 09:29:38 +0900 Subject: wip35 --- vikalpa/prelude.scm | 106 ++++++++++++++++++++---------------------- vikalpa/the-little-prover.scm | 22 ++++----- 2 files changed, 60 insertions(+), 68 deletions(-) (limited to 'vikalpa') diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 35f91dd..d03df7e 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -17,7 +17,7 @@ ;;; along with Vikalpa. If not, see . (define-module (vikalpa prelude) - #:export (implies prelude) + #:export (natural? size implies prelude) #:use-module (vikalpa)) (define-syntax implies @@ -27,7 +27,6 @@ (if x (implies y z rest ...) #t)))) (define-system prelude () - (define-primitive-function pair? (x y)) (define-primitive-function < (x y)) (define-primitive-function natural? (x)) (define-totality-claim natural? natural? <) @@ -40,14 +39,17 @@ ((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) @@ -55,77 +57,68 @@ (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 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 (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) (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 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-axiom pair-cons (x y) + (equal? (pair? (cons x y)) '#t)) - (define-proof natural-induction - (natural? n) - ()) + (define-axiom car-cdr-elim (x) + (if (pair? x) + (equal? (cons (car x) (cdr x)) x) + '#t)) - (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 car-cons (x y) + (equal? (car (cons x y)) x)) - (define-axiom natural/zero () - (equal? (natural? '0) '#t)) + (define-axiom cdr-cons (x y) + (equal? (cdr (cons x y)) y)) + + (define-axiom car-cdr-elim (x) + (implies (pair? x) + (equal? (cons (car x) (cdr x)) x))) - (define-axiom not/true () - (equal? (not #t) #f)) + (define-axiom cons-equal-car (x1 y1 x2 y2) + (implies (equal? (cons x1 y1) (cons x2 y2)) + (equal? x1 x2))) - (define-axiom not/false () - (equal? (not #f) #t)) + (define-axiom cons-equal-cdr (x1 y1 x2 y2) + (implies (equal? (cons x1 y1) (cons x2 y2)) + (equal? y1 y2))) + + #; + (define-axiom natural?/0 () + (equal? (natural? '0) '#t)) + #; (define-theorem equal/zero-less-than (x) (implies (natural? x) (equal? (not (< '0 x)) (equal? x '0)))) + #; (define-proof equal/zero-less-than (natural-induction x) (((2 2) if-nest) @@ -159,11 +152,11 @@ ((2) if-same) (() if-same))) - (define-axiom natural/sub1 (x) - (implies (natural? x) - (if (equal? '0 x) - '#t - (equal? (natural? (sub1 x)) #t)))) + ;; (define-axiom natural/sub1 (x) + ;; (implies (natural? x) + ;; (if (equal? '0 x) + ;; '#t + ;; (equal? (natural? (sub1 x)) #t)))) ;; (define-proof natural-induction ;; (total/natural? n) @@ -172,9 +165,9 @@ ;; ((2) if-same) ;; (() if-same))) -(define-theorem natural/add1 (x) - (implies (natural? x) - (equal? (natural? (add1 x)) #t))) +;; (define-theorem natural/add1 (x) +;; (implies (natural? x) +;; (equal? (natural? (add1 x)) #t))) #; (define-axiom natural/sub1 (x) @@ -199,14 +192,14 @@ '#t)) #; - (define-primitive-function + (x y) + (define-built-in-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)) @@ -306,4 +299,5 @@ ((2 1) if-true) ((2) equal-same) ((1) natural?/0) - (() if-true)))) + (() if-true))) + ) diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm index b892f7f..338843b 100644 --- a/vikalpa/the-little-prover.scm +++ b/vikalpa/the-little-prover.scm @@ -17,24 +17,22 @@ ;;; along with Vikalpa. If not, see . (define-module (vikalpa the-little-prover) - #:export (atom? the-little-prover) + #:export (the-little-prover) #:use-module (vikalpa)) -(define (atom? x) - (not (pair? x))) - (define (size x) - (if (atom? x) - 0 + (if (pair? x) (+ (size (car x)) - (size (cdr x))))) + (size (cdr x))) + 0)) (define-system the-little-prover () - (define-primitive-function atom? (x)) - (define-primitive-function size (x)) - (define-primitive-function + (x y)) - (define-primitive-function natural? (x)) - (define-primitive-function < (x y)) + (define-function atom? (x) + (not (pair? x))) + (define-builtin-function size (x)) + (define-builtin-function + (x y)) + (define-builtin-function natural? (x)) + (define-builtin-function < (x y)) (define-totality-claim natural? natural? <) ;; Axioms of Equal -- cgit v1.2.3