2019-09-04 9:39:19 (GMT)
The boolean theory currently interacts badly with lambda-expressions. For example, if I want to derive a contradiction from
(fun u v. u = b && v = b) c != (fun v. c = b && v = b)
the boolean theory will replace the boolean subterms by tseitin_and_0 and tseitin_and_1, ignoring that these boolean subterms contain bound variables:
(fun u v. tseitin_and_0) c != (fun v. tseitin_and_1)
As a consequence, beta-reduction does not allow to prove false any more.
2019-09-04 9:43:6 (GMT)
I only see two options here: either we add some kind of support for bound variables into sidekick or we make non-closed terms opaque. The latter has the disadvantage that we won't be able to rewrite below binders any more.
2019-09-04 10:10:25 (GMT)
Here's another idea: could we do the replacement by the tseitin_and_ constants non-destructively and keep the old literal around, too?
2019-09-04 11:8:38 (GMT)
Here's another idea: could we do the replacement by the
tseitin_and_constants non-destructively and keep the old literal around, too?
not sure it's a good idea, it would add a lot more work to the congruence closure.
I think making sidekick aware of binders is the cleanest solution, but also the one that requires the most effort. Making non-closed terms opaque to the boolean theory might work well enough, though.
2019-09-04 14:1:46 (GMT)
I tried to make non-closed terms opaque to the boolean theory, but now (λx. false /\ x) doesn't simplify anymore to (λx. false), which is a problem. I will try to make non-closed terms only opaque to the part of the boolean theory that uses these tseitin constants.
2019-09-04 14:5:3 (GMT)
Yeah, sorry it's that subtle.