tactic.ring feature requests

Stream: general

[Kevin Buzzard]

import tactic.ring
theorem  inductive_step (d : ℕ) : d ^ 2  + (2  * d +  1) = (succ d) ^ 2  :=
begin
-- ring doesn't work
unfold nat.pow,
-- ring doesn't work
rw succ_eq_add_one,
ring, -- works
end

[Kevin Buzzard]

I am in two minds about whether I need to tell mathematicians "obviously you need to unfold nat.pow and succ because they are not really to do with rings, which are all about + and *"

[Kevin Buzzard]

or whether I should just expect ring to deal with these

[Kevin Buzzard]

or whether it's even not possible to get ring to deal with these, for technical reasons I'm unaware of

[Kevin Buzzard]

@Mario Carneiro

[Kevin Buzzard]

import tactic.ring
open nat

def  odd : ℕ → ℕ :=  λ i, 2  * i +  1
def  square : ℕ → ℕ :=  λ i, i ^ 2

theorem  odd_square_inductive_step (d : ℕ) : square d + odd d = square (succ d)
:=  by {unfold square odd nat.pow,rw succ_eq_add_one,ring}

[Kevin Buzzard]

Why can't this just be by ring?

[Kevin Buzzard]

Can't I promise that I'll only ever call ring with an identity that can be formulated using only the axioms of a semiring?