[Merged by Bors] - feat(pfun/recursion): unbounded recursion

[cipher1024]

---

This is a simplification of #1086. The proof automation is removed.

Todo:

• run #list_unused_decls
• add copyright comments
• add module header
• run #lint

[digama0]

Reminder: please don't force-push PRs once they have been publicly submitted.

[cipher1024]

Reminder: please don't force-push PRs once they have been publicly submitted.

Why is this an issue?

[digama0]

It breaks review comments - they point to outdated and removed commits, which is very confusing for later readers.

[cipher1024]

There's one thing I'd like your opinion on. What do you think of using continuous and monotone bundled with the function they relate to throughout this API?

[digama0]

I would say, avoid partial functions (using hypotheses in Prop as arguments to functions in Type). First, make sure you don't have any unused arguments, but if you need the argument, either totalize by returning a garbage value, or if that's not possible then package the hypothesis into the domain by bundling. I see a few definitions in this PR that deserve this treatment. pfun.fix should not require monotonicity, but you can have a pfun.fix' if you need. I see theorems with proofs in the statement of the lemma; they should use bundling or totalizing to get that out of there.

In short, I think it's a good idea, although possibly not the only solution to your problem.

[digama0]

@cipher1024 I made some changes directly to the branch; please look over them and make sure I haven't done anything too damaging for your later work. The main highlights are:

• nat.up has been renamed nat.upto, as well as the file it was in
• category.Preorder was split from preorder_hom, which allowed most of the order.category.omega_CPO file to go into order.omega_CPO
• The lawful_fix file has split from fix, separating the stuff that needs CPOs from the rest

Along with that there are a lot of small tweaks to documentation comments and proofs which shouldn't be too important.

Assuming everything is to your liking, I think we're ready to merge.

bors d+

[bors]

✌️ cipher1024 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[cipher1024]

@digama0 I like the edits. Thanks for taking the time.

[cipher1024]

bors r+

[bors]

Build failed:

• Build mathlib

[cipher1024]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests