## Stream: general

### Topic: rw_mod_hom

#### Johan Commelin (May 09 2020 at 16:27):

If I have a ring hom f : R →+* S, and a hypothesis h : f x = f y, and somewhere in my goal I have f (a + x + b), then I would love to be able to write rw_mod_hom h, and get f (a + y + b) as a result.

#### Johan Commelin (May 09 2020 at 16:28):

Bonus points if h : f x = f y + f z and rw_mod_hom h would generate f (a + (y + z) + b).

#### Kenny Lau (May 09 2020 at 16:29):

simp only [ring_hom.map_add, etc]; simp only *; simp only [(ring_hom.map_add _ _).symm, etc]

#### Johan Commelin (May 09 2020 at 16:30):

Right, which is really ugly in

calc LHS = RHS1 : by short_tactic_argument
... = RHS2 : by another_short_tac


#### Johan Commelin (May 09 2020 at 16:30):

So I would like an abbreviating tactic (-;

#### Kenny Lau (May 09 2020 at 16:30):

as in,

meta def rw_mod_hom : tactic unit :=
{what i wrote above}


#### Johan Commelin (May 09 2020 at 16:31):

Probably yes. Plus support for rewriting at hypothesis etc etc...

#### Johan Commelin (May 09 2020 at 16:31):

Not saying this is hard. Just that it's nice to have (-;

#### Johan Commelin (May 09 2020 at 16:33):

Something that is (probably very) nontrivial would be

calc_mod_hom [f]
a + x + b = a + (y + z) + b : by rw h
... = a + more        : by tac


#### Chris Hughes (May 09 2020 at 18:10):

Can we extend norm_cast to other homs?

#### Gabriel Ebner (May 09 2020 at 18:13):

I think some basic support for other kinds of "coercions" would be straightforward. We already support three coercions: coe_fn, coe_sort, and coe. We could add an attribute that allows you to register other functions as coercions. However the heuristic for ↑x = ↑y which first tries to rewrite it to ↑↑x = ↑y is probably hard to generalize to other coercions.

#### Yury G. Kudryashov (May 10 2020 at 01:51):

In case of homomorphisms it's one of several coe_fn's.

Last updated: May 16 2021 at 05:21 UTC