Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] RC2: different sledgehammer behaviour with using

view this post on Zulip Email Gateway (Oct 01 2026 at 09:08):

From: Peter <cl-isabelle-users@lists.cam.ac.uk>

Hi List,

I'm currently porting stuff (myself,  not AI-assisted, to be able to
write reports like this) from 2025-2 -> 2026-RC2.

One pattern that I typically use when a metis/smt call fails (e.g. due
to a changed lemma name) was

using <lemms that still exist> sledgehammer

and this will quickly find the new names for the missing lemmas. Now,
however, I get a strange error message about one-line proof
reconstruction failed, then coming back with an essential one-line Isar
proof, that actually would have worked as a one-line proof.

--

Peter

Here's my example:

case False
    then show ?thesis
      using ab add.commute error_def zerosign_def
      sledgehammer

Sledgehammering...
cvc5 found a proof...
vampire found a proof...
spass found a proof...
e found a proof...
verit found a proof...
cvc5: One-line proof reconstruction failed: by (smt (verit))
spass: One-line proof reconstruction failed:
  by (metis diff_add_cancel[of "valof (IEEE.round To_nearest (valof a +
valof b))" "valof a + valof b"])

Isar proof (108 ms):
proof -
  show ?thesis
    by (metis False ab add.commute diff_add_cancel error_def zerosign_def)
