rw_mod_hom

Stream: general

[Johan Commelin]

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]

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

[Kenny Lau]

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

[Johan Commelin]

Right, which is really ugly in

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

[Johan Commelin]

So I would like an abbreviating tactic (-;

[Kenny Lau]

as in,

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

Can we extend norm_cast to other homs?

[Gabriel Ebner]

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]

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