From 3586ed9e429c37c0e3532a631f9644e7b7f3fe3a Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 16 Jan 2021 22:41:22 +0900
Subject: wip80

---
 examples/prelude.scm | 426 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 426 insertions(+)
 create mode 100644 examples/prelude.scm

(limited to 'examples')

diff --git a/examples/prelude.scm b/examples/prelude.scm
new file mode 100644
index 0000000..f171b6e
--- /dev/null
+++ b/examples/prelude.scm
@@ -0,0 +1,426 @@
+;;; 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 (size 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))))
+
+(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)))
+    ((is x y . ys) (implies x (is y . ys)))))
+
+(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-theorem/is exact-positive-integer? exact?)
+  (define-proof/is exact-positive-integer? exact? exact-integer?)
+  (define-theorem/is exact-positive-integer? integer?)
+  (define-proof/is exact-positive-integer? integer? exact-integer?)
+  (define-theorem/is exact-positive-integer? real?)
+  (define-proof/is exact-positive-integer? real? exact-integer?)
+  (define-theorem/is exact-positive-integer? number?)
+  (define-proof/is exact-positive-integer? number? 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-theorem/is exact-zero? integer?)
+  (define-proof/is exact-zero? integer? exact-integer?)
+  (define-theorem/is exact-zero? exact?)
+  (define-proof/is exact-zero? exact? exact-integer?)
+  (define-theorem/is exact-zero? real?)
+  (define-proof/is exact-zero? real? exact-integer?)
+  (define-theorem/is exact-zero? number?)
+  (define-proof/is exact-zero? number? real?)
+
+  (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-theorem/is natural? integer?)
+  (define-proof/is natural? integer? exact-integer?)
+  (define-theorem/is natural? exact?)
+  (define-proof/is natural? exact? exact-integer?)
+  (define-theorem/is natural? real?)
+  (define-proof/is natural? real? exact-integer?)
+  (define-theorem/is natural? number?)
+  (define-proof/is natural? number? real?)
+
+  (define-theorem/is exact-zero? natural?)
+  (define-theorem/is exact-positive-integer? natural?)
+
+  (set-measure-predicate natural?)
+  (set-measure-less-than <)
+
+(define-core-function/guard + (x y) (and (number? x) (number? y)) +)
+  (define-core-function/guard - (x y) (and (number? x) (number? y)) -)
+  (define-function/guard succ (x) (natural? x) (+ x 1))
+  (define-function/guard pred (x) (exact-positive-integer? x) (- x 1))
+  (define-function/guard natural-induction (x)
+    (natural? x)
+    (if (exact-zero? x)
+        #t
+        (succ (natural-induction (pred x)))))
+  (admit natural-induction)
+
+  (define-axiom (+ natural? natural?) (x y)
+    (implies (natural? x)
+             (natural? y)
+             (equal? (+ x y)
+                     (if (exact-zero? x)
+                         y
+                         (succ (+ (pred x) y))))))
+  (define-axiom pred/succ (x)
+    (implies (natural? x)
+             (equal? (pred (succ x)) x)))
+  (define-theorem succ/pred (x)
+    (implies (exact-positive-integer? x)
+             (equal? (succ (pred x)) x)))
+  (define-theorem (is natural? (o natural? succ)) (x)
+    (is (natural? x) (natural? (succ x))))
+
+  (define-theorem (is (o natural? pred) natural?) (x)
+    (is (natural? (pred x))
+        (natural? x)))
+
+  (define-axiom pred/zero (x)
+    (equal? (natural? (pred 0)) #f))
+
+  (define-theorem (is (o not natural?) (o not natural? pred)) (x)
+    (is (not (natural? x))
+        (not (natural? (pred x)))))
+  
+  (define-theorem (is (o natural?)
+                      (o not exact-zero?)
+                      exact-positive-integer?)
+    (x)
+    (is (not (natural? x))
+        (not (exact-zero? x))
+        (exact-positive-integer? x)))
+
+  (define-function/guard natural-induction-+ (x y)
+    (and (natural? x) (natural? y))
+    (if (exact-zero? x)
+        y
+        (succ (natural-induction-+ (pred x) y))))
+  (admit natural-induction-+)
+
+  (define-theorem (is natural? (o not exact-zero?) exact-positive-integer?) (x)
+    (is (natural? x)
+        (not (exact-zero? x))
+        (exact-positive-integer? x)))
+  
+  (define-theorem (implies natural?
+                           (equal? (o natural? pred)
+                                   exact-positive-integer?))
+    (x)
+    (implies (natural? x)
+             (equal? (natural? (pred x))
+                     (exact-positive-integer? x))))
+  
+  (define-theorem (+ (-> natural? natural? natural?)) (x y)
+    (implies (natural? x)
+             (natural? y)
+             (natural? (+ x y)))))
+
+(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-core-function size (x) size))
+
+(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)))
+  (define-proof (is exact-positive-integer? exact-integer?)
+    ((rewrite (1) exact-positive-integer?)
+     (rewrite () if-same (set x (exact-integer? x)))
+     (rewrite (3 1) if-nest)
+     (rewrite (2 1) if-nest)
+     (rewrite (2 2 1) (predicate exact-integer?))
+     (eval (2 2))
+     (rewrite (2) if-same)
+     (rewrite (3) if-false)
+     (rewrite ()  if-same)))
+  (define-proof (is exact-zero? exact-integer?)
+    ((rewrite (1) exact-zero?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite () if-same)))
+  (define-proof (is natural? exact-integer?)
+    ((rewrite (1) natural?)
+     (rewrite () if-same (set x (exact-zero? x)))
+     (rewrite (2 1) if-nest)
+     (rewrite (2) if-true)
+     (rewrite (2 1) (is exact-zero? exact-integer?))
+     (eval (2))
+     (rewrite (3 1) if-nest)
+     (rewrite (3 2 1) (is exact-positive-integer? exact-integer?))
+     (eval (3 2))
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+  (define-proof succ
+    ((rewrite (2 1 1) (is natural? number?))
+     (eval (2))
+     (rewrite ()  if-same)))
+  (define-proof pred
+    ((rewrite (2 1 1) (is exact-positive-integer? number?))
+     (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?))
+     (rewrite (2 2 2 1) if-nest)
+     (rewrite (2 2 2) (predicate natural?))
+     (rewrite (2 2 3 2) if-same (set x (natural? (pred x))))
+     (rewrite (2 2 3 2 2 1) (+ natural? natural?))
+     (rewrite (2 2 3 2 2 1) if-nest)
+     (rewrite (2 2 3 2 2) (is natural? (o natural? succ)))
+     (rewrite (2 2 3 2 1) (implies natural?
+                                   (equal? (o natural? pred)
+                                           exact-positive-integer?)))
+     (rewrite (2 2 3 2 1) (is natural? (o not exact-zero?)
+                              exact-positive-integer?))
+     (rewrite (2 2 3 2) if-true)
+     (rewrite (2 2 3) if-same)
+     (rewrite (2 2) if-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is exact-zero? natural?)
+    ((rewrite (1) exact-zero?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite ()  if-same)))
+
+  (define-proof (is exact-positive-integer? natural?)
+    ((rewrite (2 1) natural?)
+     (rewrite (2 1 3) (predicate exact-positive-integer?))
+     (rewrite (2 1) if-same)
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (is (o natural? pred) natural?)
+    ((rewrite () if-same (set x (natural? x)))
+     (rewrite (2 2 1) (predicate natural?))
+     (eval (2 2))
+     (rewrite (3 2 1) equal-if-false)
+     (eval (3 2))
+     (rewrite (2) if-same))))
-- 
cgit v1.2.3