From 065adbb66136022236efb73af740ff6b2c0f178a Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 2 Apr 2018 14:15:02 -0700 Subject: [PATCH] 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. --- proofs/signatures/th_quant.plf | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf index e212f835d..9fa697978 100644 --- 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 -- 2.30.2