fix(algebra/category): make has_coe_to_sort instances for bundled categories reducible

[semorrison]

See discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unbearable.20unhappiness.20of.20.60simp.60.20not.20working

I have added a library note explaining this issue, and put in two examples that ensure correct behaviour.

[gebner]

Should we add a linter for this?

[semorrison]

Should we add a linter for this?

... let's see if this is actually the right course before we invest that level of energy. :-)

[urkud]

Sorry, I'm very far from being an expert in reducibility & Lean... I remember that it caused problems when we did the refactoring of concrete categories, but I don't remember any details.

[gebner]

You've already written this in the "locally reducible category instances" library note:

It's especially important that the has_coe_to_sort instance not contain an extra id as we want the semiring ↥R instance to also apply to semiring R.α (it seems to be impractical to guarantee that we always access R.α through the coercion rather than directly).

This here is exactly the issue we're having with (0 : R) = (0 : R.α) not being true modulo reducible definitional equality, and hence simp failing to apply obvious lemmas. So I think the change in this PR is the right way to go and also consistent with the existing design.

Another reason to make the has_coe_to_sort instances reducible is if we ever want to apply the category theory library to actual structures. For examples, if you had an element of the bundled integers x : IntRing, then you'd want to use it as an element of the unbundled integers x : ℤ without the simplifier complaining (i.e. ↥IntRing should be reducibly-definitionally equal to ℤ).

[gebner]

BTW, another option that works is:

instance : concrete_category SemiRing :=
(by apply_instance : concrete_category (bundled semiring))

[rwbarton]

Should we add a linter for this?

What would the linter do? Check that all has_coe_to_sort instances are reducible? Why stop there?

[gebner]

What would the linter do? Check that all has_coe_to_sort instances are reducible?

Since that is the most common problem here, yes.

Why stop there?

What else would you want to check?

[rwbarton]

How about that all definitions are reducible? That would solve even more problems with simp, right? :)

I think this change is okay but I'm not convinced we are fixing the right problem at the right level. Historically in category theory (e.g. with comp_id) we tended to accept that simp just doesn't do all the things one would want, rather than trying to force the issue by marking a lot of things reducible.

[gebner]

How about that all definitions are reducible? That would solve even more problems with simp, right? :)

This is a good question. Marking some definitions as reducible can actually be counter-productive. For example, simp lemmas such as f ∘ symm f = id don't work (reliably) because (∘) is reducible. Then f ∘ symm f unfolds to λ x, f (symm f x) and you suddenly need higher-order matching.

Another reason is that a definition might unfold to something "more complex". We can probably write reliable simplification lemmas for the simple definition. But this becomes much harder once it is unfolded and perhaps simplified so that it no longer matches the original definition.

I don't think the instances in this PR are problematic in this sense.

Historically in category theory (e.g. with comp_id) we tended to accept that simp just doesn't do all the things one would want

I believe it is worthwhile to make simp work.

but I'm not convinced we are fixing the right problem at the right level

I think the approach of marking definitions as reducible is the common solution to this kind of problem. If you want the simplifier to unfold a definition during matching, then you typically mark it as reducible.

I also thought about adding this simp lemma (and fixing bundled.map so that it uses R instead of R.α):

@[simp]
lemma bundled.α_eq_coe (c) (R : bundled c) : R.α = R := rfl

Alas, this doesn't work because the simplifier cannot rewrite the α in has_zero.zero α. This is because α occurs in the return type of has_zero.zero, and the simplifier can only do rewrites that preserve the type of an expression.

[semorrison]

Just noting that in Lean 3.8 we should be able to reverse this change. #169 there solves this problem.