How do you use `termination_by`?

Stream: lean4

[Thomas Murrills]

I can't see any documentation for termination_by—I wonder if I'm looking in the wrong files (Init.WF.lean, Lean.Elab.PreDefinition.WF.TerminationHint.lean).

As far as I understand it, termination_by <xs> => <y> says that <y> 'can be used to show termination', but I'm not sure how lean uses <y>. What kinds of expressions be used to show termination, and when exactly are they sufficient to do so? (If this relies on a notion of something "decreasing in size", what notion of "decreasing" is allowed?) And what should be on the lhs of the arrow (<xs>)? Thanks! :)

[Gabriel Ebner]

Decreasing as specified by the WellFoundedRelation type class. You can put anything after the arrow that has a WellFoundedRelation instance.

[Eric Wieser]

Would an instance that produces WellFoundedRelation R from IsWellFounded R (<) be a bad idea?

[Heather Macbeth]

@Thomas Murrills I have usually found it convenient to define a SizeOf instance on the type I'm considering. For example, for integer induction,

instance : SizeOf ℤ := ⟨Int.natAbs⟩

(edit: apparently when I did this before I tagged it @[default_instance], too, so maybe there was already an instance which I was overwriting.)

[Heather Macbeth]

Then you are presented with the goal of showing that that quantity is strictly decreasing.

[Eric Wieser]

Surely instead of adding a subjective global instance you should just write termination_by => Int.natAbs some_int_arg?

[Heather Macbeth]

You're right ... my head is in teaching mode, trying to make things as silent as possible. Although in this case I do think this is a better SizeOf for Int than the default one.

[Henrik Böving]

Heather Macbeth said:

Thomas Murrills I have usually found it convenient to define a SizeOf instance on the type I'm considering. For example, for integer induction,

instance : SizeOf ℤ := ⟨Int.natAbs⟩

(edit: apparently when I did this before I tagged it @[default_instance], too, so maybe there was already an instance which I was overwriting.)

Yes there is such an instance, lean auto generates one for all inductive types itnis basically "how many nodes are in the term tree"

[Henrik Böving]

Which is of course not necessarily what you want to have

[Eric Wieser]

Ah, so your point is "there's already a subjective default that is worse in almost every case than my one"!

[Henrik Böving]

Note that you can view the default instance in action by #eval sizeOf foo or alternatively figuring out the name of the auto generated instance with #synth and #print ing it to inspect its code

[Thomas Murrills]

I see, thanks! What I don't quite get is when this is sufficient for proving termination. Sure, we might be able to produce a quantity that's an inhabitant of a type with a well-founded relation—but which quantities/relations are relevant for termination? I'm guessing we try to "lift" the well-foundedness of the relation on a given e.g. argument to the function to something to do with the function itself, but to what exactly? It’s easy to intuit when something should work, but when does it?

[Eric Wieser]

The idea is that the value you provide to termination_by is supposed to decrease with every recursive call

[Eric Wieser]

If you provide nothing then I believe the default is to use a Prod of all your recursive arguments, with lexicographic order (almost but not quite docs4#Lex, which is missing the instance needed to work with termination_by!)

[Thomas Murrills]

If I supply a value, though, how does lean actually try to prove that it does decrease with each call? What tools does it have available? (Do we just need to place some proof in the local context at the point of the recursive call, maybe?)

[Eric Wieser]

I think that's what decreasing_by is for, though I don't know what it tries by default.

[Eric Wieser]

Certainly it knows to try assumption to use local have statements as you suggest

[Henrik Böving]

There is a decreasing_tac it is called iirc that is the default, it should actually be one of the tactics that are macro extensible.