wip80

2 files changed, 0 insertions, 398 deletions

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
deleted file mode 100644
index 824b5c5..0000000
--- a/vikalpa/prelude.scm
+++ /dev/null
@@ -1,235 +0,0 @@
-;;; Vikalpa --- Proof Assistant
-;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo>
-;;;
-;;; This file is part of Vikalpa.
-;;;
-;;; Vikalpa is free software; you can redistribute it and/or modify it
-;;; under the terms of the GNU General Public License as published by
-;;; the Free Software Foundation; either version 3 of the License, or
-;;; (at your option) any later version.
-;;;
-;;; Vikalpa is distributed in the hope that it will be useful, but
-;;; WITHOUT ANY WARRANTY; without even the implied warranty of
-;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-;;; General Public License for more details.
-;;;
-;;; You should have received a copy of the GNU General Public License
-;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
-
-(define-module (vikalpa prelude)
-  #:export (prelude)
-  #:use-module (vikalpa))
-
-(define (exact-positive-integer? x)
-  (and (exact-integer? x)
-       (positive? x)))
-
-(define (exact-negative-integer? x)
-  (and (exact-integer? x)
-       (negative? x)))
-
-(define-syntax-rule (define-axiom/is p1 p2)
-  (define-axiom (is p1 p2) (x) (is (p1 x) (p2 x))))
-
-(define-syntax-rule (define-theorem/is p1 p2)
-  (define-theorem (is p1 p2) (x) (is (p1 x) (p2 x))))
-
-(define-syntax-rule (define-proof/is p1 p2 pc)
-  (define-proof (is p1 p2)
-    ((rewrite (2) if-same (set x (pc x)))
-     (rewrite (2 2 1) (is pc p2))
-     (eval (2 2))
-     (rewrite (2 1) (is p1 pc))
-     (rewrite (2) if-true)
-     (rewrite () if-same))))
-
-(define-syntax implies
-  (syntax-rules ()
-    ((_ x y) (if x y #t))
-    ((_ x y z ...) (if x (implies y z ...) #t))))
-
-(define-system prelude/macro ()
-  (define-syntax-rules cond (else)
-    ((cond (else e)) e)
-    ((cond (test then) . rest)
-     (if test then (cond . rest))))
-  (define-syntax-rules or ()
-    ((or) '#f)
-    ((or x) x)
-    ((or x . xs) (if x x (or . xs))))
-  (define-syntax-rules implies ()
-    ((implies x y) (if x y #t))
-    ((implies x y z . rest)
-     (if x (implies y z . rest) #t)))
-  (define-syntax-rules predicate ()
-    ((predicate x) (implies x (equal? x #t))))
-  (define-syntax-rules is ()
-    ((is x y) (implies x (equal? y #t)))))
-
-(define-system prelude/axiom/equal (prelude/macro)
-  (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 equal-if-false (x y)
-    (if x #t (equal? x #f))))
-
-(define-system prelude/axiom/if (prelude/axiom/equal)
-  (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-system prelude/number (prelude/axiom/if)
-  (define-core-function number? (x) number?)
-  (define-axiom (predicate number?) (x) (predicate (number? x)))
-
-  (define-core-function real? (x) real?)
-  (define-axiom (predicate real?) (x) (predicate (real? x)))
-  (define-axiom/is real? number?)
-
-  (define-core-function integer? (x) integer?)
-  (define-axiom (predicate integer?) (x) (predicate (integer? x)))
-  (define-axiom/is integer? real?)
-  (define-theorem/is integer? number?)
-  (define-proof/is integer? number? real?)
-
-  (define-core-function/guard exact? (x) (number? x) exact?)
-  (define-axiom (predicate exact?) (x) (predicate (exact? x)))
-  (define-function/guard inexact? (x)
-    (number? x)
-    (not (exact? x)))
-  (define-theorem (predicate inexact?) (x) (predicate (inexact? x)))
-
-  (define-core-function exact-integer? (x) exact-integer?)
-  (define-axiom (predicate exact-integer?) (x) (predicate (exact-integer? x)))
-  (define-axiom/is exact-integer? integer?)
-  (define-axiom/is exact-integer? exact?)
-  (define-theorem/is exact-integer? real?)
-  (define-proof/is exact-integer? real? integer?)
-  (define-theorem/is exact-integer? number?)
-  (define-proof/is exact-integer? number? real?)
-  (define-core-function/guard < (x y) (and (real? x) (real? y)) <)
-  (define-axiom (predicate <) (x y) (predicate (< x y)))
-
-  (define-function/guard positive? (x)
-    (real? x)
-    (< 0 x))
-  (define-theorem (predicate positive?) (x) (predicate (positive? x)))
-  (define-function/guard negative? (x)
-    (real? x)
-    (< x 0))
-  (define-theorem (predicate negative?) (x) (predicate (negative? x)))
-
-  (define-function exact-positive-integer? (x)
-    (and (exact-integer? x)
-         (positive? x)))
-  (define-theorem (predicate exact-positive-integer?) (x)
-    (predicate (exact-positive-integer? x)))
-  (define-theorem/is exact-positive-integer? exact-integer?)
-
-  (define-function exact-zero? (x) (equal? x 0))
-  (define-theorem (predicate exact-zero?) (x)
-    (predicate (exact-zero? x)))
-  (define-theorem/is exact-zero? exact-integer?)
-
-  (define-function natural? (x)
-    (if (exact-zero? x)
-        #t
-        (exact-positive-integer? x)))
-  (define-theorem (predicate natural?) (x)
-    (predicate (natural? x)))
-  (define-theorem/is natural? exact-integer?))
-
-(define-system prelude/measure/natural (prelude/number)
-  (set-measure-predicate natural?)
-  (set-measure-predicate <))
-
-(define-system prelude/pair (prelude/measure/natural)
-  (define-core-function pair? (x) pair?)
-  (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-system prelude (prelude/pair)
-  (define-proof inexact?
-    ((rewrite (2) if-nest)
-     (rewrite () if-same)))
-  (define-proof (predicate inexact?)
-    ((rewrite (1) inexact?)
-     (rewrite () if-not)
-     (rewrite (3 1) inexact?)
-     (rewrite (3 1 1) equal-if-false)
-     (eval (3))
-     (rewrite () if-same)))
-  (define-proof positive?
-    ((eval (2 1 1))
-     (rewrite (2 1) if-true)
-     (rewrite (2) if-nest)
-     (rewrite () if-same)))
-  (define-proof (predicate positive?)
-    ((rewrite (1) positive?)
-     (rewrite (2 1) positive?)
-     (rewrite (2 1) (predicate <))
-     (eval (2))
-     (rewrite () if-same)))
-  (define-proof negative?
-    ((rewrite (2 1) if-nest)
-     (eval (2 1))
-     (rewrite (2) if-true)
-     (rewrite () if-same)))
-  (define-proof (predicate negative?)
-    ((rewrite (1) negative?)
-     (rewrite (2 1) negative?)
-     (rewrite (2 1) (predicate <))
-     (eval (2))
-     (rewrite () if-same)))
-  (define-proof exact-positive-integer?
-    ((rewrite (1 2) (is exact-integer? real?))
-     (rewrite (1) if-same)
-     (eval ())))
-  (define-proof (predicate exact-positive-integer?)
-    ((rewrite (1) exact-positive-integer?)
-     (rewrite () if-same (set x (exact-integer? x)))
-     (rewrite (3 1) if-nest)
-     (rewrite (3) if-false)
-     (rewrite (2 1) if-nest)
-     (rewrite (2 2 1) exact-positive-integer?)
-     (rewrite (2 2 1 1) (predicate exact-integer?))
-     (rewrite (2 2 1 2) (predicate positive?))
-     (eval (2 2))
-     (rewrite (2) if-same)
-     (rewrite () if-same)))
-  (define-proof (predicate exact-zero?)
-    ((rewrite (1) exact-zero?)
-     (rewrite (2 1 1) equal-if)
-     (eval (2))
-     (rewrite () if-same)))
-  (define-proof (predicate natural?)
-    ((rewrite (1) natural?)
-     (rewrite () if-same (set x (exact-zero? x)))
-     (rewrite (2 1) if-nest)
-     (rewrite (2) if-true)
-     (rewrite (3 1) if-nest)
-     (rewrite (1) exact-zero?)
-     (rewrite (2 1 1) equal-if)
-     (eval (2))
-     (rewrite (1) exact-zero?)
-     (rewrite (3 2 1) natural?)
-     (rewrite (3 2 1) if-nest)
-     (rewrite (3 2 1) (predicate exact-positive-integer?))
-     (eval (3 2))
-     (rewrite (3) if-same)
-     (rewrite () if-same)))
-  )
diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm
deleted file mode 100644
index fe7735e..0000000
--- a/vikalpa/the-little-prover.scm
+++ /dev/null
@@ -1,163 +0,0 @@
-;;; Vikalpa --- Proof Assistant
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
-;;;
-;;; This file is part of Vikalpa.
-;;;
-;;; Vikalpa is free software; you can redistribute it and/or modify it
-;;; under the terms of the GNU General Public License as published by
-;;; the Free Software Foundation; either version 3 of the License, or
-;;; (at your option) any later version.
-;;;
-;;; Vikalpa is distributed in the hope that it will be useful, but
-;;; WITHOUT ANY WARRANTY; without even the implied warranty of
-;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-;;; General Public License for more details.
-;;;
-;;; You should have received a copy of the GNU General Public License
-;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
-
-(define-module (vikalpa the-little-prover)
-  #:export (atom? nat? the-little-prover)
-  #:use-module (vikalpa))
-
-(define (atom? x)
-  (not (pair? x)))
-
-(define (nat? x)
-  (and (integer? x)
-       (<= 0 x)))
-
-(define-system the-little-prover ()
-  (define-core-function atom? (x) atom?)
-  (define-core-function nat? (x) nat?)
-  (define-core-function < (x y)
-    (lambda (x y)
-      (if (number? x)
-          (if (number? y)
-              (< x y)
-              (< x 0))
-          (if (number? y)
-              (< 0 y)
-              #f))))
-  (set-measure-predicate nat?)
-  (set-measure-less-than <)
-  (define-core-function + (x y)
-    (lambda (x y)
-      (if (number? x)
-          (if (number? y)
-              (+ x y)
-              x)
-          (if (number? y)
-              y
-              0))))
-  (define-core-function cons (x y) cons)
-  (define-core-function car (x)
-    (lambda (x)
-      (if (atom? x) '() (car x))))
-  (define-core-function cdr (x)
-    (lambda (x)
-      (if (atom? x) '() (cdr x))))
-  (define-trivial-total-function size (x)
-    (if (atom? x)
-        0
-        (+ 1
-           (+ (size (car x))
-              (size (cdr x))))))
-
-  ;; Axioms of Equal
-  (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)
-    (if (equal? x y) (equal? x y) #t))
-
-  ;; Axioms of Cons
-  (define-axiom atom/cons (x y)
-    (equal? (atom? (cons x y)) #f))
-  (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)))
-
-  ;; Axioms of If
-  (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-nest-A (x y z)
-    (if x (equal? (if x y z) y) #t))
-  (define-axiom if-nest-E (x y z)
-    (if x #t (equal? (if x y z) z)))
-
-  ;; Axioms of Size
-  (define-axiom nat/size (x)
-    (equal? (nat? (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)))
-
-  ;; Axioms of `+` and `<`
-  (define-axiom identity-+ (x)
-    (if (nat? x)
-        (equal? (+ 0 x) x)
-        #t))
-  (define-axiom commute-+ (x y)
-    (equal? (+ x y) (+ y x)))
-  (define-axiom associate-+ (x y z)
-    (equal? (+ (+ x y) z) (+ x (+ y z))))
-  (define-axiom positive-+ (x y)
-    (if (< '0 x)
-        (if (< '0 y)
-            (equal? (< '0 (+ x y)) #t)
-            #t)
-        #t))
-  (define-axiom nat/+ (x y)
-    (if (nat? x)
-        (if (nat? y)
-            (equal? (nat? (+ x y)) #t)
-            #t)
-        #t))
-  (define-axiom common-addends-< (x y z)
-    (equal? (< (+ x z) (+ y z))
-            (< x y)))
-  
-  ;; Prelude
-  (define-function list-induction (x)
-    (if (atom? x)
-        x
-        (cons (car x)
-              (list-induction (cdr x)))))
-
-  (define-function star-induction (x)
-    (if (atom? x)
-        x
-        (cons (star-induction (car x))
-              (star-induction (cdr x)))))
-
-  (define-proof list-induction
-    (size x)
-    (((2 3) size/cdr)
-     ((2) if-same)
-     ((1) nat/size)
-     (() if-true)))
-
-  (define-proof star-induction
-    (size x)
-    (((2 3 1) size/car)
-     ((2 3 2) size/cdr)
-     ((2 3) if-true)
-     ((2) if-same)
-     ((1) nat/size)
-     (() if-true))))