Commenting with `SPC c l` puts server in state where it can derive "False" from nothing

[James-Hanson]

Open the following file MWE.thy in isabelle-emacs:

theory MWE imports
    Main
begin

lemma "False"
    sledgehammer

Wait until Sledgehammer reports No proof found. Comment and then uncomment with SPC c l. Sledgehammer now reports:

 Sledgehammering...
 spass found a proof...
 spass: Try this: |1|: by (metis Unity_def old.unit.exhaust) (> 1.0 s, timed out)

I've tried this in two different installations. I haven't been able to replicate this in jEdit, so I'm guessing it has something to do with isabelle-emacs in particular.

[m-fleury]

First the most important thing: Sledgehammer giving you a proof that does not impact correctness. Actually it is the entire point of Isabelle not trusting external tools and rechecking the proof.

Now it does happen on Isabelle/jEdit:

lemma False
  sledgehammer[spass,debug](Unity_def old.unit.exhaust)
  oops

(the difference is that emacs and Isabelle/jEdit are using a different file to store the state for Sledgehammer)

If you want to look at the proof, you can do:

  sledgehammer[spass,debug,overlord](Unity_def old.unit.exhaust)

and read the files .isabelle/Isabelle2023-vsce/prob_spass_1.p and .isabelle/Isabelle2023-vsce/prob_spass_1_proof.p

[m-fleury]

If you are interested in the proofs:

list_of_formulae(axioms).
formula(equal:lt(product_Unity, product_Abs_unit(fTruE)), fact_0_Unity__def, 900). % Unity_def
formula(forall([Y : product_unit], equal(Y, product_Unity)), fact_1_old_Ounit_Oexhaust, 2250). % old.unit.exhaust

formula(not(pp(fFalsE)), help_pp_1_1_U).
formula(forall([P : booL], or(equal(P, fTruE), equal(P, fFalsE))), help_fTrue_1_1_T).
formula(pp(fTruE), help_fTrue_1_1_U).
end_of_list.

(d0,A,r1000,rw2000) 1[0:Inp] ||  -> pp(fTruE)*. derived from formulae  help_fTrue_1_1_U
(d0,A,r2250,rw49500) 2[0:Inp] ||  -> equal(U:product_unit,product_Unity)*. derived from formulae  fact_1_old_Ounit_Oexhaust
(d0,A,r1000,rw3000) 3[0:Inp] || pp(fFalsE)* -> . derived from formulae  help_pp_1_1_U
(d0,A,r900,rw3600) 4[0:Inp] ||  -> equal(product_Unity,product_Abs_unit(fTruE))**. derived from formulae  fact_0_Unity__def
(d0,A,r1000,rw44000) 5[0:Inp] ||  -> equal(V:booL,fFalsE) equal(V:booL,fTruE)*. derived from formulae  help_fTrue_1_1_T
(d0,A,r900,rw20700) 6[0:Rew:4.0,2.0] ||  -> equal(U:product_unit,product_Abs_unit(fTruE))*.
(d1,A,r900,rw115200) 10[0:SpR:5.1,6.0] ||  -> equal(V:booL,fFalsE) equal(U:product_unit,product_Abs_unit(V:booL))*.
(d2,A,r900,rw118800) 13[0:SpR:10.1,6.0] ||  -> equal(fTruE,fFalsE)** equal(U:product_unit,W:product_unit)*.
(d2,A,r900,rw8100) 15[0:Con:13.1] ||  -> equal(fTruE,fFalsE)**.
(d0,A,r900,rw1800) 16[0:Rew:15.0,1.0] ||  -> pp(fFalsE)*.
(d0,A,r0,rw0) 19[0:MRR:16.0,3.0] ||  -> .

Each line is A B -> C D should be read as A v B --> C v D (or ~A v ~B v C v D). As far as I understand, the inference from step 13 to 15 is wrong.

[James-Hanson]

Thank you.

Is this a known bug in Spass or something? Also, is there some way to get Emacs to stop reporting this proof, or would you just recommend ignoring it?

[m-fleury]

Spass is not developed anymore.

What you could do is deleting the Sledgehammer state (just delete the file ~/.isabelle/Isabelle2023-vsce/mash_state). The wrong proof might come back though. Or you just ignore it.