Schematic variables as functions in isabelle?

Question

I am working on proving a lemma in predicate logic using Isabelle, and I've encountered a schematic variable in the proof state that I'm finding somewhat confusing. I would greatly appreciate your insights.

Here's the Isabelle code for the lemma:

lemma "(∃x. ∀y. P x y) ⟹ (∀y. ∃x. P x y)"
  apply(erule exE)
  apply(rule allI)
  apply(rule exI)

After running the above code, the last proof state is:

proof (prove)
goal (1 subgoal):
 1. ⋀x y. ∀y. P x y ⟹ P (?x4 x y) y

What does conclusion P (?x4 x y) y mean exactly? What is the use of ?x4 here and is it a function of x and y. I guess here it's supposed to return x, but why is it ?x4 x y in the first place?

I tried apply assumption but it couldnt finish the proof, why?

Answer 1

Generally, a schematic variable like ?x4 means that you may instantiate this variable at a later time in the proof—but it must be done consistently over the whole proof state.

Let us look at your example, tweaked to disambiguate between left-hand and right-hand side names for clarity:

lemma ‹∃xl. ∀yl. P xl yl ⟹ ∀yr. ∃xr. P xr yr›
  apply(erule exE)
  apply(rule allI)
  apply(rule exI)
-----
Proof state:
  ⋀xl yr. ∀yl. P xl yl ⟹ P (?xr4 xl yr) yr

?xr4 indeed is a function of abstract type 'a ⇒ 'b ⇒ 'a if 'a is the type of xl/r and 'b the type of yl/r. So, (?xr4 xl yr) is a function application that means that you may use xl and yr to construct your witness in the proof of P (...) yr.

As you've pointed out, apply assumption will usually help with such instantiations. It finds a fact that can be unified to the goal by more-or-less straightforward instantiations.

In your particular proof state apply assumption fails, because the term ∀yl. P xl yl is different from P (...) yr, no matter how we fill the hole (...).

So, we first have to derive a fact that looks like the goal. For instance, we could:

  apply(drule spec)
-----
Proof state:
  ⋀xl yr. P xl (?yl6 xl yr) ⟹ P (?xr4 xl yr) yr

spec: ∀x. ?P x ⟹ ?P ?x used as a forward (or destruction) rule allows to push a universal quantification in a fact into a schematic variable (or, more commonly, to instantiate it directly). Here, it leads to a new schematic variable term (?yl6 xl yr) appearing on the left-hand side.

Now, there are clear instantiations for both: ?yl6 == λx y. y and ?xr4 == λx y. x make both terms evaluate to P xl yr. Therefore, we can close the proof here.

  by assumption