[isabelle-dev] Pink tactics

[Jasmin Blanchette]

Dear colleagues,

Sledgehammer invokes "simp" as part of proof reconstruction. I'm currently adding a mode, inspired by Magnushammer [1], where the simplifier is applied directly, without relying on an automatic theorem prover. However, for this to work, I need to call "by (simp add: ...)" with a timeout, where "..." is a potentially long list of lemmas that might lead to nontermination.

What happens quite often is that the "simp" call (actually, a call to "Goal.prove" in ML) throws "Interrupt". This is propagated through Sledgehammer and leads to the "sledgehammer" command to stop working and turn pink.

The issue is not restricted to "simp". "using ... by auto" can also lead to the same behavior.

I can sometimes reproduce the issue without Sledgehammer, using repository version Isabelle/10d85056cf3b. I write "sometimes" because it's clearly nondeterministic. Here's a .thy file:

theory Scratch
  imports Main
begin

lemma "1 + 2 = 4"
  apply (simp add: one_add_one numeral_plus_one one_plus_numeral numeral_eq_one_iff one_eq_numeral_iff semiring_norm(85) semiring_norm(83) numeral_plus_numeral add_numeral_left numeral_One numeral_Bit0 one_plus_numeral_commute Let_numeral numeral_eq_iff semiring_norm(87) semiring_norm(6) semiring_norm(2) numerals(1) nat_1_add_1 add_One_commute is_num_normalize(1) semiring_norm(82) dbl_simps(3) verit_eq_simplify(8) Let_1 add_right_cancel add_left_cancel verit_eq_simplify(10) add_neg_numeral_special(9) dbl_simps(5) neg_equal_iff_equal add.inverse_inverse verit_minus_simplify(4) neg_numeral_eq_iff Let_neg_numeral minus_add_distrib minus_add_cancel add_minus_cancel add_neg_numeral_simps(3) dbl_simps(1) neg_one_eq_numeral_iff numeral_eq_neg_one_iff semiring_norm(167) dbl_simps(4) add.inverse_distrib_swap group_cancel.neg1 minus_equation_iff equation_minus_iff verit_negate_coefficient(3) neg_numeral_neq_numeral numeral_neq_neg_numeral is_num_normalize(8) one_neq_neg_one numeral_neq_neg_one one_neq_neg_numeral dbl_def uminus_numeral_One ab_semigroup_add_class.add_ac(1) add_mono_thms_linordered_semiring(4) group_cancel.add1 group_cancel.add2 add.assoc add.left_cancel add.right_cancel add.commute)

end

The enclosed screenshots show what happens. If there's a way to call a tactic with a timeout as a blackbox, without risk of triggering fatal errors that lead Sledgehammer to entirely fail (i.e., become pink), I would be a taker.

Best,
Jasmin

[1] https://arxiv.org/abs/2303.04488

--
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 9337
Email: jasmin.blanchette at ifi.lmu.de
Web: https://www.tcs.ifi.lmu.de/



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230828/08239f59/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screenshot 2023-08-28 at 17.22.13.png
Type: image/png
Size: 25966 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230828/08239f59/attachment-0002.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screenshot 2023-08-28 at 17.21.56.png
Type: image/png
Size: 26045 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230828/08239f59/attachment-0003.png>