Hanno Becker (Feb 21 2023 at 15:25): Hanno Becker (Feb 21 2023 at 15:25):Hi! This is a follow-up and hopefully clarifying generalization of the "Ignoring subgoals with too many schematics" question.
In the context of largely automated reasoning, what is the 'idiomatic' way to deal with introduction rules introducing a schematic variable with multiple constraints, _some_ of which are simple (something like a bound) but some of which are truly constraining?
When applying such a rule, one is left with one subgoal per constraint. If, by bad luck, one happens to look at one of the trivial goals first, tactics are likely going to instantiate the schematic incorrectly.
How could one force Isabelle to solve the 'hard' subgoals first?
Lukas Stevens (Feb 21 2023 at 15:35):I normally just try to avoid such situations by instantiating the theorems.
Lukas Stevens (Feb 21 2023 at 15:37):What you would need, more generally speaking, is a way to annotate theorems in order to guide auto towards the right subgoal to solve first. But that is not possible at the moment.
Hanno Becker (Feb 23 2023 at 13:13):Ok. Thank you for your reply Lukas!
Last updated: Apr 26 2024 at 08:19 UTC