Can someone explain to me what this error is saying

Stream: general

[Frederick Pu]

Screenshot-2024-04-01-144614.png

[Bolton Bailey]

This usually means you have already completed the proof, and you can just delete the tactic that is giving you this error and everything should work.

[Frederick Pu]

Bolton Bailey said:

This usually means you have already completed the proof, and you can just delete the tactic that is giving you this error and everything should work.

But when I delete it I get an unsolved goal error.
Screenshot-2024-04-01-211215.png

[David Renshaw]

what if you remove the curly braces?

[Mario Carneiro]

the issue is that decreasing_by is a state with multiple goals, one per recursive call, so you need all_goals to apply the tactic sequence to every goal, or multiple braces if you want to prove them separately

[Mario Carneiro]

Also keep in mind that curly braces are not a no-op in the tactic language; they focus on the first goal and lean/std/mathlib usually uses · tacs for this instead. The no-op grouping device in the tactic language is ( ... )

[Mario Carneiro]

I think this is a bug in the decreasing_by parser though; most places which accept tactic sequences also accept a braced group, but usually the initial state only has one goal so it's not observable whether you are using the { ... } tactic combinator or the tacticSeqBracketed syntax. cc: @Joachim Breitner

[Frederick Pu]

Mario Carneiro said:

the issue is that decreasing_by is a state with multiple goals, one per recursive call, so you need all_goals to apply the tactic sequence to every goal, or multiple braces if you want to prove them separately

I know it doesnt apply in this case, but what if you have multiple different wf goals that require different tactics to prove?

[Mario Carneiro]

the intent is that you would write something like this:

decreasing_by
  · proof for first call
  · proof for second call
    more proof
  · proof for third call

or:

decreasing_by
  all_goals
    proof for every call

[Mario Carneiro]

if you like to use braces, you could also format it as

 decreasing_by
  {
    proof for first call
  }
  {
    proof for second call
    more proof
  }
  {
    proof for third call
  }

(but note the lack of surrounding braces), or

 decreasing_by (
  {
    proof for first call
  }
  {
    proof for second call
    more proof
  }
  {
    proof for third call
  }
)

if you really want some outer delimiters

[Joachim Breitner]

Which version of lean is that? It looks to me that you are seeing the effect of the old behavior, where the decreasing_by is applied to each goal separately, so for one goal simp_wf works and then the simp call fails, and for another one you need the simp, and now you have to juggle with try or first… precisely the kind of confusion I was hoping to reduce by that refactoring. (The termination_by set_subtrees is a hint that this is an older version of lean.)

[Joachim Breitner]

Oh, and to help @Frederick Pu with their problem on their version of Lean; can you try simp_wf ; try simp [ … ]?

[Frederick Pu]

Joachim Breitner said:

Oh, and to help Frederick Pu with their problem on their version of Lean; can you try simp_wf ; try simp [ … ]?

Yeah thanks that works although it's not really relevant in this case. Probably be a useful trick when I have multiple wf goals tho