[Merged by Bors] - refactor(analysis/asymptotics): make is_o irreducible

[sgouezel]

is_o is currently not irreducible. Since it is a complicated type, Lean can have trouble checking if two types with is_o are defeq or not, leading to timeouts as described in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/undergraduate.20calculus/near/193776607
This PR makes is_o irreducible.

TO CONTRIBUTORS:

Please include a summary of the changes made in this PR above "TO CONTRIBUTORS:", as that text will become the commit message. You are also encouraged to append the following co-authorship template if you'd like to acknowledge suggestions / commits made by other users:

Co-authored-by: name name@example.com

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in the tactic doc entries
  • write an example of use of the new feature in test/tactics.lean or another test file
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

If you're confused by comments on your PR like bors r+ or bors d+, please see our notes on bors for information on our merging workflow.

[rwbarton]

This looks simple enough, but given that is_o is a Prop (and not a function, say), another, "less magical" approach could be to turn it into a structure instead of a def; have you considered this?

[sgouezel]

I don't see the advantage of the structure over the irreducibility. In some situations, Lean might want to see into the structure to see if two is_o things are equal, and then it would face the same problem as before, so it seems to me that irreducibility is safer.

[semorrison]

LGTM

[PatrickMassot]

@avigad I think you wrote that definition, do you have any comment?

[avigad]

It looks good to me. Lean shouldn't be unfolding is_o: everything should depend on the interface for reasoning with it, not the internal definition. So I see no harm in sealing it off.

[jcommelin]

LGTM

[gebner]

In some situations, Lean might want to see into the structure to see if two is_o things are equal, [...]

This is not the case. If is_o is a structure then Lean can't unfold is_o .... at all. This is exactly the same situation as with irreducible.

[sgouezel]

OK, thanks for the clarification. Is there any advantage of a structure over the irreducible attribute, or are they really equivalent? The advantage I can see in not having a structure is that in the whole file developing asymptotics we use a lot the definition of is_o, and we only turn on the attribute at the end of the file.

[rwbarton]

structure just seems conceptually simpler--for example it means the elaborator and the kernel agree on what things are definitionally equal. Using irreducible seems like more of a hack. I don't have any concrete advantages, though.

[urkud]

I have two comments.

1. You make is_O_with and is_o irreducible but is_O is still reducible. Is it intentional?
2. Could you please add lemmas like is_o.def to unfold definitions without rw? Probably with main versions returning eventually and primed versions returning is_O_with.

[sgouezel]

1 - Yes, it was intentional to leave is_O reducible, as I am under the impression that sigma types create less difficulty for Lean than pi types. Still, as I don't like inconsistencies, I have also made it irreducible.

2 - I have added a few lemmas in the direction you are indicating. Maybe these are not exactly the statements you would like -- I would say this can be changed later, when you play with is_o and is_O and get a feel for what is missing.

[jcommelin]

I agree. Let's just try this out.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib