Hanno Becker (May 25 2024 at 19:27): Hanno Becker (May 25 2024 at 19:27):Is there a way to make simp ignore specific premises, both for (a) use during simplification of other premises / goal, (b) simplification of the premise itself?
I considered adding a wrapper IGNORE x == x, and have a trivial cong rule IGNORE x = IGNORE x (in fact, there's already the in-built ASSUMPTION which is very similar), but that solves only (b) I think -- at any rate, the long running simp calls I'm trying to speedup this way don't get noticably any faster with this technique.
Hanno Becker (May 26 2024 at 19:40):Extending the idea above, one can introduce a wrapper around P ==> Q, say IGNORE_imp P Q == P ==> Q, and wrap to-be-ignored assumptions into that. I think that should be OK for the simplifier, but sadly not for clarsimp, which no longer recognizes introduction rules once the goal is wrapped in IGNORE_imp.
Hanno Becker (May 26 2024 at 19:41):The best seems to be a way to hook into the simplifier and add a filter deciding whether a premise enters the simplification process or not...
Last updated: Dec 21 2024 at 12:33 UTC