Trying to understand fix/assume/show "Failure to refine goal"; Cmd to show proof info for schematic vars

Question

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 use print_commands. I looked through those commands to try to find commands that will give me information about how schematic variables are instantiated. I found print_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" in lemma fix_2, the this fact and its implicit hypothesis, card w = 0 [w == {}], are used to create a rule similar to what is exported after the {...} block in lemma 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.

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 of x in the this fact will be replaced by P.
• For fix y, a rule will be created using both the this fact and its implicit hypothesis, such as after the {...} in fix_1 below. In this rule, y will 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_1 to look at how the use of let affects this.
• def_1, which uses def and a {...} block, to see how def behaves and how this is exported.
• def_2, which has no {...} block, to be able to look at this before show is used.
• fix_1 and fix_2, which are likewise to def_1 and def_2, but use fix/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 with w. 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 == t abbreviates fix 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 fix and assume build up a local context (see §2.2.1), while show refines 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: alpha is like have a: alpha plus 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 show into have, or weakening the local context by replacing occurrences of assume by presume.

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)

Answer 1

You are making something that should be simple very complicated.

In the proof of fix_2, you have fix w. This extends the context with w. The context no longer matches the original context of the goal, hence show card {} = 0 yields the error message you mention.

Probably the lemma you really need in this proof is !!w. card w = 0. When proving this lemma, you will insert fix w in a local block, and it will all work.