Hi Eugene,Thanks for providing the files. In your example the reconstruction with by (smt (verit) ...) works but take more time than the timeout used by Sledgehammer.
Sadly, this is an example that I cannot fix. Sledgehammer has some expectations on Skolemization steps that are not true for the proof format of veriT, leading to such weird bugs. Many proofs can be fitted to fit the expectations, but others cannot easily -- and that one cannot.
If this is a big issue for you, the solution is to remove veriT from the provers used by Sledgehammer.
Sorry for the inconveniance, Mathias On 13/02/2021 17:20, Eugene W. Stark wrote:
This has occurred again and I was able to capture the files involved. I am forwarding them to you in an off-list message. I would note that it is not necessarily repeatable on every try -- I think it must depend on some cache state or other randomness. However, I hope that if you try it several times you will be able to repeat what I am seeing (I included a screenshot to show it). - Gene Stark On 1/31/21 8:27 AM, Eugene W. Stark wrote:I apologize. I tried to "git stash" to save what I had done since posting, but Isabelle auto-reloaded the theory I was working on and nuked the undo history. I am finding it impossible now to work back to the place where I observed the problem. If it occurs again, I will make a better effort to capture a context for you. Thanks. On 1/31/21 7:47 AM, Eugene W. Stark wrote:It is part of a context of something like 3K lines of code. Is that useful to you? On 1/31/21 7:43 AM, Mathias Fleury wrote:Hi Eugene, Can you also provide the lemma? The conversion from proofs generated by veriT to Isar proofs is very complicated, but I cannot fix it without being the context to reproduce it… Thanks, Mathias On 31/01/2021 13:31, Eugene W. Stark wrote:The following has happened to me twice now. I have never seen this type of failure before. Using "try", I get the following suggestion:Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and "nitpick"... "verit": Sledgehammer ("verit") found a proof: by (smt (verit) "1" R.coinitial_ide_is_con R.comp_def R.composite_of_def R.conI R.con_comp R.cong_reflexive R.has_composites' R.join_of_join R.join_of_unique_upto R.join_src R.null_is_zero(1) R.pre_rts_axioms R.pre_rts_with_joins_axioms R.prfx_implies_con R.resid_reflects_con R.residuation_axioms R.rts_axioms R.rts_with_composites_axioms R.src_eqI calculation commutative_square_def comp_null(1) null_char pre_rts.prfx_implies_con pre_rts_with_joins.has_joins residuation.arrI residuation.con_def residuation.con_iff_arr_resid residuation.con_sym rts.composite_comp(2) rts.extensional rts.resid_comp(1) rts.resid_comp(2) rts.resid_join(1) rts.resid_join(2) rts.resid_join(3) rts_with_composites.comp_assoc seqI seq_char) (> 1.0 s, timed out) Isar proof (4 ms): proof - have "h ▹ f ≠ h ▹ null ∨ null ≠ h ▹ null ∨ null ≠ R.null ∨ h ▹ f = R.null" by auto qedThe Isar proof is not workable, for obvious reasons.