Marco David (Apr 21 2020 at 21:18): Marco David (Apr 21 2020 at 21:18):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?
Marco David (Apr 21 2020 at 21:35):On a related note, how can one increase "linarith_split_limit" and is this sensible if e.g. the proof would require more splitting?
Lukas Stevens (Apr 22 2020 at 09:22):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: Apr 19 2024 at 08:19 UTC