Replace from core-system/equal to core-system/equal-t-nil.

3 files changed, 491 insertions, 37 deletions

diff --git a/Makefile.am b/Makefile.am
index 4d43492..44052ed 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -44,8 +44,9 @@ bin_SCRIPTS =
 SOURCES =                       \
   vikalpa.scm
 
-TESTS =                  \
-  tests/test-vikalpa.scm
+TESTS =                              \
+  tests/test-vikalpa.scm             \
+  tests/test-vikalpa-equal-t-nil.scm
 
 TEST_EXTENSIONS = .scm
 
diff --git a/tests/test-vikalpa-equal-t-nil.scm b/tests/test-vikalpa-equal-t-nil.scm
new file mode 100644
index 0000000..251fd10
--- /dev/null
+++ b/tests/test-vikalpa-equal-t-nil.scm
@@ -0,0 +1,432 @@
+;;; 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 (tests vikalpa-equal-t-nil)
+  #:use-module (srfi srfi-64)
+  #:use-module (vikalpa))
+
+(define-syntax-rule (if/nil test t f)
+  (if (equal? test 'nil)
+      f
+      t))
+
+(define (bool->t/nil x)
+  (if x
+      't
+      'nil))
+
+(define-system test/defs (core-system/equal-t-nil)
+  (define-syntax-rules implies ()
+    ((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 equal-if-false (x y)
+    (if x 't (equal x 'nil)))
+  (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 'nil 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-core-function natural? (x)
+    (lambda (x)
+      (bool->t/nil (and (exact-integer? x)
+                        (<= 0 x)))))
+  (define-core-function/guard < (x y)
+    (and (natural? x) (natural? y))
+    (lambda (x y)
+      (bool->t/nil (< x y))))
+  (define-core-function/guard + (x y)
+    (and (natural? x) (natural? y))
+    +)
+  (set-measure-predicate natural?)
+  (set-measure-less-than <)
+  (define-core-function pair? (x) (compose bool->t/nil 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-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 (pair? cons) (x y)
+    (equal (pair? (cons x y)) 't))
+  (define-axiom (eliminate cons) (x)
+    (implies (pair? x)
+             (equal (cons (car x) (cdr x)) x)))
+  (define-axiom (predicate pair?) (x)
+    (implies (pair? x) (equal (pair? x) 't)))
+
+  (define-function size (x)
+    (if (pair? x)
+        (+ (size (car x))
+           (size (cdr x)))
+        1))
+  (admit size)
+  (define-axiom (natural? size) (x)
+    (equal (natural? (size x)) 't))
+  (define-axiom (< size car) (x)
+    (implies (natural? x)
+             (equal (< (size (car x)) (size x)) 't)))
+  (define-axiom (< size cdr) (x)
+    (implies (pair? x)
+             (equal (< (size (cdr x)) (size x)) 't)))
+  (define-guard-theorem size)
+
+  (define-function null? (x)
+    (equal x '()))
+  (define-theorem (predicate null?) (x)
+    (implies (null? x) (equal (null? x) 't)))
+  (define-theorem (substitute null?) (x)
+    (implies (null? x) (equal x '())))
+
+  (define-function cdr-induction (x)
+    (if (pair? x)
+        (cons (car x) (cdr-induction (cdr x)))
+        '()))
+  (define-guard-theorem cdr-induction)
+
+  (define-function list? (x)
+    (if (null? x)
+        't
+        (if (pair? x)
+            (list? (cdr x))
+            'nil)))
+  (define-guard-theorem list?)
+
+  (define-theorem (predicate list?) (x)
+    (implies (list? x) (equal (list? x) 't)))
+  (define-theorem (is null? list?) (x)
+    (implies (null? x) (equal (list? x) 't)))
+  (define-theorem (is pair? (o list? cdr) list?) (x)
+    (implies (pair? x)
+             (list? (cdr x))
+             (equal (list? x) 't)))
+  (define-theorem (is list? (o not null?) pair?) (x)
+    (implies (list? x)
+             (not (null? x))
+             (equal (pair? x) 't)))
+
+  (define-theorem (is-not pair? null?) (x)
+    (implies (pair? x)
+             (equal (null? x) 'nil)))
+
+  (define-theorem (is list? pair? (o list? cdr)) (x)
+    (implies (list? x)
+             (pair? x)
+             (equal (list? (cdr x)) 't)))
+
+  (define-theorem (is list? (o not pair?) null?) (x)
+    (implies (list? x)
+             (not (pair? x))
+             (equal (null? x) 't)))
+
+  (define-function/guard append (x y)
+    (and (list? x) (list? y))
+    (if (null? x)
+        y
+        (cons (car x) (append (cdr x) y))))
+  (define-guard-theorem append)
+
+  (define-theorem (substitute (append null? _)) (x)
+    (equal (append '() x) x))
+
+  (define-theorem (associative append) (x y z)
+    (implies (list? x)
+             (list? y)
+             (list? z)
+             (equal (append (append x y) z)
+                    (append x (append y z))))))
+
+(define-system test/proofs (test/defs)
+  (define-proof (predicate null?)
+    ((rewrite (1) null?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2 1))
+     (rewrite (2) equal-same)
+     (rewrite () if-same)))
+
+  (define-proof (guard size)
+    ((rewrite (2 1) (natural? size))
+     (rewrite (2 2 1) (natural? size))
+     (rewrite (2 2 2 1) (predicate pair?))
+     (rewrite (2 2 2 2) (predicate pair?))
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (guard cdr-induction)
+    ((rewrite (2) if-nest)
+     (rewrite (2) (predicate pair?))
+     (rewrite () if-same)))
+
+  (define-proof list?
+    (size x)
+    ((rewrite (1) (natural? size))
+     (rewrite () if-true)
+     (rewrite (3 2) (< size cdr))
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (guard list?)
+    ((rewrite (3 2) (predicate pair?))
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (substitute null?)
+    ((rewrite (1) null?)
+     (rewrite (2 1) equal-if)
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (predicate list?)
+    (cdr-induction x)
+    ((rewrite (2) if-same (= x (list? (cdr x))))
+     (rewrite (2 2 1) if-nest)
+     (rewrite (2 2 2 2 1) list?)
+     (rewrite (2 2 2 2 1 3 2) equal-if)
+     (rewrite (2 2 2 2 1 3) if-nest)
+     (rewrite (2 2 2 2 1) if-same)
+     (rewrite (2 2 2 2) equal-same)
+     (rewrite (2 2 2) if-same)
+     (rewrite (2 2) if-same)
+     (rewrite (2 3 1) if-nest)
+     (rewrite (2 3) if-true)
+     (rewrite (2 3 1) list?)
+     (rewrite (2 3 1 3) if-nest)
+     (rewrite (2 3) if-same (= x (null? x)))
+     (rewrite (2 3 2 1) if-nest)
+     (rewrite (2 3 2) if-true)
+     (rewrite (2 3 2 1 1) (substitute null?))
+     (eval (2 3 2))
+     (rewrite (2 3 3 1) if-nest)
+     (rewrite (2 3 3) if-nest)
+     (rewrite (2 3) if-same)
+     (rewrite (2) if-same)
+     (rewrite (3 1) list?)
+     (rewrite (3) if-same (= x (null? x)))
+     (rewrite (3 2 1) if-nest)
+     (rewrite (3 2) if-true)
+     (rewrite (3 2 1 1) (substitute null?))
+     (eval (3 2))
+     (rewrite (3 3 1) if-nest)
+     (rewrite (3 3 1) if-nest)
+     (rewrite (3 3) if-false)
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is null? list?)
+    ((rewrite (1) null?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (is pair? (o list? cdr) list?)
+    ((rewrite (2 2 1) list?)
+     (rewrite (2 2 1 3 2) (predicate list?))
+     (rewrite (2 2 1 3) if-nest)
+     (rewrite (2 2 1) if-same)
+     (rewrite (2 2) equal-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof cdr-induction
+    (size x)
+    ((rewrite (1) (natural? size))
+     (rewrite () if-true)
+     (rewrite (2) (< size cdr))
+     (rewrite () if-same)))
+
+  (define-proof (is list? (o not null?) pair?)
+    ((rewrite (2) if-not)
+     (rewrite (1) list?)
+     (rewrite () if-same (= x (null? x)))
+     (rewrite (2 1) if-nest)
+     (rewrite (2) if-true)
+     (rewrite (2) if-nest)
+     (rewrite (3 1) if-nest)
+     (rewrite (3) if-same (= x (pair? x)))
+     (rewrite (3 2 1) if-nest)
+     (rewrite (3 2 2 3 1) (predicate pair?))
+     (rewrite (3 2 2 3) equal-same)
+     (rewrite (3 2 2) if-same)
+     (rewrite (3 2) if-same)
+     (rewrite (3 3 1) if-nest)
+     (rewrite (3 3) if-false)
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is-not pair? null?)
+    ((rewrite () if-same (= x (null? x)))
+     (rewrite (2 1 1) (substitute null?))
+     (eval (2 1))
+     (rewrite (2) if-false)
+     (rewrite (3 2 1) equal-if-false)
+     (rewrite (3 2) equal-same)
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is list? pair? (o list? cdr))
+    ((rewrite () if-same (= x (pair? x)))
+     (rewrite (2 2) if-nest)
+     (rewrite (3 2) if-nest)
+     (rewrite (3) if-same)
+     (rewrite (2 1) list?)
+     (rewrite (2 1 1) (is-not pair? null?))
+     (rewrite (2 1) if-false)
+     (rewrite (2 1) if-nest)
+     (rewrite (2 2 1) (predicate list?))
+     (eval (2 2))
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof append
+    (size x)
+    ((rewrite (2 2 1) (natural? size))
+     (rewrite (2 2) if-true)
+     (rewrite (2 2 3) if-same (= x (pair? x)))
+     (rewrite (2 2 3 2) (< size cdr))
+     (rewrite (2 2 3 1) (is list? (o not null?) pair?))
+     (rewrite (2 2 3) if-true)
+     (rewrite (2 2) if-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (guard append)
+    ((rewrite (2 2 3 2 2 2) (predicate pair?))
+     (rewrite (2 2 3 2 2) if-nest)
+     (rewrite (2 2 3 2 1) (is list? pair? (o list? cdr)))
+     (rewrite (2 2 3 2) if-true)
+     (rewrite (2 2 3 1) (is list? (o not null?) pair?))
+     (rewrite (2 2 3) if-true)
+     (rewrite (2 2) if-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is list? (o not pair?) null?)
+    ((rewrite (2) if-not)
+     (rewrite () if-same (= x (pair? x)))
+     (rewrite (2 2) if-nest)
+     (rewrite (2) if-same)
+     (rewrite (3 2) if-nest)
+     (rewrite (3 1) list?)
+     (rewrite (3) if-same (= x (null? x)))
+     (rewrite (3 2 1) if-nest)
+     (rewrite (3 2) if-true)
+     (rewrite (3 2 1) (predicate null?))
+     (eval (3 2))
+     (rewrite (3 3 1) if-nest)
+     (rewrite (3 3 1) if-nest)
+     (rewrite (3 3) if-false)
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (substitute (append null? _))
+    ((rewrite (1) append)
+     (eval (1 1))
+     (rewrite (1) if-true)
+     (rewrite () equal-same)))
+
+  (define-proof (associative append)
+    (cdr-induction x)
+    ((rewrite (3 2 2 2) if-same (= x (null? x)))
+     (rewrite (3 2 2 2 2 1 1 1) (substitute null?))
+     (rewrite (3 2 2 2 2 2 1) (substitute null?))
+     (rewrite (3 2 2 2 1) (is list? (o not pair?) null?))
+     (rewrite (3 2 2 2) if-true)
+     (rewrite (3 2 2 2 1 1) (substitute (append null? _)))
+     (rewrite (3 2 2 2 2) (substitute (append null? _)))
+     (rewrite (3 2 2 2) equal-same)
+     (rewrite (3 2 2) if-same)
+     (rewrite (3 2) if-same)
+     (rewrite (3) if-same)
+     (rewrite (2) if-same (= x (list? y)))
+     (rewrite (2 2 1 2) if-nest)
+     (rewrite (2 2 2 2) if-nest)
+     (rewrite (2 3 1 2) if-nest)
+     (rewrite (2 3 2 2) if-nest)
+     (rewrite (2 3 1) if-same)
+     (rewrite (2 3) if-true)
+     (rewrite (2 3) if-same)
+     (rewrite (2 2) if-same (= x (list? z)))
+     (rewrite (2 2 2 1 2) if-nest)
+     (rewrite (2 2 2 2 2) if-nest)
+     (rewrite (2 2 3 1 2) if-nest)
+     (rewrite (2 2 3 2 2) if-nest)
+     (rewrite (2 2 3 1) if-same)
+     (rewrite (2 2 3) if-true)
+     (rewrite (2 2 3) if-same)
+     (rewrite (2 2 2) if-same (= x (list? (cdr x))))
+     (rewrite (2 2 2 2 1) if-nest)
+     (rewrite (2 2 2 3 1) if-nest)
+     (rewrite (2 2 2 3) if-true)
+     (rewrite (2 2 2 2 2 2 2) append)
+     (rewrite (2 2 2 2 2 2 2 1) (is-not pair? null?))
+     (rewrite (2 2 2 2 2 2 2) if-false)
+     (rewrite (2 2 2 2 2 2 2 2) equal-if)
+     (rewrite (2 2 2 2 2 2 1 1) append)
+     (rewrite (2 2 2 2 2 2 1 1 1) (is-not pair? null?))
+     (rewrite (2 2 2 2 2 2 1 1) if-false)
+     (rewrite (2 2 2 2 2 2 1) append)
+     (rewrite (2 2 2 2 2 2 1) if-same
+              (= x (pair? (cons (car x) (append (cdr x) y)))))
+     (rewrite (2 2 2 2 2 2 1 2 1) (is-not pair? null?))
+     (rewrite (2 2 2 2 2 2 1 1) (pair? cons))
+     (rewrite (2 2 2 2 2 2 1) if-true)
+     (rewrite (2 2 2 2 2 2 1) if-false)
+     (rewrite (2 2 2 2 2 2 1 1) (car cons))
+     (rewrite (2 2 2 2 2 2 1 2 1) (cdr cons))
+     (rewrite (2 2 2 2 2 2) equal-same)
+     (rewrite (2 2 2 2 2) if-same)
+     (rewrite (2 2 2 2) if-same)
+     (rewrite (2 2 2) if-same (= x (list? x)))
+     (rewrite (2 2 2 2 1) (is list? pair? (o list? cdr)))
+     (rewrite (2 2 2 2) if-true)
+     (rewrite (2 2 2 3 3) if-nest)
+     (rewrite (2 2 2 3) if-same)
+     (rewrite (2 2 2) if-same)
+     (rewrite (2 2) if-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same))))
+
+(define-system test (test/proofs))
+
+(test-begin "test-vikalpa-equal-t-nil")
+
+(test-equal '(result/expr b)
+  (system-rewrite (test)
+                  '(car (cdr (cons a (cons b c))))
+                  '((rewrite (1) (cdr cons))
+                    (rewrite () (car cons)))))
+
+(test-equal '()
+  (system-check (test)))
+
+(test-end "test-vikalpa-equal-t-nil")
diff --git a/vikalpa.scm b/vikalpa.scm
index 6a2af81..8c3d10c 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -26,7 +26,7 @@
             set-measure-predicate
             set-measure-less-than
             core-system
-            core-system/equal
+            core-system/equal-t-nil
             define-system
             define-proof
             define-core-function
@@ -61,12 +61,22 @@
     #:init-keyword #:definitions
     #:init-value '())
   (equal-symbol #:getter get-equal-symbol
-                #:init-value 'equal?)
+                #:init-value 'equal?
+                #:init-keyword #:equal-symbol)
+  (true-object #:getter get-true-object
+               #:init-value ''#t
+               #:init-keyword #:true-object)
+  (false-object #:getter get-false-object
+                #:init-value ''#f
+                #:init-keyword #:false-object)
   (measure-predicate #:getter get-measure-predicate
                      #:init-value #f)
   (measure-less-than #:getter get-measure-less-than
                      #:init-value #f))
 
+(define-syntax-rule (true) (get-true-object (current-system)))
+(define-syntax-rule (false) (get-false-object (current-system)))
+
 (define-class <definition> ()
   (name #:getter get-name
         #:init-keyword #:name)
@@ -132,11 +142,6 @@
           (equal? name (get-name x)))
         (get-definitions s)))
 
-(define-method (update-equal-symbol (s <symbol>) (sys <system>))
-  (let ((new (shallow-clone sys)))
-    (slot-set! new 'equal-symbol s)
-    new))
-
 (define-method (update-measure-predicate (s <symbol>) (sys <system>))
   (let ((new (shallow-clone sys)))
     (slot-set! new 'measure-predicate s)
@@ -1075,7 +1080,7 @@
                     #:guards (get-guards f)
                     #:expression (get-expression f)
                     #:code (get-code f)
-                    #:claim ''#t
+                    #:claim (true)
                     #:proof '())))
            (current-system (update-definition g (current-system)))
            (validate g)))
@@ -1116,7 +1121,7 @@
                            #:name (get-name d)
                            #:variables (get-variables d)
                            #:expression (get-expression d)
-                           #:claim ''#t
+                           #:claim (true)
                            #:proof '())
                          (make <admitted-function>
                            #:name (get-name d)
@@ -1124,7 +1129,7 @@
                            #:guards (get-guards d)
                            #:expression (get-expression d)
                            #:code (get-code d)
-                           #:claim ''#t
+                           #:claim (true)
                            #:proof '()))))
               (validate g)
               (current-system (update-definition g (current-system))))))
@@ -1145,15 +1150,24 @@
     (define-core-function equal? (x y) equal?)
     (current-system)))
 
-(define (core-system/equal)
-  (parameterize ((current-system (make <system>)))
-    (current-system (update-equal-symbol 'equal (current-system)))
+(define (core-system/equal-t-nil)
+  (parameterize ((current-system (make <system>
+                                   #:equal-symbol 'equal
+                                   #:true-object ''t
+                                   #:false-object ''nil)))
     (define-syntax-rules and ()
-      ((and) '#t)
+      ((and) 't)
       ((and x) x)
-      ((and x . xs) (if x (and . xs) #f)))
-    (define-core-function not (x) not)
-    (define-core-function equal (x y) equal?)
+      ((and x . xs) (if x (and . xs) 'nil)))
+    (define-core-function equal (x y) (lambda (x y)
+                                        (if (equal? x y)
+                                            't
+                                            'nil)))
+    (define-core-function not (x)
+      (lambda (x)
+        (if (eq? x 'nil)
+            't
+            'nil)))
     (current-system)))
 
 (define-syntax define-system
@@ -1216,28 +1230,28 @@
 (define (smart-if x y z)
   (cond
    ((equal? y z) y)
-   ((equal? x ''#t) y)
-   ((equal? x ''#f) z)
+   ((equal? x (true)) y)
+   ((equal? x (false)) z)
    (else `(if ,x ,y ,z))))
 
 (define (smart-and . args)
   (cond
-   ((null? args) ''#t)
-   ((equal? ''#t (car args)) (apply smart-and (cdr args)))
+   ((null? args) (true))
+   ((equal? (true) (car args)) (apply smart-and (cdr args)))
    (else
     (let ((rest (apply smart-and (cdr args))))
-      (if (equal? ''#t rest)
+      (if (equal? (true) rest)
           (car args)
           (smart-if (car args)
                     rest
-                    ''#f))))))
+                    (false)))))))
 
 (define (smart-implies x y)
   (cond
-   ((equal? ''#f x) ''#t)
-   ((equal? ''#t y) ''#t)
+   ((equal? (false) x) (true))
+   ((equal? (true) y) (true))
    (else
-    (smart-if x y ''#t))))
+    (smart-if x y (true)))))
 
 (define (make-totality-claim* m-expr f)
   (let* ((name (get-name f)))
@@ -1258,8 +1272,8 @@
     (smart-if `(,(get-measure-predicate (current-system)) ,m-expr)
               (let loop ((expr (get-expression f)))
                 (cond
-                 ((expr-quoted? expr) ''#t)
-                 ((variable? expr) ''#t)
+                 ((expr-quoted? expr) (true))
+                 ((variable? expr) (true))
                  ((if-form? expr)
                   (let ((test/result (loop (if-form-test expr)))
                         (then/result (loop (if-form-then expr)))
@@ -1271,7 +1285,7 @@
                  ((app-form? expr)
                   (let ((rest
                          (let f ((args (app-form-args expr)))
-                           (cond ((null? args) ''#t)
+                           (cond ((null? args) (true))
                                  ((single? args) (loop (car args)))
                                  (else (smart-and (loop (car args))
                                                   (f (cdr args))))))))
@@ -1284,7 +1298,7 @@
                  (else (error "(vikalpa) make-totality-claim: error"
                               (get-name f)
                               m-expr))))
-              ''#f)))
+              (false))))
 
 (define (make-guard-claim expr)
   (define (find-preconds expr)
@@ -1313,7 +1327,7 @@
                 (build (if-form-else expr))))
      ((app-form? expr)
       (apply smart-and (map build/find-if (app-form-args expr))))
-     (else ''#t)))
+     (else (true))))
   (define (build expr)
     (cond
      ((if-form? expr)
@@ -1326,7 +1340,7 @@
       (apply smart-and
              (append (find-preconds expr)
                      (list (build/find-if expr)))))
-     (else ''#t)))
+     (else (true))))
   (build expr))
 
 (define (make-induction-claim f vars c)
@@ -1368,7 +1382,7 @@
             ((if-form? expr)
              (let ((app-forms (find-app-forms (if-form-test expr))))
                (smart-implies (if (null? app-forms)
-                                  ''#t
+                                  (true)
                                   (fold smart-implies
                                         c
                                         (map prop app-forms)))
@@ -1607,7 +1621,7 @@
                 (if (lookup `(guard ,(get-name f)) (current-system))
                     #f
                     (if (equal? (make-guard-claim (get-expression f))
-                                ''#t)
+                                (true))
                         #f
                         `((guard ,(get-name f))
                           (add (define-guard-theorem ,(get-name f)))))))
@@ -1639,8 +1653,15 @@
                         (parameterize ((current-system sys))
                           (rewrite (get-claim d)
                                    (get-proof d))))))
+               (display
+                (list result
+                      (parameterize ((current-system sys))
+                        (result/expr (true)))))
+               (newline)
                (cond
-                ((equal? result (result/expr ''#t))
+                ((equal? result
+                         (parameterize ((current-system sys))
+                           (result/expr (true))))
                  (next))
                 (else
                  (next (list (get-name d) result))))))