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 /proofs/signatures | |
| 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.
Diffstat (limited to 'proofs/signatures')
| -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 |