Unfocus goal after`decreasing_by`

Stream: lean4

[Martin Dvořák]

There is Ackermann function in Mathlib:
https://github.com/leanprover-community/mathlib4/blob/fd3a089b1eae469ba1e1d14ec4f1c3e568f187de/Mathlib/Computability/Ackermann.lean#L62
Specifying termination_by was sufficient in the declaration; it was automatically inferred that the recursion was decreasing on the lexicographical ordering of the pair of Nat arguments.
Nevertheless, I wanted to see how to prove decreasing_by manually.

So I copied the definition and added the decreasing_by part at the end:

import Mathlib.Tactic

def ackermann : Nat → Nat → Nat
| 0  , n   => n+1
| m+1, 0   => ackermann m 1
| m+1, n+1 => ackermann m (ackermann (m+1) n)
termination_by ackermann m n => (m, n)
decreasing_by
  simp_wf
  left
  simp

My problem is that all three goals are focused.
It is OK when I perform simp_wf on all goals simultaneously.
However, the subsequent left must not be performed on the last goal.
How can I unfocus the last goal (or focus only the first one) please?
Unsurprisingly, I am required to prove False after the simp on the last line.

[Yaël Dillies]

What about

first
| left
  simp
| simp

[Martin Dvořák]

I am not sure what first is supposed to so, but it doesn't work here.

[Sebastian Ullrich]

If you want to give case-specific proofs, use have

[Martin Dvořák]

I'd first need to specify which goal is focused. Otherwise my have part gets opened in all three goals (in some of them, it might not even have all necessary terms in the context).

[Sebastian Ullrich]

I mean a term have in the respective branch, like the error message suggests when the default decreasing_by fails

[Martin Dvořák]

I don't understand.

[Daniil Kisel]

It is enough to have a hypothesis in scope of the recursive call and you can provide it with have just before the call.

[Martin Dvořák]

I am sorry I don't understand the last two comments.
Could you please show me what you mean in code?

[Daniil Kisel]

def f (n : Nat) : Nat :=
  if n = 0
    then 0
    else
      have : n / 10 < n := sorry
      f (n / 10)
termination_by _ => n

[Martin Dvořák]

Oh I see!

import Mathlib.Tactic

def ackermann : Nat → Nat → Nat
| 0  , n   => n+1
| m+1, 0   =>
    have wfm : Prod.Lex
        (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂)
        (m, 1) (Nat.succ m, 0) := by
      left
      exact lt_add_one m
    ackermann m 1
| m+1, n+1 =>
    have wfn : Prod.Lex
        (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂)
        (m+1, n) (m+1, n+1) := by
      right
      exact lt_add_one n
    ackermann m (ackermann (m+1) n)
termination_by ackermann m n => (m, n)
decreasing_by
  simp_wf
  simp_all

Now my wfm and wfn are used by the simp_all and only one goal remains open!

[Martin Dvořák]

Nevertheless, cannot I simply focus one goal at a time?

[Daniil Kisel]

(deleted)

[James Gallicchio]

I think the decreasing_by tactic is just run blindly on each of the goals. So no? This is definitely a restriction, in particular it is impossible to do forward reasoning without manually copying the goals into haves

[Eric Wieser]

I think we've seen cases in the past where the haves have been rejected by the linter, forcing the use of decreasing_by instead; maybe @Yaël Dillies remembers...

[Yaël Dillies]

Eric, I think we now understand what's causing this: The have really are necessary within the definition, but then they mistakenly make their way onto the equational lemmas, meaning that whenever you unfold the definition somewhere else, they become unused haves.