Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unfolding not performed

Email Gateway (Aug 22 2022 at 20:22):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!

I’m experiencing a situation where the simplifier doesn’t solve an
apparently trivial goal. I was able to narrow the problem down to an
issue with unfolding, which is exemplified by the following code:

lemma rewrite_rule:
shows "((a ⟷ b) ∧ (a ⟶ c)) = ((a ⟷ b) ∧ (b ⟶ c))"
by blast

lemma
shows "((a ⟷ b) ∧ (a ⟶ c)) = ((a ⟷ b) ∧ (b ⟶ c))"
unfolding rewrite_rule
oops

I would expect unfolding rewrite_rule to change the goal to
((a ⟷ b) ∧ (b ⟶ c)) = ((a ⟷ b) ∧ (b ⟶ c)). However, it doesn’t change
the goal at all. Why is that?

I’m using Isabelle2018.

All the best,
Wolfgang

Email Gateway (Aug 22 2022 at 20:22):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
I added using [[simp_trace]] and found out that Isabelle thinks the
rule ?a = ?b ∧ (?a ⟶ ?c) ≡ ?a = ?b ∧ (?b ⟶ ?c) is permutative (and
doesn’t apply it, because it wouldn’t make the term smaller). However,
I’d say that this rule is clearly not permutative.

All the best,
Wolfgang

Email Gateway (Aug 22 2022 at 20:22):

From: Tobias Nipkow <nipkow@in.tum.de>
Hi Wolfgang,

The test is indeed only approximate, it just checks if the two terms have the
same skeleton. Maybe for misguided efficiency reasons? I cannot remember. It is
one of those things that if we changed it now, it would probably break too many
existig proofs.

Best
Tobias
smime.p7s

Email Gateway (Aug 22 2022 at 20:22):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m wondering whether

simp cong: conj_cong

might solve your original problem. This will simplify e.g. x=t & P x to x=t & P t.

Larry Paulson

Email Gateway (Aug 22 2022 at 20:22):

From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Wolfgang Jeltsch

On the practical side, you can also use a lower level rewrite method for similar problems - something that I adopted from the existing implementation of the command unoverload_definition in Types-To-Sets [1]:

ML ‹

fun pure_unfold ctxt thms =
(
ctxt
|>
(
thms
|> map (Local_Defs.meta_rewrite_rule ctxt)
|> Conv.rewrs_conv
|> Conv.try_conv
|> K
|> Conv.top_conv
)
);

val unfold_tac' = CONVERSION oo pure_unfold;
fun unfold_meth' ths ctxt = SIMPLE_METHOD' (unfold_tac' ctxt ths);

Theory.setup (
Method.setup \<^binding>‹unfold'› (Attrib.thms >> unfold_meth')
"primitive unfold definitions"
);

›

lemma rewrite_rule:
shows "((a ⟷ b) ∧ (a ⟶ c)) = ((a ⟷ b) ∧ (b ⟶ c))"
by auto

lemma "((a ⟷ b) ∧ (a ⟶ c)) = ((a ⟷ b) ∧ (b ⟶ c))"
apply (unfold' rewrite_rule)
apply (rule HOL.refl)
done

[1] F. Immler, “Automation for unverloading definitions,” Jan. 2019. [Online]. Available: http://isabelle.in.tum.de/repos/isabelle/rev/ab5a8a2519b0

Thank you

Hi!

I’m experiencing a situation where the simplifier doesn’t solve an
apparently trivial goal. I was able to narrow the problem down to an
issue with unfolding, which is exemplified by the following code:

lemma rewrite_rule:
shows "((a ⟷ b) ∧ (a ⟶ c)) = ((a ⟷ b) ∧ (b ⟶ c))"
by blast

lemma
shows "((a ⟷ b) ∧ (a ⟶ c)) = ((a ⟷ b) ∧ (b ⟶ c))"
unfolding rewrite_rule
oops

I would expect unfolding rewrite_rule to change the goal to
((a ⟷ b) ∧ (b ⟶ c)) = ((a ⟷ b) ∧ (b ⟶ c)). However, it doesn’t change
the goal at all. Why is that?

I’m using Isabelle2018.

All the best,
Wolfgang

Email Gateway (Aug 22 2022 at 20:23):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hello!

Yes, this indeed solves this goal. That said, the code I sent in my
initial e-mail was only a minimal example to expose the problem. The
actual code is about process calculi, where the solution with the
congruence rule is not applicable.

All the best,
Wolfgang

Email Gateway (Aug 22 2022 at 20:23):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!

Thanks for the code.

That said, in my actual formalization, I’m using a custom proof method
that uses rewriting only internally. This proof method is supposed to
solve goals automatically and therefore has to invoke simp, so that
multiple rewrite steps with automatically picked rules are possible. A
more manual method, like your unfold' is unfortunately not usable
there.

All the best,
Wolfgang

Email Gateway (Aug 22 2022 at 20:23):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi, Tobias!

Thanks a lot for this explanation. I’ll see that I’ll somehow work
around this issue.

Could perhaps the reference manual be changed to reflect the definition
of permutative rule that the implementation uses?

All the best,
Wolfgang

Last updated: Nov 21 2024 at 12:39 UTC