[Merged by Bors] - fix(algebra/ordered*): add norm_cast attribute

[kbuzzard]

---

A few with_top and with_bot coercion lemmas didn't have the norm_cast attribute. I added them.

Comments:

1. I went to the docs to read about which lemmas should be tagged, but the recent refactor which meant that everything should be tagged norm_cast also entailed a cleanup of the docs, so I was a bit in the dark as to exactly what I should be tagging. I went for an "if it moves, norm_cast it" approach on the basis that it would be easier for a reviewer to say "no, you don't tag that kind of lemma" than for a reviewer to say "you missed this one, 100 lines up".

2. The norm_cast attribute was not available in order.bounded_lattice so I just add the attribute to the coe lemmas from that file in the ordered_group file, where the attribute was available. This can't be the right answer. But again I took the approach that it was better to do the wrong thing than just ignore the problem completely and then forget about it.

3. coe_zero and coe_eq_zero were only written for canonically ordered rings or something -- I've changed it so that they apply to additive monoids. Why can't they just apply to with_zero? Is there a problem with defining a zero on with_top X to be the zero of X, whenever X has a zero?

[robertylewis]

These all look reasonable! Just suspicious of the two I've tagged, and any others that norm_cast can already prove. It's not necessarily a problem to tag them anyway, just not needed.

[robertylewis]

If this lemma is proved by norm_cast it probably shouldn't need to be tagged norm_cast itself. Does something fail without this? what norm_cast lemmas does it use? Are other lemmas in the file provable with norm_cast already?

[kbuzzard]

Answers: 1) Nothing seems to fail if I untag it 2) The only way I know how to answer this is with set_option trace.simplify.rewrite true, which tells me coe_eq_zero is proved using coe_zero. There must be more to it than this though; norm_cast is doing something simp isn't doing. 3) with_bot.coe_zero can be proved by norm_cast, using with_top.coe_zero (see below)

[robertylewis]

As above, the proof is already norm_cast.

[kbuzzard]

In fact norm_cast can even prove coe_zero -- it uses with_top proofs to prove with_bot theorems, presumably because the with_bot instances are defined using with_top instances rather than being redefined. I don't know if this is good or bad.

[gebner]

You probably want coe_bit0 and coe_bit1 as well, otherwise norm_cast doesn't work on numerals. (I hope I didn't miss them.)

[kbuzzard]

I added coe_bit0 and coe_bit1 for both with_bot and with_top. I am a bit confused about whether we even need these lemmas for with_bot. I don't know if they're good simp lemmas, and norm_cast can prove the with_bot lemmas using the with_top lemmas. I added them on the basis that the library should be complete, but I didn't tag the with anything. I tagged with_top.coe_add with simp and it broke the proof of add_eq_top [ordered_add_comm_monoid α] : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤. I figured who was to say which was simpler out of \u(a+b) and \u a + \u b -- sometimes you want to push coercions in and sometimes pull them out -- there's no obvious "go this way" route.

[robertylewis]

I'm afraid I was wrong when I wrote

If this lemma is proved by norm_cast it probably shouldn't need to be tagged norm_cast itself

because of norm_cast's special handling for numerals. I've reverted a few of the attributes you deleted, because I think they're actually not redundant. (I can construct examples that work only with the attribute.) The others, AFAICT, aren't needed.

There shouldn't be an issue importing norm_cast earlier, so I moved some of the attributions to bounded_lattice where they belong.

[robertylewis]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Run tests and docs
• Lint mathlib
• Build mathlib