ring tactic with homomorphism

Stream: maths

[Johan Commelin]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Chris Hughes]

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]

@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]

@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]

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]

Aaah, I see. Yes, that is true.

[Mario Carneiro]

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.