wip32

1 files changed, 57 insertions, 0 deletions

diff --git a/examples/the-little-prover.scm b/examples/the-little-prover.scm
new file mode 100644
index 0000000..0a12eaa
--- /dev/null
+++ b/examples/the-little-prover.scm
@@ -0,0 +1,57 @@
+(use-modules (vikalpa)
+             (vikalpa the-little-prover)
+             (ice-9 pretty-print))
+
+(define-system the-little-prover-0 (the-little-prover)
+  (define-theorem simple-list-induction (x)
+    (equal? (if (natural? (size x))
+                (if (atom? x) '#t (< (size (cdr x)) (size x)))
+                '#t)
+            #t))
+
+  (define-proof simple-list-induction
+    ()
+    (((1 2 3) size/cdr)
+     ((1 2) if-same)
+     ((1) if-same)
+     (() equal-same)))
+
+  (define-function list-length (xs)
+    (if (atom? xs)
+        '0
+        (+ '1 (list-length (cdr xs)))))
+
+  (define-proof list-length
+    (natural? (size xs))
+    ((() simple-list-induction)))
+
+  (define-theorem natural?/1 ()
+    (equal? (natural? 1) #t))
+
+  (define-proof natural?/1
+    ()
+    ((() if-same (set x (natural? '0)))
+     ((2 1) natural?/succ)
+     ((2) equal-same)
+     ((1) natural?/0)
+     (() if-true)))
+
+  (define-theorem natural?/list-length (xs)
+    (natural? (list-length xs)))
+
+  (define-proof natural?/list-length
+    (list-induction xs)
+    (((2 1) list-length)
+     ((2 1) if-nest-A)
+     ((2) natural?/0)
+     ((3 2 1) list-length)
+     ((3 2 1) if-nest-E)
+     ((3) if-same (set x (natural? (succ '0))))
+     ((3 2 2) natural?/+
+      ;; ルール探索アルゴリズムにバグがある
+      (set x (succ '0))
+      (set y (list-length (cdr xs))))
+     ((3 2) if-same)
+     ((3 1) natural?/1)
+     ((3) if-true)
+     (() if-same))))