a formula should be an instance of itself (#1668)

Proof checking failed when applying the instantiation rule so that the original formula and the instantiated formula are the same. Fixed using the new "ifequal" construct in lfsc.

diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf
index e212f835dfc421ef5a19f08d0b331aae85a93cb4..9fa6979788aa656c74b0d40d6cfbda8bee1ac7b5 100644 (file)
--- a/proofs/signatures/th_quant.plf
+++ b/proofs/signatures/th_quant.plf
@@ -3,18 +3,19 @@
                 (! f formula
                   formula))))
 
-(program eqterm ((n1 term) (n2 term)) bool
-    (do (markvar n1)
-        (let s (ifmarked n2 tt ff)
-           (do (markvar n1) s))))
+;This program recursively checks the instantiation.
+;Composite terms (such as "apply _ _ ...") are handled recursively.
+;Then, if ti and t are equal, we return true. Otherwise, we first verify that t is the variable for which ti is substitued (ifmarked). if this is the case, ti should be equal to k.
 
 (program is_inst_t ((ti term) (t term) (k term)) bool
-  (match t
-    ((apply s1 s2 t1 t2)
-      (match ti
-        ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
-        (default ff)))
-    (default (eqterm ti (ifmarked t k t)))))
+ (match t
+   ((apply s1 s2 t1 t2)
+     (match ti
+       ((apply si1 si2 ti1 ti2) 
+           (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
+       (default ff)))
+   (default (ifequal ti t tt (ifmarked t (ifequal ti k tt ff) ff)))))
+
 
 (program is_inst_f ((fi formula) (f formula) (k term)) bool
   (match f