Email Gateway (Aug 22 2022 at 10:33): Email Gateway (Aug 22 2022 at 10:33):From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,
today I stumbled upon some behaviour of simp I don't understand.
Consider the following simple theory
theory Scratch imports Main begin
consts P :: "bool"
consts f :: "'a ⇒ 'a"
notepad begin
fix a b :: 'a
assume X: "⋀x :: 'a. f x ≠ a ⟹ f x = x"
have "f b ≠ a ⟹ f b = b"
apply (simp add: X)
apply (subst X) apply simp_all
done
sorry
end
Here, "simp add: X" fails, even though all its premises can be solved by
"assumption" -- or, as the second line shows, by "simp". Has anyone got
an idea why this is the case?
Looking at the the simp trace, one seees that the simplifier tries
recursively to rewrite the premis "f x ~= a". This fails ultimately. But
I would have expected it trying to solve the premis by assumption, then.
-- Lars 'simp is not simple' Noschinski
Email Gateway (Aug 22 2022 at 10:33):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Lars,
The rule “X” appears to violate the golden rule of thumb when using “simp”, i.e. that both the rhs and the preconditions should be simpler than the lhs (see Section 2.5.3 of Concrete Semantics). Surely, “f x ~= a” is not simpler than “f x”. That bad things happen then doesn’t surprise me so much…
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 10:33):From: Lars Noschinski <noschinl@in.tum.de>
It is only simpler insofar as that it is literally part of the
assumptions. I would not have been surprised if the simplifier had
started looping -- after all, it is not really simpler. But refusal to
rewrite does not yet fit into my mental model of the simplifier.
Email Gateway (Aug 22 2022 at 10:33):From: Tobias Nipkow <nipkow@in.tum.de>
You are both right. The "X" violates the golden rule, and the violation is so
blatant that the simplifier ignores that rule altogether. It would take a bit of
work to emit a warning.
Tobias
smime.p7s
Last updated: Apr 26 2024 at 01:06 UTC