Zulip Chat Archive

Stream: maths

Topic: ring tactic with homomorphism


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 15:03):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 15:07):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 30 2018 at 17:07):

Aaah, I see. Yes, that is true.

view this post on Zulip 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