qed
e: One-line proof reconstruction failed:
  by (metis add_minus_cancel[of "valof a + valof b" "- (- (valof a +
valof b)) + (- (- (- (valof a + valof b))) + valof (a + b))"]
    add_minus_cancel[of "- (valof a + valof b)" "- (- (- (valof a +
valof b))) + valof (a + b)"]
    add_minus_cancel[of "- (- (valof a + valof b))" "valof (a + b)"]
    add_minus_cancel[of "valof a + valof b" "- (- (valof a + valof b))

Isar proof (969 ms):
proof -
  show ?thesis
    by (smt (verit) False ab error_def zerosign_def)
qed
Done

But note that the proposed Isar-proofs are essentially one-liners, and
work when used as such, e.g., the following is perfectly valid.

case False
    then show ?thesis
      using ab add.commute error_def zerosign_def
        by (metis False ab add.commute diff_add_cancel error_def
zerosign_def)

and so it keeps valid when manually removing the already "used" lemmas
from the metis call.

then show ?thesis
      using ab add.commute error_def zerosign_def
        by (metis diff_add_cancel )

view this post on Zulip Email Gateway (Oct 05 2026 at 09:50):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>

Dear Peter,

Thanks for your detailed report. Unfortunately, it's not quite detailed enough -- it's not self-contained. Is there any chance that you could send us a .thy file that can be processed, ideally using "Main" as its only "import"?

In the meantime, I'll see if I can reproduce the issue on my side by blindly playing around.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/staff/jasmin-blanchette

On 1. Oct 2026, at 11:08, Peter (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:

Hi List,

I'm currently porting stuff (myself, not AI-assisted, to be able to write reports like this) from 2025-2 -> 2026-RC2.

One pattern that I typically use when a metis/smt call fails (e.g. due to a changed lemma name) was

using <lemms that still exist> sledgehammer

and this will quickly find the new names for the missing lemmas. Now, however, I get a strange error message about one-line proof reconstruction failed, then coming back with an essential one-line Isar proof, that actually would have worked as a one-line proof.

--

Peter

Here's my example:

case False
then show ?thesis
using ab add.commute error_def zerosign_def
sledgehammer

Sledgehammering...
cvc5 found a proof...
vampire found a proof...
spass found a proof...
e found a proof...
verit found a proof...
cvc5: One-line proof reconstruction failed: by (smt (verit))
spass: One-line proof reconstruction failed:
by (metis diff_add_cancel[of "valof (IEEE.round To_nearest (valof a + valof b))" "valof a + valof b"])

Isar proof (108 ms):
proof -
show ?thesis
by (metis False ab add.commute diff_add_cancel error_def zerosign_def)
qed
e: One-line proof reconstruction failed:
by (metis add_minus_cancel[of "valof a + valof b" "- (- (valof a + valof b)) + (- (- (- (valof a + valof b))) + valof (a + b))"]
add_minus_cancel[of "- (valof a + valof b)" "- (- (- (valof a + valof b))) + valof (a + b)"]
add_minus_cancel[of "- (- (valof a + valof b))" "valof (a + b)"]
add_minus_cancel[of "valof a + valof b" "- (- (valof a + valof b)) + - (- (valof a + valof b))"]
add_minus_cancel[of "- (valof a + valof b)" "- (- (valof a + valof b))"] add_minus_cancel[of "- (valof a + valof b)" "valof a + valof b"]
diff_minus_eq_add[of "- (- (valof a + valof b)) + (- (- (- (valof a + valof b))) + valof (a + b))" "- (valof a + valof b)"]
diff_minus_eq_add[of "- (valof a + valof b)" "- (- (valof a + valof b)) + - (- (valof a + valof b))"]
diff_minus_eq_add[of "- (valof a + valof b)" "- (- (valof a + valof b)) + (valof a + valof b)"])
vampire: One-line proof reconstruction failed:
by (metis add_minus_cancel[of "valof a + valof b" "valof (IEEE.round To_nearest (valof a + valof b))"]
add_uminus_conv_diff[of "valof (IEEE.round To_nearest (valof a + valof b))" "valof a + valof b"])
verit: One-line proof reconstruction failed: by (smt (verit))

Isar proof (969 ms):
proof -
show ?thesis
by (smt (verit) False ab error_def zerosign_def)
qed
Done

But note that the proposed Isar-proofs are essentially one-liners, and work when used as such, e.g., the following is perfectly valid.

case False
then show ?thesis
using ab add.commute error_def zerosign_def
by (metis False ab add.commute diff_add_cancel error_def zerosign_def)

and so it keeps valid when manually removing the already "used" lemmas from the metis call.

then show ?thesis
using ab add.commute error_def zerosign_def
by (metis diff_add_cancel )

smime.p7s

view this post on Zulip Email Gateway (Oct 05 2026 at 10:03):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>

Hi Peter, all,

Good news: I was able to reproduce the problem with this example (put right at the bottom of "Sledgehammer.thy"):

lemma "(x::nat) = 0 ∨ x > 0"
proof (cases "x = 0")
case False
then show ?thesis
using zero_less_iff_neq_zero
sledgehammer[vampire, dont_try0]

It would appear that "using ..." is ignored in the reconstruction code. I'll investigate.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/staff/jasmin-blanchette

On 5. Oct 2026, at 11:49, Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de> wrote:

Dear Peter,

Thanks for your detailed report. Unfortunately, it's not quite detailed enough -- it's not self-contained. Is there any chance that you could send us a .thy file that can be processed, ideally using "Main" as its only "import"?

In the meantime, I'll see if I can reproduce the issue on my side by blindly playing around.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/staff/jasmin-blanchette

On 1. Oct 2026, at 11:08, Peter (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:

Hi List,

I'm currently porting stuff (myself, not AI-assisted, to be able to write reports like this) from 2025-2 -> 2026-RC2.

One pattern that I typically use when a metis/smt call fails (e.g. due to a changed lemma name) was

using <lemms that still exist> sledgehammer

and this will quickly find the new names for the missing lemmas. Now, however, I get a strange error message about one-line proof reconstruction failed, then coming back with an essential one-line Isar proof, that actually would have worked as a one-line proof.

--

Peter

Here's my example:

case False
then show ?thesis
using ab add.commute error_def zerosign_def
sledgehammer

Sledgehammering...
cvc5 found a proof...
vampire found a proof...
spass found a proof...
e found a proof...
verit found a proof...
cvc5: One-line proof reconstruction failed: by (smt (verit))
spass: One-line proof reconstruction failed:
by (metis diff_add_cancel[of "valof (IEEE.round To_nearest (valof a + valof b))" "valof a + valof b"])

Isar proof (108 ms):
proof -
show ?thesis
by (metis False ab add.commute diff_add_cancel error_def zerosign_def)
qed
e: One-line proof reconstruction failed:
by (metis add_minus_cancel[of "valof a + valof b" "- (- (valof a + valof b)) + (- (- (- (valof a + valof b))) + valof (a + b))"]
add_minus_cancel[of "- (valof a + valof b)" "- (- (- (valof a + valof b))) + valof (a + b)"]
add_minus_cancel[of "- (- (valof a + valof b))" "valof (a + b)"]
add_minus_cancel[of "valof a + valof b" "- (- (valof a + valof b)) + - (- (valof a + valof b))"]
add_minus_cancel[of "- (valof a + valof b)" "- (- (valof a + valof b))"] add_minus_cancel[of "- (valof a + valof b)" "valof a + valof b"]
diff_minus_eq_add[of "- (- (valof a + valof b)) + (- (- (- (valof a + valof b))) + valof (a + b))" "- (valof a + valof b)"]
diff_minus_eq_add[of "- (valof a + valof b)" "- (- (valof a + valof b)) + - (- (valof a + valof b))"]
diff_minus_eq_add[of "- (valof a + valof b)" "- (- (valof a + valof b)) + (valof a + valof b)"])
vampire: One-line proof reconstruction failed:
by (metis add_minus_cancel[of "valof a + valof b" "valof (IEEE.round To_nearest (valof a + valof b))"]
add_uminus_conv_diff[of "valof (IEEE.round To_nearest (valof a + valof b))" "valof a + valof b"])
verit: One-line proof reconstruction failed: by (smt (verit))

Isar proof (969 ms):
proof -
show ?thesis
by (smt (verit) False ab error_def zerosign_def)
qed
Done

But note that the proposed Isar-proofs are essentially one-liners, and work when used as such, e.g., the following is perfectly valid.

case False
then show ?thesis
using ab add.commute error_def zerosign_def
by (metis False ab add.commute diff_add_cancel error_def zerosign_def)

and so it keeps valid when manually removing the already "used" lemmas from the metis call.

then show ?thesis
using ab add.commute error_def zerosign_def
by (metis diff_add_cancel )

smime.p7s

view this post on Zulip Email Gateway (Oct 05 2026 at 11:46):

From: Makarius <makarius@sketis.net>

On 05/10/2026 12:03, Jasmin Blanchette wrote:

Hi Peter, all,

Good news: I was able to reproduce the problem with this example (put right at
the bottom of "Sledgehammer.thy"):

lemma "(x::nat) = 0 ∨ x > 0"
proof (cases "x = 0")
  case False
  then show ?thesis
    using zero_less_iff_neq_zero
    sledgehammer[vampire, dont_try0]

It would appear that "using ..." is ignored in the reconstruction code. I'll
investigate.
Great. I will wait until the evening with the pending Isabelle2026-RC3
(approx. 18:00 Royal Bavarian Time).

Makarius

view this post on Zulip Email Gateway (Oct 05 2026 at 11:59):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>

Hi Makarius,

Please apply the attached export.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/staff/jasmin-blanchette



On 1. Oct 2026, at 11:08, Peter (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:

Hi List,

I'm currently porting stuff (myself, not AI-assisted, to be able to write reports like this) from 2025-2 -> 2026-RC2.

One pattern that I typically use when a metis/smt call fails (e.g. due to a changed lemma name) was

using <lemms that still exist> sledgehammer

and this will quickly find the new names for the missing lemmas. Now, however, I get a strange error message about one-line proof reconstruction failed, then coming back with an essential one-line Isar proof, that actually would have worked as a one-line proof.

--

Peter

Here's my example:

case False
then show ?thesis
using ab add.commute error_def zerosign_def
sledgehammer

Sledgehammering...
cvc5 found a proof...
vampire found a proof...
spass found a proof...
e found a proof...
verit found a proof...
cvc5: One-line proof reconstruction failed: by (smt (verit))
spass: One-line proof reconstruction failed:
by (metis diff_add_cancel[of "valof (IEEE.round To_nearest (valof a + valof b))" "valof a + valof b"])

Isar proof (108 ms):
proof -
show ?thesis
by (metis False ab add.commute diff_add_cancel error_def zerosign_def)
qed
e: One-line proof reconstruction failed:
by (metis add_minus_cancel[of "valof a + valof b" "- (- (valof a + valof b)) + (- (- (- (valof a + valof b))) + valof (a + b))"]
add_minus_cancel[of "- (valof a + valof b)" "- (- (- (valof a + valof b))) + valof (a + b)"]
add_minus_cancel[of "- (- (valof a + valof b))" "valof (a + b)"]
add_minus_cancel[of "valof a + valof b" "- (- (valof a + valof b)) + - (- (valof a + valof b))"]
add_minus_cancel[of "- (valof a + valof b)" "- (- (valof a + valof b))"] add_minus_cancel[of "- (valof a + valof b)" "valof a + valof b"]
diff_minus_eq_add[of "- (- (valof a + valof b)) + (- (- (- (valof a + valof b))) + valof (a + b))" "- (valof a + valof b)"]
diff_minus_eq_add[of "- (valof a + valof b)" "- (- (valof a + valof b)) + - (- (valof a + valof b))"]
diff_minus_eq_add[of "- (valof a + valof b)" "- (- (valof a + valof b)) + (valof a + valof b)"])
vampire: One-line proof reconstruction failed:
by (metis add_minus_cancel[of "valof a + valof b" "valof (IEEE.round To_nearest (valof a + valof b))"]
add_uminus_conv_diff[of "valof (IEEE.round To_nearest (valof a + valof b))" "valof a + valof b"])
verit: One-line proof reconstruction failed: by (smt (verit))

Isar proof (969 ms):
proof -
show ?thesis
by (smt (verit) False ab error_def zerosign_def)
qed
Done

But note that the proposed Isar-proofs are essentially one-liners, and work when used as such, e.g., the following is perfectly valid.

case False
then show ?thesis
using ab add.commute error_def zerosign_def
by (metis False ab add.commute diff_add_cancel error_def zerosign_def)

and so it keeps valid when manually removing the already "used" lemmas from the metis call.

then show ?thesis
using ab add.commute error_def zerosign_def
by (metis diff_add_cancel )

sledgehammer.export
smime.p7s

view this post on Zulip Email Gateway (Oct 05 2026 at 13:31):

From: Makarius <makarius@sketis.net>

On 05/10/2026 13:59, Jasmin Blanchette wrote:

Hi Makarius,

Please apply the attached export.
OK, it will be in Isabelle2026-RC3 (later today).

Makarius

view this post on Zulip Email Gateway (Oct 05 2026 at 21:41):

From: Makarius <makarius@sketis.net>

On 05/10/2026 13:59, Jasmin Blanchette wrote:

Hi Makarius,

Please apply the attached export.

I have done that for Isabelle2026-RC3, but have not tried out anything myself.

Makarius

Last updated: Oct 08 2026 at 21:07 UTC