termination_by needing implicit argument

Stream: general

[Jin Wei]

I am using recursion to define a function f where one of its argument a is made implicit since it is not directly involved in the definition of f. Later on, I realize the data of a is necessary to prove this recursion terminates.

My natural attempt was to try termination_by @f ... => ... to make a explicit. However, Lean returns an error and says "expected '_' or identifier" after termination_by. I am wondering if there is a way to solve this issue? (I could return back and require a to be explicit, but it will be painful to modify the rest of the code).

[Yaël Dillies]

You can use ‹type_of_a› where you would have used a

[Yaël Dillies]

A bit hazardous, but might work

[Joachim Breitner]

I think the termination_by syntax doesn't care about implicit or explicit. Have you tried using the parameter? Maybe provide a #mwe

[Yaël Dillies]

It does. I've had this problem before.

[Joachim Breitner]

(the f x y z there isn't really a function application, more like a lambda and an identifier in case of mutual recursion)

[Joachim Breitner]

Hmm, I'm still somewhat surprised, so likely I am misunderstanding the issue (or am simply wrong)

[Jin Wei]

Yaël Dillies said:

You can use ‹type_of_a› where you would have used a

Sorry that I don't quite follow. Could you please elaborate on this?

[Yaël Dillies]

You tried termination_by @f a => g a. Instead do termination_by f => g ‹α›, where a : α.

[Joachim Breitner]

Can someone give me an example? I'm probably misunderstanding something, because
https://live.lean-lang.org/#code=def%20foo%20%7Bn%20%3A%20Nat%7D%20%3A%20Nat%20%3A%3D%20%0D%0A%20%20match%20n%20with%20%0D%0A%20%20%7C%200%20%3D%3E%200%0D%0A%20%20%7C%20n%2B1%20%3D%3E%20%40foo%20n%0D%0Atermination_by%20foo%20%3D%3E%20n
seems to work. (Didn't figure out how to copy that code on the phone)

[Jin Wei]

Joachim Breitner said:

Can someone give me an example? I'm probably misunderstanding something, because
https://live.lean-lang.org/#code=def%20foo%20%7Bn%20%3A%20Nat%7D%20%3A%20Nat%20%3A%3D%20%0D%0A%20%20match%20n%20with%20%0D%0A%20%20%7C%200%20%3D%3E%200%0D%0A%20%20%7C%20n%2B1%20%3D%3E%20%40foo%20n%0D%0Atermination_by%20foo%20%3D%3E%20n
seems to work. (Didn't figure out how to copy that code on the phone)

I think you are right after trying on my own. termination_by f knows default identifiers for both implicit and explicit arguments. This is the better solution in my situation. Thanks!