Email Gateway (Aug 18 2022 at 17:09): Email Gateway (Aug 18 2022 at 17:09):From: Jeremy Siek <jeremy.siek@colorado.edu>
I've noticed that on a few occasions, referencing a lemma with
a "using" followed by auto didn't work, whereas adding the
lemma to the simp set via "auto simp:" did work.
Are there some general rules of thumb regarding when to use
which?
Best regards,
Jeremy
Email Gateway (Aug 18 2022 at 17:09):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
heh, I’ve observed it the other way around and came up with this
explanation: When it is added via using, the simplifier will actually
simplify the fact and then consider it in its rules, making it more
likely to match. When adding it via "simp add:", the fact might be in a
form that never matches.
For your case, the explanation might be similar in that the fact matches
only in a non-simplified form. But I’m sure the experts can come up with
more explanations.
I cannot provide a general rule though.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 17:09):From: Makarius <makarius@sketis.net>
More precisely, Isar does nothing more than adding the facts to the
"using" slot of the proof state. It is then up to the subsequent proof
method to make sense of it. For semi-automated methods like simp, auto,
blast etc. this means to insert the facts into the goal state and proceed
as usual. This effectively means that type variables cannot be
instantiated under most circumstances.
It is one of the many pitfalls of implicit polymorphism (or the lack
thereof) in certain situations.
Makarius
Email Gateway (Aug 18 2022 at 17:11):From: Jeremy Siek <jeremy.siek@colorado.edu>
Thanks all for the explanations on this!
Last updated: Apr 20 2024 at 04:19 UTC