Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Potential bug regarding `OF` with match patter...

Email Gateway (Feb 11 2022 at 02:01):

From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hi!

I’d like to report a behavior of the OF attribute with match pattern
facts that seems like a bug to me.

Consider the following contrived example of a lemma:

lemma
assumes "Suc n < Suc m"
shows "n < m"
by (simp only: Suc_less_SucD [OF assms])

The proof is accepted, which is to be expected, as the fact
Suc_less_SucD [OF assms] is precisely what is to be proved.

Now let’s make this a bit more complicated, using some Eisbach:

lemma
assumes "Suc n < Suc m"
shows "n < m"
by (
match assms in assumption: _ ⇒
‹simp only: Suc_less_SucD [OF assumption]›
)

The proof in this example fails. When debugging with simp_trace, it
becomes apparent that the rewrite rule added to the simplifier is not
n < m ≡ True but Suc n < Suc m ≡ True. Apparently, the computation
of the fact Suc_less_SucD [OF assumption] goes completely wrong, and
assumption itself is returned as the result.

If simp only: Suc_less_SucD [OF assumption] is replaced by insert Suc_less_SucD [OF assumption], the proof is accepted again. So it seems
the above-mentioned behavior has to do with particularities of simp.

Interestingly, the problem goes away when outsourcing the proof method
expression to a custom method. The following code works as it should:

method nat_less_solver uses Suc_less_Suc = (
match Suc_less_Suc in assumption: _ ⇒
‹simp only: Suc_less_SucD [OF assumption]›
)

lemma
assumes "Suc n < Suc m"
shows "n < m"
by (nat_less_solver Suc_less_Suc: assms)

All the best,
Wolfgang

Email Gateway (Feb 11 2022 at 10:44):

From: Peter Lammich <lammich@in.tum.de>
This behaviour is, indeed, weird.

This works:

apply (
match assms in assumptionX: _ ⇒
‹rule Suc_less_SucD[OF assumptionX]›
)

with simp only:, it doesn't. Further investigation reveals, that the
OF-attribute is, actually, never applied (where things get really
weird):

attribute_setup myOF = ‹Attrib.thms >> (fn Bs => Thm.rule_attribute Bs
(fn _ => fn A => A OF (@{print} Bs)))›

apply ( match assms in assumptionX: _ ⇒ ‹rule Suc_less_SucD[myOF
assumptionX]› )

Proves the goal, and prints ["Suc n < Suc m"]⌂

apply ( match assms in assumptionX: _ ⇒ ‹simp only: Suc_less_SucD[myOF
assumptionX]› )

Fails, no printout ...

This hints at the Method.section concept. With
setup ‹Config.put_global Method.old_section_parser false›

we get a printout, but the fact is still not added to the simplifier,
nor is the OF attribute interpreted correctly (it's still Suc _ < Suc _ after the OF ...) At this point, I'm giving up, and hope someone who
knows more about why section-parser has been updated, and the subtle
interactions with Eisbach, can take over

Email Gateway (Feb 11 2022 at 10:50):

From: Peter Lammich <lammich@in.tum.de>
Addendum: the behaviour I reported below was with the import order
imports "HOL-Eisbach.Eisbach" Main

When I change to
imports Main "HOL-Eisbach.Eisbach"

then the following will prove the goal:

theory Scratch
imports Main "HOL-Eisbach.Eisbach"
begin

setup ‹Config.put_global Method.old_section_parser true›

lemma
assumes "Suc n < Suc m"
shows "n < m"
by ( match assms in assumptionX: _ ⇒ ‹simp only: Suc_less_SucD[OF
assumptionX]› )

Last updated: Jul 15 2022 at 23:21 UTC