Hanno Becker (Feb 19 2023 at 19:53): Hanno Becker (Feb 19 2023 at 19:53):Hi, again! I run into a context where I've got two subgoals A ?x and B ?x ?y (shared schematic ?x!), of which A ?x can be uniquely instantiated + solved from the context, while B ?x ?y with _both_ ?x and ?y schematic, has multiple correct instantiations, all but one of which with 'wrong' x. In this context, it is therefore vital to first solve A ?x, and _then_ B x ?y. Are there some tricks one can play to ignore B ?x ?y until at least x is instantiated?
Wolfgang Jeltsch (Feb 19 2023 at 22:37):If the subgoal A ?x is first, you can apply a proof method that only tackles a single goal and instantiates schematic variables (sometimes this proof method can just be assumption). If you need to apply a proof method that tackles several goals, like auto, you can limit it to work only on the first subgoal by appending [1] to it.
Hanno Becker (Feb 21 2023 at 15:18):Thank you Wolfgang! Unfortunately, this doesn't work for me, because I'm working with largely automatic reasoning, and the difficulty is to prevent the 'driver' to look at B ?x ?y first. The issue is actually more general, and I'll re-phrase the question in those terms shortly.
Last updated: Apr 26 2024 at 08:19 UTC