My questions here are a spin-off of what was a tangent in my previous question.
For these questions, I use a very simple lemma, though my second question is fairly involved.
The error "Local statement fails to refine any pending goal" is one of the more frustrating errors, when using show or thus and when all my logic appears correct, so I'm trying to better understand the error message that occurs below at lemma fix_2.
I know the fix for it, which is my lemma fix_1, but the more I know, the better I might be at dealing with another "fails to refine any pending goal".
Anyone interested might be able to answer Q1 and Q2 just by reading the questions, and then looking at the two lemmas.
There's a lot of information I put in below. I format the comments below like I do to be able to compare how this and goal change after commands. Doing that, I'm able to get a better understanding of what's happening with the use of let, def, and fix/assume, where the main purpose is to try and understanding the error at the show command of lemma fix_2.
I don't know how to make a question like this simple.
Questions
Here, I put forth two questions. You will need to skip down to look at lemma let_1 and lemma fix_2. I tried to use HTML anchors to create links within this page, but it didn't work.
Q1: Below, at
lemma let_1, I useprint_commands. I looked through those commands to try to find commands that will give me information about how schematic variables are instantiated. I foundprint_binds, which shows my use of schematic variable?w. Are there any other commands that will give me information about what's happening with schematic variables in a proof?Q2: Am I right in saying the following?
- At the use of the
show "card {} = 0"inlemma fix_2, thethisfact and its implicit hypothesis,card w = 0 [w == {}], are used to create a rule similar to what is exported after the{...}block inlemma fix_1, where the exported rule there is(?w2 == {}) ==> card ?w2 = 0. - The created rule is then used to do some kind of unification with the proof goal in
show "card {} = 0", in which the schematic variable is instantiated with{}, but something doesn't match up, and an error occurs.
- At the use of the
The behavior of def and fix/assume described
The primary context of this question is this statement by L.Noschinski on the IsaUserList:
When you use "fix" or "def" to define a variable, they either get just generalized (i.e. turned into schematics) (fix) or replaced by their right hand side (definitions) when a block is closed / a show is performed.
I partially restate it to show how I understand it for the show command, where what I say is also based on how def_1 and fix_1 behave below, which both use a {...} block:
If the statements def x == "P" and fix y assume "y == P" are used before a show command, as in def_2 and fix_2 below, at the use of the show command, the following will happen:
- For
def x, any use ofxin thethisfact will be replaced byP. - For
fix y, a rule will be created using both thethisfact and its implicit hypothesis, such as after the{...}infix_1below. In this rule,ywill be replaced by a schematic variable.
Five lemmas for studying this, goal, have and show
declares
I use show_question_marks because I need to see when schematic variables are introduced when fix/assume is used.
The use of show_hyps shows the implicit hypothesis for a proof fact, in square brackets. These implicit conditions get used in an exported rule when fix/assume is used.
declare[[show_question_marks=true, show_hyps=true]]
declare[[show_sorts=false, show_types=false, show_brackets=false]]
One basic lemma, and 5 variations which have a proof fact not used
The basic lemma shows what's actually being proved. I then have the following:
let_1to look at how the use ofletaffectsthis.def_1, which usesdefand a{...}block, to see howdefbehaves and howthisis exported.def_2, which has no{...}block, to be able to look atthisbeforeshowis used.fix_1andfix_2, which are likewise todef_1anddef_2, but usefix/assume.
lemma with no proof fact
All of the lemmas below are the next lemma, and are proved the same. What the others have in addition is one proof fact which is not needed, and not used by the show command.
The purpose of the proof fact is to help me see how def and fix change the this fact when have is proved, and see how they export this after a block {...} is closed.
lemma "card {} = (0::nat)"
proof-
show "card {} = 0"
by(simp)
qed
let_1
lemma let_1: "card {} = (0::nat)"
proof-
let ?w = "{}::'a set" (*No `this` fact: ?w is instantiated as {}.*)
print_commands
print_binds (*term bindings: w? == bot *)
have "card ?w = (0::nat)" (*goal: card {} = 0 *)
by(simp) (*this: card {} = 0 *)
show "card {} = 0" (*goal: card {} = 0 *)
by(simp)
qed
def_1, {...}
lemma def_1: "card {} = (0::nat)"
proof-
{def w == "{}::'a set" (*this: w == {} [w == {}] [name "local.w_def"] *)
from this
have "card w = (0::nat)" (*goal: card w = 0 *)
by(simp) (*this: card w = 0 [w == {}] *)
} (*this: card {} = 0 *)
show "card {} = 0" (*goal: card {} = 0 *)
by(simp)
qed
def_2, no block
lemma def_2: "card {} = (0::nat)"
proof-
def w == "{}::'a set" (*this: w == {} [w == {}] [name "local.w_def"] *)
from this
have "card w = (0::nat)" (*goal: card w = 0 *)
by(simp) (*this: card w = 0 [w == {}] *)
show "card {} = 0" (*goal: card {} = 0 *)
by(simp)
qed
fix_1, {...}
lemma fix_1: "card {} = (0::nat)"
proof-
{fix w assume "w == {}::'a set" (*this: w == {} [w == {}] *)
from this
have "card w = (0::nat)" (*goal: card w = 0 *)
by(simp) (*this: card w = 0 [w == {}] *)
} (*this: (?w2 == {}) ==> card ?w2 = 0 *)
show "card {} = 0" (*goal: card {} = 0 *)
by(simp)
qed
fix_2, no block
lemma fix_2: "card {} = (0::nat)"
proof-
fix w assume "w == {}::'a set"(*this: w == {} [w == {}] *)
from this
have "card w = (0::nat)" (*goal: card w = 0 *)
by(simp) (*this: card w = 0 [w == {}] *)
show "card {} = 0" (*Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(?w3 == {}) ==> card {} = 0 *)
oops
Filling in details for L.Paulson's answer, per my understanding
140119:
The answer to Q2 and why the error occurs in fix_2 is given by L.Paulson when he says,
In the proof of
fix_2, you have "fix w". This extends the context withw. The context no longer matches the original context of the goal...
After having done a search on "local context" in isar-ref.pdf, I do the gofer work to fill in some details, as I understand them.
The explicit answer to my Q2 is, no, I'm not right, where I'll quote from isar-ref.pdf to explain why the formula (?w3 == {}) ==> card {} = 0 is in the error message.
Another short answer from isar-ref.pdf is that presume in place of assume will "weaken the local context" and get rid of the error, because, apparently, the context is no longer extended by w, as described by L.Paulson.
Why the complexity of my example fix_2
My setup for this question was academic, as if a professor said, "In fix_2, modify the lemma in a minimal way to get rid of the error, while still using fix. In particular, do not use def, obtain, or let to eliminate the error. My use of {...}, as in fix_1, was an acceptable solution, but I wanted to go further and understand what produces the formula in the error message of fix_2, to help me in the future.
My use of fix/assume in fix_2 is specific to the previous question I link to at the top. Here, I introduced a proof fact to ensure an error, like I get there, but here, I don't use the proof fact, to simplify things, so I don't have to use from this or thus, but only have to use show.
In my answer to my previous question, for the lemma at hand, I couldn't see why def produced no error when fix/assume did. The info in the output panel is almost identical there for def and fix/assume, and isar-ref.pdf describes def as an abbreviation for fix/assume, page 117, where the key word is "basically":
Basically,
def x == tabbreviatesfix x "assume x == t"...
Local context, it' like, not unimportant, which is to say huge
There was this foggy notion in my mind that somewhere in the answer was the issue of local context, because I've seen the word "context" a lot in the docs. Knowing that is why I threw in the use of {...} to fix the problem once I read L.Noschinski's tip, and why I searched on "local context" after L.Paulson's answer.
Why (?w3 == {}) ==> card {} = 0 is in the error message, I think
The explanation is on page 34 of isar-ref.pdf in 2.2.2 Structured statements:
A simple statement consists of named propositions. The full form admits local context elements followed by the actual conclusions, such as
fixes x assumes "A x" shows "B x". The final result emerges as a Pure rule after discharging the context:!!x. A x ==> B x.
I'm assuming here that fixe/assume in a proof works similar to a fixes/assumes in a lemma statement.
My first guess, rather than my Q2, was on track. By L.Noschinski, I knew that w in assume "w == {}" gets changed to a schematic variable when show is invoked, so the left-hand side of the error formula, (?w3 == {}) ==> card {} = 0, matches up with with the formula of assume "w == {}", and the right-hand side matches up with the formula of show "card {} = 0".
I changed my guess on a bicycle ride, that a rule like fix_1's exported this was created, (?w2 == {}) ==> card ?w2 = 0, and that ?w2 was instantiated with {}. That didn't match very well with (?w3 == {}) ==> card {} = 0, but it was all a guess anyway.
Two more quotes about local context
Because of my use of fix/assume, this next quote put me on the right track, after given the answer by L.Paulson that my fix/assume extends the context.
pg.32 in 2.2 The Isar proof language:
The remaining elements
fixandassumebuild up a local context (see §2.2.1), whileshowrefines a pending sub-goal by the rule resulting from a nested sub-proof (see §2.2.3).
My pursuit here has largely been about trying to see what's happening under the hood when show is used. I'm still pursuing commands to give me some feedback about show that's not normally shown in the output panel:
pg.117 in 6.2.4 Goals:
show a: alphais likehave a: alphaplus a second stage to refine some pending sub-goal for each one of the finished result...
Using presume in place of assume
Finally, I show another solution to my academic exercise. What I quote below wouldn't have had any meaning to me without L.Paulson's answer that in fix_2, I'm extending the context.
pg.120 in 6.3.2 Initial and terminal proof steps:
Debugging such a situation might involve temporarily changing
showintohave, or weakening the local context by replacing occurrences ofassumebypresume.
lemma fix_3: "card {} = (0::nat)"
proof-
fix w presume "w == {}::'a set"(*this: w == {} [w == {}] *)
from this
have "card w = (0::nat)" (*goal: card w = 0 *)
by(simp) (*this: card w = 0 [w == {}] *)
show "card {} = 0" (*goal: card {} = 0 *)
print_binds (*term bindings:
?this == card w = 0
... == 0
?thesis == card bot = 0 *)
by(simp)
