Hanno Becker (Feb 17 2023 at 06:49): Hanno Becker (Feb 17 2023 at 06:49):Hi! Is there support for recognising and reconciling similar subgoals? I'm doing a large proof where it seems difficult to avoid a temporary case split, but where, ultimately, I end up with subgoals of a shape close to A0 => A1 => ... => An => X_i => GOAL, which I would like to 'fold' into a single goal A0 => A1 => ... => An => (X0 \/ X1 \/ ... ) => GOAL since the subsequent reasoning will be the same for all of them. The proof is largely automatic and the exact shape of assumptions and goals somewhat fluent, so it's difficult to state the desired A0 => A1 => ... => An => (X0 \/ X1 \/ ... ) => GOAL upfront.
Last updated: Apr 20 2024 at 08:16 UTC