Zulip Chat Archive

Stream: general

Topic: missing simp lemmas?


view this post on Zulip Johan Commelin (Feb 11 2019 at 09:05):

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]

view this post on Zulip Mario Carneiro (Feb 11 2019 at 09:05):

won't work

view this post on Zulip Mario Carneiro (Feb 11 2019 at 09:06):

If ring_hom becomes a type then these can be simp lemmas

view this post on Zulip Johan Commelin (Feb 11 2019 at 09:09):

Too bad...

view this post on Zulip Kevin Buzzard (Feb 11 2019 at 09:21):

You could make them typeclasses ;-)

view this post on Zulip Mario Carneiro (Feb 11 2019 at 09:26):

huh? it's already a typeclass

view this post on Zulip Wojciech Nawrocki (Feb 11 2019 at 16:40):

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

view this post on Zulip Kevin Buzzard (Feb 11 2019 at 16:43):

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

view this post on Zulip Reid Barton (Feb 11 2019 at 16:47):

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

view this post on Zulip Reid Barton (Feb 11 2019 at 16:47):

Here, f


Last updated: May 13 2021 at 05:21 UTC