CODEWITHSUNDEEP
isabelle
thor
thor

Reputation: 22480

Why is this seemingly incorrect proof OK with Isabelle?

While copying the following proof from the PDF tutorial of Isabelle 2020 into the IDE (about Cantor’s theorem that a function from a set to its powerset cannot be surjective), I made a typo on the "from 1 have 2" line.

lemma "¬ surj (f :: 'a ⇒ 'a set)"
proof
  assume 0: "surj f"
  from 0 have 1: "∀ A. ∃ a. A = f a" by(simp add: surj_def )
  from 1 have 2: "∃ a. {x. x ∉ f x} = f a" by blast
  from 2 show "False" by blast
qed

, so that the line now reads (with a wrong forall quantifier)

  from 1 have 2: "∀ a. {x. x ∉ f x} = f a" by blast

Strangely, both the original proof in the example and this changed version work. But the changed version is incorrect, isn't it?

Am I missing something or can someone explain how the changed version (below) is correct?

lemma "¬ surj (f :: 'a ⇒ 'a set)"
proof
  assume 0: "surj f"
  from 0 have 1: "∀ A. ∃ a. A = f a" by(simp add: surj_def )
  from 1 have 2: "∀ a. {x. x ∉ f x} = f a" by blast
  from 2 show "False" by blast
qed

--- Update ---

To help diagnose the problem, below is the output when I place the mouse on the "from 2 show ..." line. It mentions an exported rule, which seems to be the theorem to be proven. (I don't remember exporting the rule myself, other than maybe accidentally getting the quantifier right in a few trials.)

show False 
Successful attempt to solve goal by exported rule:
  (surj f) ⟹ False 
proof (state)
this:
  False

goal:
No subgoals!

I just tried closing Isabelle and reopening the same .thy file, and got the same result. (As you can see, I am new to the Isabelle environment). Did I just save the theorem somewhere when I entered the right text?

Upvotes: 0

Views: 215

Answers (1)

Mathias Fleury
Mathias Fleury

Reputation: 2261

Which Isabelle version are you using? On mine the blast call does not terminate (within a few seconds), as highlighted by the background:

Isabelle version of the proof

However, Isabelle is optimistic: it assumes that blast will eventually terminate (it won't). Hence the next step is checked (and that one holds because types are not empty: "∀ a. P a", then "∃ a. P a"). That might give you the impression that the proof is going through, but it is not the case.

Upvotes: 2

Related Questions