feat: avoid termination_by', introduce WellFounded.wrap

[nomeata]

I’d like to remove support for the termination_by' annotation. Until
#371 it wasn't used anywhere else in
lean, std, mathlib, so this PR removes the single use of it.

It does so using the pattern that can be used to replace uses of
termination_by': Using WellFounded.wrap one can indicate an explicit
WellFounded relation to use.

This also un-privates the wfRel instance for WellFoundedRelation { val // Acc r val }
which looks useful enough.

So this PR uses that pattern to avoid the use of termination_by' here,
and at the same time provides the necessary definitions for others, so
when Lean drops support for termination_by'
(leanprover/lean4#3033), we can tell users how
migrate.

[nomeata]

Maybe there is a more idiomatic name rather than WellFounded.Wrapped and .wrap?

[digama0]

We also need a way to get a well founded relation out of a value of type WellFoundedRelation A (i.e. the thing that termination_by' is expecting).

[nomeata]

Would that be wfr.wf.wrap?

[digama0]

Yes that works. Next challenge: how to get the type inference working correctly when there are multiple arguments involved?

[digama0]

By the way, the wfRel instance in this file is very similar to Wrapped, but it only requires Acc r x instead of WellFounded r. (It is also private so that we didn't have to do the API work for it.)

[nomeata]

Yes that works. Next challenge: how to get the type inference working correctly when there are multiple arguments involved?

What example do you have in mind? I'd expect once the WellFounded is given, all is known?

Note that users will have to manually select and tuple the arguments they care about. But the target audience (users of termination_by') should already know how do deal with that without too much handholding, I'd think?

[digama0]

Yes that works. Next challenge: how to get the type inference working correctly when there are multiple arguments involved?

What example do you have in mind? I'd expect once the WellFounded is given, all is known?

Not exactly, as in this example where the original text was termination_by' ⟨r, hwf⟩, type inference plays a major role in specifying well founded instances. If the instance is a Sigma' type due to tupling the user code might have a pattern match with ⟨a, b, c⟩ in it, and without the expected type provided by lean we would have difficulty typechecking this.

Note that users will have to manually select and tuple the arguments they care about. But the target audience (users of termination_by') should already know how do deal with that without too much handholding, I'd think?

Lean needs quite a lot of handholding to infer dependent sigma types.

[nomeata]

By the way, the wfRel instance in this file is very similar to Wrapped, but it only requires Acc r x instead of WellFounded r. (It is also private so that we didn't have to do the API work for it.)

Interesting, thanks for the pointer. So an alternative would be to make that not private and add

def wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : {x : α // Acc r x} :=
  ⟨_, h.apply x⟩

which is nice, because there are no additional definitions with unused arguments to write and explain, and the instance looks kinda useful anyways.

I have updated the PR accordingly, WDYT?

[nomeata]

Lean needs quite a lot of handholding to infer dependent sigma types.

I’d expect that the user has to define the Wellfounded (PSigma …) type explicitly ahead of times anyways, so by the time they write wf.wrap …, the type is well known? Quite like we see in the wild already with termination_by'.