Exists irrational number: sqrt fails to refine pending goal

Question

In Isabelle, why does this

theory Example
  imports "HOL-Examples.Sqrt"
begin

theorem exists_irrational_number: "∃x. x ∉ ℚ"
proof (rule exI)
  show "sqrt 2 ∉ ℚ" using sqrt_2_not_rat by simp
qed

end

have the proof state

goal (1 subgoal):
 1. ?x ∉ ℚ

but give the error

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  sqrt 2 ∉ ℚ

I think it has something to do with the sqrt...

Answer 1

Unfortunately, the listing is no minimal reproducible example. I assume that the theory Sqrt contains something like the lemma from https://lawrencecpaulson.github.io/2022/05/04/baby-examples.html.

The problem you're running into becomes visible if you make Isabelle print types:

declare [[show_types]]

theorem exists_irrational_number: "∃x. x ∉ ℚ"
proof (rule exI)
  show "sqrt 2 ∉ ℚ" using sqrt_2_not_rat by simp

Let's reexamine the error output now:

(?x::'a) ∉ ℚ
variables:
?x :: 'a 
Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
sqrt (2::real) ∉ ℚ

That is, Isabelle cannot infer that your lemma is meant to talk about reals. (This is due to the genericity of the definition of ℚ.) On the other hand, your witness statement is type-inferred to talk about reals because this is where sqrt is a function. But a statement that talks about reals does not refine the proof goal in its stated genericity.

The straight-forward way of fixing this is through a more specific statement of the theorem, giving type real to x:

theorem exists_irrational_number: "∃x::real. x ∉ ℚ"

Now, the proof goes through.

If you think about it, this all makes perfect sense. Another valid typing of the term would read:

"∃x::rat. x ∉ ℚ"

And this claim, obviously, would be a false one (because "∀x::rat. x ∈ ℚ" unfolding Rats_def by simp). Therefore, the intended lemma only is true with the right types.