Hanno Becker (Feb 07 2023 at 09:45): Hanno Becker (Feb 07 2023 at 09:45):Hi. In some proof I'm conducting, apply (simp) simplifies the goal further than I had expected and intended. I've now prefixed the step with using [[simp_trace=true]] and am looking at the simp trace to understand which perhaps erroneously simp-declared rule is applied . However, there appears to be a 'jump' at the decisive simplification: In step N, I see rewriting {term N} == {term N+1}, and both sides are OK (= simplifications I want). But in step N+1, it says [1] SIMPLIFIER INVOKED ON THE FOLLOWING TERM: {term M}, where term M is _not_ term N+1, and instead, in between term N+1 and term M the simplification I want to avoid seems to have been applied without mentioning / indication of where that was coming from. Can someone help?
The simplification in question itself hoists out a HOL if out of a rather complex definition, which then shortly after leads to a splitting of the goal -- both is what I want to avoid since one can keep on reasoning uniformly for a while. Is there a way to prevent such hoisting of ifs?
Hanno Becker (Feb 07 2023 at 10:08):Ah... it looks like it's if_split that I didn't want, and simp split del:if_split helps.
Mathias Fleury (Feb 07 2023 at 16:49):In general, I use
supply [[simp_trace, simp_trace_depth_limit=5]]
For more desparate cases, there simp_debug
Hanno Becker (Feb 09 2023 at 05:45):Thanks @Mathias Fleury !
Last updated: Apr 25 2024 at 01:08 UTC