crec

Stream: general

[Reid Barton]

I wrote a version of well-founded recursion which allows you to maintain a "consistency" condition in the recursion.
https://gist.github.com/rwbarton/7bd5b3b19d930f577355a596a5ed8b4d

[Reid Barton]

Compared to well_founded.fix, the difference is that you get to specify a condition q : Π ⦃i j⦄ (h : i < j), C i → C j → Prop. In the induction step you can assume that all the previous choices are consistent according to q, and you need to produce a new value which is consistent with all the previous choices.

[Reid Barton]

In the end, you get a function whose values are all consistent according to q

[Reid Barton]

Mostly it's useful when you need to have the consistency condition in hand in order to perform the next step of the recursive construction.

[Reid Barton]

For example, you could take C n to be sequences defined up to n, and q to say that the first sequence is a prefix of the second

[Reid Barton]

For example, suppose you want to construct an order-preserving map from nat to an order P without a greatest element. It's easy to prove by induction on n that there is an order-preserving map from fin n to P, but this is not good enough if these maps are all unrelated!

[Mario Carneiro]

I think this could be stated as a "dependent choice" problem

[Mario Carneiro]

you want the definition of F a to depend on F b for all b < a

[Mario Carneiro]

ah, nevermind, I don't think I can simplify it past what you've already done. You want to define the type and value together in the recursion, but that's what crec_core accomplishes

[Mario Carneiro]

You can probably remove the i < j from q, since it's defining a prop

[Mario Carneiro]

the f parameter of H can be uncurried, I don't know whether it is better or worse to also split it up into two parameters for the subtype in the target

[Reid Barton]

Thanks for the suggestions. I haven't tried actually using this for anything yet, so I'll have to see what seems more natural at the use site.

[Johannes Hölzl]

@Reid Barton can I add crec to mathlib?

[Reid Barton]

Yes, absolutely.
https://github.com/rwbarton/lean-model-categories/blob/top-dev/src/logic/crec.lean is the version I actually use at the moment.
I think the usability could still be improved; in particular it's not very convenient to use crec and crec_consistent separately because you typically have to repeat q, which could be rather complicated.

[Reid Barton]

crec' was an attempt to improve on that, but I still haven't found the best way to use it, for example https://github.com/rwbarton/lean-model-categories/blob/top-dev/src/top_small.lean#L110-L137 is a bit awkward.

[Reid Barton]

Bhavik Mehta said:

Okay, where should it go? And can someone help me document it?

One reason I've been dragging my feet on crec in particular is that I feel there's some better version of it that wants to come out, maybe involving tactic support, I'm not sure. For example, https://github.com/guillaumebrunerie/initiality uses the same pattern but on a much larger scale--of course one could translate it as-is into Lean, but is there a place for crec (as-is) or some other kind of structure here? crec also doesn't do a very good job of solving the problem it was originally conceived for (it reduced it to something tractable, but far from elegant).

[Reid Barton]

But, I guess we can just add it is for now, and worry about all that later.