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
Last updated: Dec 07 2023 at 08:19 UTC