Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] What does it mean when a schematic variable is...

Email Gateway (Oct 09 2023 at 09:45):

From: Eero Pomell <eero.the.engineer@gmail.com>
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?

Email Gateway (Oct 09 2023 at 10:00):

From: Peter Lammich <lammich@in.tum.de>
Hi,

"?x4 x y" is a schematic variable that can depend on the bound variables
x and y. E.g., you can unify ?x4 with x (?x4 = %x y. x).

Without these parameters, a schematic variable cannot depend on bound
variables.

Email Gateway (Oct 09 2023 at 10:06):

From: Jan van Brügge <jan@vanbruegge.de>
Those are all the forall-bound variables that the unification of the schematic variable may use. For example if you would bring new forall-bound variables into scope you wouls not be able to unify the schematic variable with them.

Your proof does not work because you still have a HOL forall in your assumptions. If you add apply (erule allE) before apply assumption it will work.

Cheers,
Jan

Oct 9, 2023 11:45:19 AM Eero Pomell <eero.the.engineer@gmail.com>:

Email Gateway (Oct 09 2023 at 11:43):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hi,

I am not sure what is your objective in the whole exercise.
You are surely aware of a simple
lemma "(∃x. ∀y. P x y) ⟹ (∀y. ∃x. P x y)"
 by  blast

A structured proof revealing the idea behind the proof would look like

lemma "∃x. ∀y. P x y ⟹ ∀y. ∃x. P x y"
proof
  assume ex: "∃x. ∀y. P x y"
  fix y
  obtain x where "P x y"
    using ex by blast
  thus "∃x. P x y"
    by blast
qed

If you are trying to learn using tactics then the proof can be
lemma "(∃x. ∀y. P x y) ⟹ (∀y. ∃x. P x y)"
  apply(erule exE)
  apply(rule allI)
  apply(rule exI)
  apply (erule allE)
  by assumption

as Jan pointed out.

If you just want to understand the meaning of the schematic variable in
the last goal, look at a mixed:
lemma "(∃x. ∀y. P x y) ⟹ (∀y. ∃x. P x y)"
  apply(erule exE)
  apply(rule allI)
  apply(rule exI)
proof-
  show "⋀x y. ∀y. P x y ⟹ P ((λ x y. x) x y) y"
    by blast
qed

where ?x4 is instantiated with (λ x y. x) as Peter pointed out. In other
words, the schematic variable in a goal means that you will prove the
the goal if you manage to prove it for any instantiation of the
schematic variable (that is, an instantiation of your choice).
Note that Isabelle guesses two instantiations in the last "by
assumption" above.

Stepan

Last updated: Apr 28 2024 at 20:16 UTC