terru (Jan 21 2026 at 14:17): terru (Jan 21 2026 at 14:17):A student asked me why proofs of this form (never mind the abstract P, they had a concrete predicate in its place) are rejected:
lemma "∃x. P x"
proof
obtain x where "P x" sorry
then show "P x" by auto
qed
(the show here gives Result contains obtained parameters: x)
And I had to admit that I have no idea why (I habitually start such proofs with proof -, in which case the goal does not contain the local x, and of course the result ∃x. P x is perfectly provable from having obtained a concrete witness x) — i can see that in general, obtained variables should not occur in result statements, but here that restriction seems overzealous. Or could it be dangerous to permit this, and if so, how and when?
Jonathan Julian Huerta y Munive (Jan 21 2026 at 16:40):An informal answer would be the one below (a more detailed answer might be more nuanced). The following three starts of the proof produce the same proof obligation:
lemma "∃x. P x"
apply standard
oops
lemma "∃x. P x"
apply (rule exI)
oops
lemma "∃x. P x"
proof
oops
That is, when one writes proof without the -, there is an automatic attempt to apply an Isabelle rule/theorem. In the case of an existential quantifier, applying proof will automatically try to apply the fact exI (i.e. ?P ?x ⟹ ∃x. ?P x), which says that to show an existential statement, one must provide a witness. However, after apply (rule exI), your witness has already been chosen for you but it doesn't have a proper name (its provisional name is ?x). You can see this yourself by checking the state after providing a witness as below and checking the state after deleting the square brackets and their content:
lemma "∃x. P x"
apply (rule exI[where x=c])
oops
In other words, doing apply (rule exI[where x=c]) is telling Isabelle: "the term c is the witness for my existential statement". Similarly, apply (rule exI) is telling Isabelle: "the term ?x is the witness for my existential statement". The problem then is that if you obtain a term x, this obtained one is not necessarily the same as the one introduced by a naive application of exI (i.e. ?x). If we allow the suggested proof-structure, we would implicitly be saying that x = ?x which is not true in all types. The correct conclusion for the proof-structure then should be show "P ?x" but in your local context the variable ?x does not formally have an assigned value inside the type (thus the error Unbound schematic variable: ?x).
Fabian Huch (Jan 21 2026 at 18:18):This has nothing to do with exI or naming (?x is a regular schematic variable, there is no 'provisional name'), but is a consequence of how natural deduction works (which Isar implements) -- have a look at the ∃E rule:
image.png
y cannot appear free in B.
Fabian Huch (Jan 21 2026 at 18:22):(here's a simple example without exI:
lemma refl2: "x = x ⟹ True"
by simp
lemma True
proof (rule refl2)
obtain x where "P x" sorry
then show "x=x" by simp
qed
returns Result contains obtained parameters: x
Local statement fails to refine any pending goal)
Kevin Kappelmann (Jan 21 2026 at 22:34):terru said:
Or could it be dangerous to permit this, and if so, how and when?
It would be unsound. Consider this:
lemma good: "∀(x :: bool). ∃y. x = y"
apply (rule allI)
apply (rule exI) (*note: ?y may depend on x*)
apply (rule refl)
done
lemma bad: "∃(x :: bool). ∀y. x = y"
apply (rule exI)
apply (rule allI) (*note: ?x may not depend on y*)
apply (rule refl)
oops
lemma bad: "∃(x :: bool). ∀y. x = y"
proof (rule exI, rule allI)
fix y :: bool
obtain z where "z = y" by auto
then show "z = y" by auto (*note: ?x may not depend on new skolem variable z*)
qed
well, yes, this all makes sense to me. But I'm still struggling with the idea that the non-proof I gave should mean something fundamentally different, from, say:
lemma "∃x. P x"
proof -
obtain x where "P x" sorry
show "∃x. P x"
apply (rule exI)
using ‹P x› .
qed
Since I thought that an initial proof method should (modulo changes to the context, but that seems (?) unimportant here as the obtain only needs P, which is the same in both) do the same as applying it as the first step to ?thesis & then supplying intermediate facts (assuming they still make sense). So either more is going on in the context than I was aware of, or my understanding of initial proof methods is wrong?
Fabian Huch (Jan 22 2026 at 09:54):Now you only use the obtained variable within the subproof of B in the ND rule
Fabian Huch (Jan 22 2026 at 09:55):Here's an even simpler falsity without any existental introduction:
have "(⋀y. x = y) ⟹ False" for x :: bool by auto
then have False
proof
fix y::bool obtain x where "x=y" by blast
then show "x=y" sorry
qed
Last updated: Feb 06 2026 at 20:37 UTC