Email Gateway (Aug 22 2022 at 14:55): Email Gateway (Aug 22 2022 at 14:55):From: Lars Hupel <hupel@in.tum.de>
Dear list,
the following problem came up in a question on Stack Overflow:
If you load the attached theory and replace the 'oops' with 'by simp',
you'll get loads of tracing from linarith, but the proof doesn't seem to
go through, even if you continue with tracing after execution gets
suspended.
Cheers
Lars
Scratch.thy
Email Gateway (Aug 22 2022 at 14:55):From: Manuel Eberl <eberlm@in.tum.de>
To clarify the issue a bit more: Lars expected that the simplifier
should not run into problems with normalize.simps because the recursive
call is inside an if, and the default cong rule for If (if_cong_weak)
should prevent infinite application of normalize.simps.
I managed to reduce the problematic example a bit more:
fun normalize :: "nat ⇒ nat" where
"normalize x = (if x ≥ 100 then normalize (x div 2) else x)"
lemma if_cong' [cong]: "(if b then x else y) = (if b then x else y)" by simp
declare [[simp_trace]]
declare [[simp_trace_depth_limit = 1000]]
lemma "100 - normalize x = undefined"
apply (subst normalize.simps)
apply simp
I think the problem here is that the simplifier does not rewrite under
the "If", but the splitter performs case distinctions and then the "If"
gets rewritten away and one can again apply normalize.simps, closing the
circle, and then everything loops.
The question is now whether this is intended behaviour or not and
whether this is a known issue.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 14:55):From: Tobias Nipkow <nipkow@in.tum.de>
This is a known issue. In the outdated LNCS 2283 you can find a discussion what
to do about it in Section 3.5.3 Simplification and Recursive Functions. The
gist: don't use "if", use pattern matching or "case". Or disable if_split.
Tobias
smime.p7s
Last updated: Apr 19 2024 at 12:27 UTC