Email Gateway (Aug 19 2022 at 13:51): Email Gateway (Aug 19 2022 at 13:51):From: Julian Brunner <julianbrunner@gmail.com>
Hello everyone,
I've recently run into a situation where the unfolding command doesn't
terminate when used with statements containing local definitions.
Consider the following example:
locale foo =
fixes a :: "nat option"
assumes not_None: "a ~= None"
begin
definition "b == the a"
lemma a_Some: "a = Some b"
unfolding b_def
using not_None
by auto
lemma these_a: "Option.these {a} = {b}"
unfolding a_Some
by simp
end
Here, the unfolding command in the proof of 'these_a' doesn't
terminate. I've figured out that the reason for this is that when
defining 'b', what actually happens is that 'foo.b' of type 'nat
option => nat' is defined globally, with 'b' being a local
abbreviation for 'foo.b a'. This, of course, means that 'a_Some'
actually says 'a = Some (foo.b a)', so unfolding that of course
doesn't terminate.
I've been struggling to find a workaround for this. In my actual
theory (this is just a toy example), being able to unfold a statement
similar to 'a_Some' (or, adding it to the simplifier, for that matter)
would be hugely beneficial, since it is much easier to work with than
the assumption from which it was derived. I've tried using the defines
element and additional fixed variables when declaring the locale to
introduce an actual constant for 'b'. While this has worked fine
within the context of the locale, it makes global statements about the
locale more complex, which is unfortunate, considering the intent of
simplifying proofs inside the locale.
Does anyone know of a good way to deal with a situation like this?
Thanks in advance,
Julian
Email Gateway (Aug 19 2022 at 13:57):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Julian,
You can use congruence rules for the foundational constant to stop the simplifier from
working on the locale parameters. It does not work with unfolding, because unfold ignoes
congruence rules. Here's your example:
locale foo =
fixes a :: "nat option"
assumes not_None: "a ~= None"
begindefinition "b == the a"
lemma a_Some: "a = Some b"
unfolding b_def
using not_None
by autoend
lemma foo_b_cong [cong]: "foo.b a == foo.b a" by(rule reflexive)
-- "You have to supply as many parameters to foo.b as there are locale parameters on which
b depends."
context foo begin
lemma these_a: "Option.these {a} = {b}"
by(simp add: a_Some)
end
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 14:00):From: Julian Brunner <julianbrunner@gmail.com>
While unfolding would have been nicer, it's a start and it seems like
unfolding can be emulated using something like 'apply (simp only:
a_Some cong: foo_b_cong)'. Thank you!
Email Gateway (Aug 19 2022 at 14:00):From: Gottfried Barrow <igbi@gmx.com>
No response is necessary. I put this in only because I wanted to say a
few days back that I've learned that there's no guarantee that simp
can be controlled with only, which, consequently, destroys its use as
a means to make known that you're making a proof step explicit, such as
with your example above.
To a certain extent, simp behaves like auto. It can call other
automatic proof methods on its own. I decided it is what it is, and
there must be good reason for it to not shut down calling particular
proof methods when only is used. This next example shows that you
cannot completely control simp with only:
lemma "2 + 2 = (4::nat)"
using[[simp_trace, simp_trace_depth_limit=100, linarith_trace,
rule_trace]]
apply(simp only:)
done
It's calling some form of the linear arithmetic proof method. But this
is explained in the Isar Reference manual, page 188, "...but also
non-trivial tools like linear arithmetic in HOL. The latter may lead to
some surprise of the meaning of 'only' in Isabelle/HOL compared to English!"
Monolingual English speakers can only speculate whether surprises would
result in the context of "nur, lediglich, erst, einzig, bloß, und allein."
Regards,
GB
Last updated: Apr 25 2024 at 16:19 UTC