Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer

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,


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…



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
The Isar proof is not workable, for obvious reasons.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.