Zulip Chat Archive

Stream: general

Topic: tactic.ring feature requests


Kevin Buzzard (Mar 29 2018 at 12:03):

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 (Mar 29 2018 at 12:04):

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 (Mar 29 2018 at 12:04):

or whether I should just expect ring to deal with these

Kevin Buzzard (Mar 29 2018 at 12:04):

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

Kevin Buzzard (Mar 29 2018 at 12:05):

@Mario Carneiro

Kevin Buzzard (Mar 29 2018 at 14:36):

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 (Mar 29 2018 at 14:36):

Why can't this just be by ring?

Kevin Buzzard (Mar 29 2018 at 14:39):

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?


Last updated: Dec 20 2023 at 11:08 UTC