## Stream: maths

### Topic: ring tactic with homomorphism

#### Johan Commelin (Apr 30 2018 at 12:53):

Consider the following MWE

import tactic.ring
import data.real.basic

open real

def f : ℤ → ℝ := λ x, (x : ℝ)

example (n : ℝ) : (n + 3) * (n + 4) = n * n + 10 + 7 * n + 2
:= by ring

example (n : ℤ) : f (n + 3) * f (n + 4) = (f n) * (f n) + 10 + 7 * (f n) + f 2
:= by ring -- fails


#### Johan Commelin (Apr 30 2018 at 12:53):

How hard would it be to teach the ring tactic to use the axioms for ring homomorphisms?

#### Kevin Buzzard (Apr 30 2018 at 15:03):

You could start by making f part of the is_ring_hom class.

#### Kevin Buzzard (Apr 30 2018 at 15:05):

instance f_is_a_ring_hom : is_ring_hom f := { map_add := sorry,map_mul := sorry,map_one := sorry} is how to start

#### Kevin Buzzard (Apr 30 2018 at 15:06):

and then you need to fill in the proofs, which are all already there, with names I can't quite remember yet, hang on.

#### Kevin Buzzard (Apr 30 2018 at 15:07):

They are probably called things like cast_mul, cast_add and cast_one.

#### Chris Hughes (Apr 30 2018 at 16:10):

I think the difficult part is getting ring to recognize f 2 + f3 = f 5. Apart from the problem with literals you can just simp[is_ring_hom.map_add] etc first.

#### Johan Commelin (Apr 30 2018 at 17:04):

@Kevin Buzzard Right..., so maybe instead of defining f, I should actually just assume that it is a ring hom. Maybe Lean should be able to deduce itself that this determines f completely!

#### Johan Commelin (Apr 30 2018 at 17:04):

@Chris Hughes Yes, I understand. But I really want Lean to deal with these things using only one straightforward tactic. After all, it is one of these “mathematically trivial” steps.

#### Chris Hughes (Apr 30 2018 at 17:05):

I'm saying that it should be easy to add it to the ring tactic, if all it requires is a simp in the definition of ring

#### Johan Commelin (Apr 30 2018 at 17:07):

Aaah, I see. Yes, that is true.

#### Mario Carneiro (May 01 2018 at 00:05):

I'm not so sure about adding this to ring. This is outside the scope of ring as I see it, which is to solve equations in the first order theory of rings. If you want something like this it should be a different tactic; as Chris says it may be as simple as just simp with an appropriate simp set followed by ring.

Last updated: May 11 2021 at 16:22 UTC