diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2018-04-02 14:15:02 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-02 14:15:02 -0700 |
| commit | 065adbb66136022236efb73af740ff6b2c0f178a (patch) | |
| tree | 1abcf462bb6fd175d7a5542bcbd9a1a555333543 | |
| parent | 75d15b2cd923f92fd26020e0c8d1786b4396d608 (diff) | |
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.
| -rw-r--r-- | proofs/signatures/th_quant.plf | 21 |
1 files 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 |