nested exception: no goals

Stream: general

[Scott Morrison]

Anyone ever seen this before:

The nested exception contains the failure state for the decreasing tactic.
nested exception message:
tactic failed, there are no goals to be solved
state:
no goals

[Keeley Hoek]

Does it just mean that dec_tac in using_well_founded failed because a tactic inside expected goals when there weren't any, e.g. with an appeal to refl at the end when everything is gone already?

[Scott Morrison]

Hmm... I was getting this without an explicit using_well_founded!

[Scott Morrison]

Anyone, I seem to have found a workaround.

[Keeley Hoek]

I would suspect that the culprit is something like the tactic.dunfold_targets in init.meta.well_founded_tactics (which run by default)

[Keeley Hoek]

Probably there should be some trys wrapping some of that code

[Scott Morrison]

ah... I had just found that same file. :-)

[Scott Morrison]

But this is in core :-(

[Scott Morrison]

So sad.

[Keeley Hoek]

indeed

[Scott Morrison]

3.5...

[Keeley Hoek]

I half typed a comment about that but thought it was a bit sassy

[Scott Morrison]

Ok, I've addressed this problem in #1419. It comes at a slight cost: having to add using_well_founded { dec_tac := well_founded_tactics.default_dec_tac' } to half a dozen proofs across mathlib, to used the patched version of default_dec_tac.

[Scott Morrison]

I think it's worth it however, to let us make simp better at inequalities.

[Keeley Hoek]

@Scott Morrison I think you could do better with the syntax by just defining a structure somewhere with a short name (e.g. wf_tacs) and type well_founded_tactics, equal to { dec_tac := well_founded_tactics.default_dec_tac' }.

[Keeley Hoek]

Then using_well_founded wf_tacs works. Depending on how much of a hack using_well_founded is in the parser (probably a lot), we could even define notation for that; maybe using_well_founded'

[Keeley Hoek]

Yeah, I have no idea how to do the notation thing, probably not possible.

[Keeley Hoek]

Actually, I think with some work I could make it work if you wrote recdef instead of def for the recursive definition, but I don't know a way to make using_well_founded wf_tacs shorter.

[Keeley Hoek]

Also, we should put default_dec_tac' in lean 3.5.0 right away

[Scott Morrison]

What is the procedure for adding patched tactics in 3.5.0? We both replace the old broken tactic, and add the primed version as an alias for backwards compatibility?

[Scott Morrison]

Thanks for this syntax suggestion, I've added it to the PR now.

[Keeley Hoek]

I think maybe no-one has patched a tactic yet?
Or just, maybe they have fixed bugs like stuff crashing all of lean if you use it wrong.---not a useful enough fix to warrant a copy to mathlib.