Stream: Beginner Questions

Topic: `simp add` fails while `simp only` succeeds -- how?

Hanno Becker (Jan 06 2023 at 21:24):

Hi! I've bumped into a situation where apply(simp add: foo_thms) fails while apply(simp only:foo_thms) succeeds, with foo_thms a list of theorems. How is that possible? My impression was that simp succeeds if and only if at least one simplification was successfully applied.

Manuel Eberl (Jan 06 2023 at 22:15):

That does sound odd. Hard to pinpoint what's going on there without being able to reproduce the exact situation, maybe run the simp trace.

Wolfgang Jeltsch (Jan 07 2023 at 00:21):

@Hanno Becker, by “fails”, do you mean the proof method really fails, in the sense that it can’t perform any rewrites and an error is reported, or do you mean that it just can’t solve the goal completely, while the version with only: can. If you meant the latter, there would be a simple explanation: the rules from the simpset, which are additionally considered when not using only:, cause some rewrite that destroys a subterm that could be rewritten using foo_thms.

Hanno Becker (Jan 07 2023 at 07:58):

@Wolfgang Jeltsch The method _fails_, which I interpret as no suitable rewrite being found, which is quite odd given that simp has more rules at its disposal in the simp add: ... variant than the simp only: ... variant. Or is there some kind of threshold being applied to the number of rules that simp will consider?

Hanno Becker (Jan 07 2023 at 07:59):

@Manuel Eberl How do I get the simp trace?

Wolfgang Jeltsch (Jan 07 2023 at 16:30):

Wolfgang Jeltsch The method fails, which I interpret as no suitable rewrite being found, which is quite odd given that simp has more rules at its disposal in the simp add: ... variant than the simp only: ... variant.

A real failure of the add: variant is odd indeed.

Or is there some kind of threshold being applied to the number of rules that simp will consider?

Not to my knowledge, at least.

Wolfgang Jeltsch (Jan 07 2023 at 16:33):

How do I get the simp trace?

You can globally enable simp traces by putting declare [[simp_trace]] into your code and locally by putting using [[simp_trace]] before your apply or by that invokes simp.

Hanno Becker (Jan 07 2023 at 19:06):

Thank you @Wolfgang Jeltsch , I will give that a go and see if it sheds any light on what's going on.

Last updated: Apr 20 2024 at 04:19 UTC