Why is `coe_fn_coe_base` a `simp` lemma?

Stream: general

[Anne Baanen]

The library note function coercion points out that docs#coe_fn_coe_base is likely to cause simp loops, if you have a @[simp] lemma foo_hom.coe_coe (f : foo_hom A B) : ((f : bar_hom A B) : A → B) = (f : A → B). As a consequence, each foo_hom has to declare its own has_coe_to_fn instance.

I can't think of any types where we really want to have the double coercion as the simp normal form, so why is coe_fn_coe_base actually a simp lemma at all?

[Anne Baanen]

(I'm currently rebuilding mathlib with the simp attribute removed, no errors yet...)

[Gabriel Ebner]

EDIT: sorry wrong lemma

[Gabriel Ebner]

For everybody else who got confused, Anne wants to remove the ⇑x = ⇑↑x lemma.

[Eric Wieser]

Isn't the problem that the ⇑ on the LHS and RHS are different operations, and that the simp lemmas about say ring_hom will only be about the one that's defeq to ring_hom.has_coe_to_fun?

[Anne Baanen]

nevermind, sorry

[Anne Baanen]

If coe_fn_coe_base is actually used anywhere, that issue would be solved, but we'd have to deal with ⇑↑↑↑↑(f : alg_hom A B) as a simp-normal form. (Since we can go alg_hom -> ring_hom -> monoid_with_zero_hom -> monoid_hom -> mul_hom.)

[Anne Baanen]

I found a counterexample where coe_fn_coe_base is needed!

mathlib/src/topology/algebra/module.lean:1369:14: error: solve1 tactic failed, focused goal has not been solved
state:
R : Type u_1,
M : Type u_2,
M₂ : Type u_3,
_inst_1 : topological_space M,
_inst_2 : topological_space M₂,
_inst_3 : ring R,
_inst_4 : add_comm_group M,
_inst_5 : topological_add_group M,
_inst_6 : module R M,
_inst_7 : add_comm_group M₂,
_inst_8 : module R M₂,
e : M ≃L[R] M₂,
f : M →L[R] M₂,
F : units (M →L[R] M),
hF : ↑F = ↑(e.symm).comp f,
x : M
⊢ ⇑e (⇑F x) = ⇑f x

[Anne Baanen]

... and another instance of coe_fn (f : units _) in mathlib/src/analysis/calculus/fderiv.lean:2128

[Eric Wieser]

If ⇑↑↑↑↑f were the simp-normal form, then presumably we would no longer need ring_hom.map_mul as a simp lemma because ⇑↑(↑↑↑f) (x * y) would match mul_hom.map_mul (↑↑↑f) x y?

[Anne Baanen]

I think so, although it is quite probable it will then fail to match ⇑↑(↑↑↑f) 1with one_hom.map_one.

[Eric Wieser]

Oh good point, diamonds make that not a good idea at all

[Eric Wieser]

In addition to the pile of arrows already being not a good idea at all

[Anne Baanen]

Compilation finished. In summary I see:

• 2 simps that require adding coe_fn_coe_base
• 2 existing simp only [coe_fn_coe_base, ...]
• 2 existing rw ← coe_fn_coe_base
• 4 existing simp [-coe_fn_coe_base, ...]

[Eric Wieser]

Did you test what happens if you also remove the has_coe_to_fun instances?

[Anne Baanen]

Not yet

[Anne Baanen]

One example, in algebra/group/hom.lean is monoid_hom.comp: this fails (times out) if coe_fn_coe_base is @[simp] and there is no has_coe_to_fun instance for monoid_hom. Removing the simp attribute as well, makes it work again.

[Anne Baanen]

Because of diamonds we indeed have that only one of one_hom.map_one or mul_hom.map_mul gets matched with monoid_hom:

set_option trace.simplify.rewrite true

example [monoid M] [monoid N]
  (f : M →* N) (a b : M) : f (a * b) = f a * f b := by simp only [mul_hom.map_mul, coe_fn_coe_base]
-- works, `⇑f (a * b) ==> ⇑↑f (a * b) ==> ⇑↑f a * ⇑↑f b <== ⇑f a * ⇑f b`
example [monoid M] [monoid N]
  (f : M →* N) : f 1 = 1 := by simp only [one_hom.map_one, coe_fn_coe_base]
-- fails, `⇑↑f 1 = 1`

[Eric Wieser]

In your branch with both has_coe_to_fun on all but mul_hom / one_hom and coe_fn_coe_base removed, I assume?

[Eric Wieser]

In which case, it seems like coe_fn_coe_base is sort of a sanity check that users remembered to define the has_coe_to_fun to avoid that issue, even if it rarely comes up in actual use?

[Anne Baanen]

Shouldn't we leave these checks up to the linter, instead of having to diagnose it via simp timeouts? :P

[Eric Wieser]

Doesn't the presence of coe_fn_coe_base cause the simp linter to complain about downstream lemmas about types missing has_coe_to_fun?

[Eric Wieser]

Or does it cause the linter itself to timeout?

[Anne Baanen]

It causes simp calls to timeout if there are simp lemmas like docs#monoid_hom.to_mul_hom_coe that turn ⇑↑f back into ⇑f (in this case via ⇑(f.to_mul_hom).

[Anne Baanen]

I pushed 2 commits to GitHub if you want to check it out: https://github.com/leanprover-community/mathlib/commit/36ce6ed48233102677000c9ec42f6a31fc427892 and https://github.com/leanprover-community/mathlib/commit/38163b184a7e43dcc826a9d5cabfc672c7167a14

[Anne Baanen]

I looked into the build error if you remove the has_coe_to_fn instance, looks like simps doesn't realize that there still is a coercion to a function and starts generating lemmas of the form f.to_fun _ = _ instead of ⇑f _ = _.

[Anne Baanen]

Seems to be fixed when manually adding the projection, but I'm wondering why it's not found.

@[to_additive]
def monoid_hom.simps.to_fun {M N : Type*} [monoid M] [monoid N] : (M →* N) → M → N := coe_fn