Hi everyone, I'm trying to tame quite a large conjuction of algebraic equations over nats and ints. In one of my proofs, applying simp or auto does an unwanted substitution in my goal. Is there a way to tell simp to simplify only my assumptions and leave the goal as is?

On a related note, how can one increase "linarith_split_limit" and is this sensible if e.g. the proof would require more splitting?

If your assumption are named, you can tag them with the attribute simplified. To only rewrite parts of the goal, you can use the tactic `rewrite`

from HOL-Library. Unfortunately, this tactic does not use the simplifier but only uses the given rules. It would be conceivable to extend `rewrite`

to use the simplifier, though. Another trick is to state the assumptions as a logical conjunction, say `A`

, and write down `A = xxx`

where xxx does appear nowhere in the context and then apply `auto`

to see what auto rewrites `A`

to.

Last updated: Dec 07 2023 at 08:19 UTC