isabelle

Why this trivally incorrect lemma can be proved using sos?

I'm new to Isabelle and have encountered a problem that I'm struggling with. I have the following lemma:

imports Main HOL.HOL HOL.Real "HOL-Library.Sum_of_Squares"

lemma 
  fixes r :: real
  assumes "r = 8/7" 
  shows "r = 2"
proof-
  show "r = 2" using assms by sos 
qed

I would like to understand why Isabelle accepts this proof despite the contradiction. Is it something related to the sos method, or am I misunderstanding something fundamental about the way proofs work in Isabelle?

Any insights would be greatly appreciated, and I thank you in advance for your help.

The Isabelle theorem prover accepts this proof and outputs "No subgoals!" However, I'm puzzled, as the lemma is clearly incorrect.

Solution

  • This is mostly a user interface problem. The Isabelle/jEdit 2022 window for this proof should look like this:

    Isabelle editor window with by sos highlighted in thistle

    Notice that the by sos is still highlighted in thistle. This is Isabelle/jEdit's way of communicating that the proof method has not terminated yet. (But it also has not given up yet. Giving up would be highlighted in pink.)

    Compare the line to the trivial by rule proof that I've added in the line above. This is what checked proof steps look like.

    Thus, by sos has not proven the bogus claim. (Phew!)

    Then what's with the “No subgoals”?

    But why is Isabelle then claiming No subgoals in the proof state?! The answer is that Isabelle tries to check the theory in a parallelized manner. A proof method that takes long should not block the other proof-checking threads. So, other threads continue from that line with the hypothesis that, should by sos terminate, there would be no remaining subgoals and they could use the proven lemma.

    The main effect of this is that one can open, check, and edit theories much faster than one could if there were no parallelization. But it also means that following proof steps could indeed complete even though the theory is broken.

    As long as there are any highlighted proof steps, everything below could be false, even though individual proof steps are sound.