decreasing_by goals leak wf implementation details

[nomeata]

The goals shown by decreasing_by can contain scary implementation details, especially the PSigma/PSum due to non-unary functions and mutual recursion.

The simp_wf tactic is typically used to clean that up, but, as it runs unrestricted simp, may do too much.

It seems desirable that after decreasing_by the goal shown to the user is exactly what they expect based on what they wrote – no implementation details visible, but also no additional proof steps taken.

There is a similar issue in the FunInd code, where Lean.Tactic.FunInd.cleanPackedArgs is used to clean this up; this can be inspiration.

Versions

v4.11.0-rc1

Additional Information

Zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60simp_wf.60.20in.20.60decreasing_by.60

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

So after

def g (x : Nat) (y : Nat) : Nat := g (x - 1) y
decreasing_by

we have

x y : Nat
⊢ (invImage (fun x => PSigma.casesOn x fun x y => x) instWellFoundedRelationOfSizeOf).1 ⟨x - 1, y⟩ ⟨x, y⟩

If we now run

  try simp (config := { unfoldPartialApp := true, zetaDelta := true }) only [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]

which is simp_wf with an only added we get

⊢ (sizeOf (x - 1)).lt (sizeOf x)

which isn’t great. We’d have to throw in

simp only [sizeOf_nat, Nat.lt_eq]

I can thow them into the simp arguments, but this is of course optimizing for the special case of Nat arguments, and if the termination is via sizeOf or Nat then the goal would be not as clean. Probably ok.

So one fix would be to change simp_wf to run simp only, and run it always, and (for backwards compat) add a simple simp call to the beginning of decreasing_tactic. Trying that.