Email Gateway (Aug 18 2022 at 18:49): Email Gateway (Aug 18 2022 at 18:49):From: John Ridgway <john@jacelridge.com>
I'm having a problem. Given the following lemma:
lemma "
!! C tau_0 epsilon_0 rs Rs cx w tau_11 epsilon_11 tau_10 epsilon_10 y.
[| C = valconfig w (exntoprimmech cx) Rs tau_11 epsilon_11;
tau_0 = tau_10;
epsilon_0 = epsilon_10;
rs = dom Rs;
Rs : validmechanisms;
exntoprimmech cx : rs;
(w, tau_11) : mvalhastype;
exception cx tau_11 : epsilon_11;
\<forall>cx' tau_11'. exception cx' tau_11' : epsilon_11 --> cx' = cx \<and> tau_11' = tau_11;
tau_10 = tau_11;
epsilon_10 = epsilon_11;
Rs : validmechanisms;
isemptyrs (exntoprimmech cx) Rs;
tau_11 : istype;
Rs (exntoprimmech cx) = Some y |]
==> (\<exists>C' tau_1 epsilon_1.
(C, C') : onestep \<and>
(C', tau_1, epsilon_1) : configurationhastype \<and> (tau_1, tau_0) : issubtype \<and> epsilon_1 \<subseteq> epsilon_0) \<or>
(\<exists>w r Rs tau_0 epsilon_0. isemptyrs r Rs \<and> C = valconfig w r Rs tau_0 epsilon_0)"
I try apply(simp) as the first step in my proof, and Isabelle goes away for a long time. I don't know whether it ever comes back; I gave up on it before then. Removing the premise
\<forall>cx' tau_11'. exception cx' tau_11' : epsilon_11 --> cx' = cx \<and> tau_11' = tau_11;
allows the whole mess to be proved by simp. What about that premise is causing the trouble? Or is it likely an interaction with other stuff? How do I figure out which it is?
Thanks in advance for your help.
Peace
Email Gateway (Aug 18 2022 at 18:49):From: Tobias Nipkow <nipkow@in.tum.de>
This is a tricky situation. The simplifier diverges and you want to find
out why. In principle the answer is simple: switch on the simplifier
trace. In practice, this can overload the interface (Proof General and
jedit) because an infinite rewrite tends to produce an infinite trace.
You may be lucky because the infinity of the trace only manifests itself
when the trace depth is set sufficiently high (initially it is 1). Or
you may be able to abort the simp command quickly enough before the
interface freezes up.
I general it is hard to figure out why something diverges just by
looking at the initial proof state because it may involve some
unexpected interaction between the hundreds of existing rewrite rules
and the goal state. In you goal, the offending assumption will be turned
into two rewrite rules by the simplifier:
exception ?cx' ?tau_11' : epsilon_11 ==> (?cx' = cx) = True
exception ?cx' ?tau_11' : epsilon_11 ==> (?tau_11' = tau_11) = True
Not sure why that could lead to a problem.
Tobias
PS The "!! ..." prefix is not needed.
Email Gateway (Aug 18 2022 at 18:50):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Hi John,
if you find you have to invoke the simplifier trace, you may want to
try the I3P interface for the purpose:
it copes with the stream of messages with minimal processing overhead
(by lazy rendering) and always allows you to "interrupt"
the prover to examine the message already received :)
(Just revoke the command, I3P keeps sending INT to Isabelle until
it succeeds. Also, there is a "local option" that turns on
the trace for a single command; right-click to the left gutter in the
editor.)
In your example, I found that the following pattern repeats:
[1]Applying instance of rewrite rule "??.unknown":
exception ?x ?xa3 ∈ epsilon_11 ⟹ cx ≡ ?x
[1]Trying to rewrite:
exception ?x ?xa3 ∈ epsilon_11 ⟹ cx ≡ ?x
[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
exception ?x ?xa3 ∈ epsilon_11
[1]SUCCEEDED
cx ≡ cx
Hope this helps,
Holger
Email Gateway (Aug 18 2022 at 18:50):From: John Ridgway <john@jacelridge.com>
I now have a bare-bones theory which demonstrates this problem:
theory temp imports Main begin
lemma "
\<lbrakk> (x::nat,y::nat) \<in> xys;
\<forall>x' y'. (x', y') \<in> xys \<longrightarrow> x'=x \<and> y'=y;
y'' = y \<rbrakk> \<Longrightarrow>
True"
apply(simp)
done
end
Note that I'm importing from Main (HOL), so nothing I've added is causing any problems. If I can't do this, how do I say that a particular constructed value is in a set, and that any constructed value in the set is equal to this one? The y''=y premise is essential to causing the simplifier to loop (x''=x also causes a loop). I'm at a loss.
Peace
Email Gateway (Aug 18 2022 at 18:50):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Nothing in Isabelle can really be trusted to solve your problems as a
black box. In this situation you can do two things. One is to try lots
of variants, and the other is to try to understand exactly how the
system works.
The simp variants (simp(no_asm)) and (simp(no_asm_use)) can sometimes
help with these problems by rewriting your assumptions before using them
as rewrites. This won't help in this case. Many other solvers which
don't call the simplifier can solve your reduced example (metis, blast,
safe).
In summary: before thinking, always blindly type a bunch of nonsense.
This may not solve your real problem, and keeping the simplifier on your
side is usually necessary. The simplifier (in assumption-using mode, the
default) treats assumptions as rewrite rules as though they'd been
supplied with [simp]. This causes it to diverge frequently since they
may loop in various ways. In this case, it's treating your rule as a way
of rewriting any natural into x or y by showing it is a component of a
member of xys. This includes naturals that have already been rewritten
to x or y, as well as the naturals in the assumption it must prove to
use this rule (it really is that stupid). In short, you can't let this
assumption stay in this form.
You can probably finesse your way around this by using the logically
equivalent assumption
"ALL x' y'. ((x', y') : xys) = (x' = x & y' = y & xys ~= {})"
(This can be proven equal to your assumption by fast)
The simplifier is now not being given a license to rewrite any x or y,
but only terms of the form (x', y') : xys. This should hopefully be a
force for good and not evil.
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 18:50):From: John Ridgway <john@jacelridge.com>
I actually went with
(x,y) \<in> xys
and
ALL x' y'. (x' \<notequal> x \<or> y' \<notequal> y) --> ((x',y') \<notin> xys)
and that seems to work better. Thanks for your help.
Peace
Email Gateway (Aug 18 2022 at 18:50):From: Tobias Nipkow <nipkow@in.tum.de>
Tom, your analysis is not quite accurate: the rewrite rules coming out
of the hypothesis do not rewrite any natural number. The simplifier is
intelligent enough to avoid that. As I pointed out in my previous email,
it derives the rewrite rule
(?x', ?y') : xys ==> (?x'=x) = True
(?x', ?y') : xys ==> (?y'=y) = True
They are harmless. However, I failed to see that it also derives
(?x', ?y') : xys ==> x = ?x'
(?x', ?y') : xys ==> y = ?y'
Either of them causes a problem together with (x,y) : xys, because they
allow x = x = x = ... or y = y = y = ... .
Tobias
Last updated: Apr 24 2024 at 20:16 UTC