missing simp lemmas?

Stream: general

[Johan Commelin]

Shouldn't these be simp lemmas?

namespace is_ring_hom
variables {β : Type v} [ring α] [ring β]
variables (f : α → β) [is_ring_hom f] {x y : α}

lemma map_zero : f 0 = 0 :=
calc f 0 = f (0 + 0) - f 0 : by rw [map_add f]; simp
     ... = 0 : by simp

lemma map_neg : f (-x) = -f x :=
calc f (-x) = f (-x + x) - f x : by rw [map_add f]; simp
        ... = -f x : by simp [map_zero f]

lemma map_sub : f (x - y) = f x - f y :=
by simp [map_add f, map_neg f]

[Mario Carneiro]

won't work

[Mario Carneiro]

If ring_hom becomes a type then these can be simp lemmas

[Johan Commelin]

Too bad...

[Kevin Buzzard]

You could make them typeclasses ;-)

[Mario Carneiro]

huh? it's already a typeclass

[Wojciech Nawrocki]

Why wouldn't this work? Can simp not match a type class when looking up lemmas?

[Kevin Buzzard]

I mean map_zero_class etc :-) Then type class inference could do it, right?

[Reid Barton]

It can't match a rule where the left-hand side is the application of a variable function. Or so I've gathered.

[Reid Barton]

Here, f