Help with abbreviation / local notation

Stream: new members

[Manoj Kummini]

How does one use abbreviation or local notation correctly? In the following code, if I use abbreviation, I get an error saying that f is noncomputable, so I added the line noncomputable theory. When I used local notation, I get an unknown idenfier error. (I have added these errors as comments within the code.)

Additionally, the ring tactic gets a timeout and the ring_exp tactic does not solve the goal.

import data.mv_polynomial.basic
import data.mv_polynomial.comm_ring
import data.zmod.basic

open mv_polynomial
--noncomputable theory

section

abbreviation R := mv_polynomial (fin 6) (zmod 101)
abbreviation f : R  := (X 0)*(X 1)*(X 2) - (X 3)*(X 4)*(X 5)
abbreviation g : R  := (X 0)*(X 1)*(X 2)
abbreviation h : R  := (X 3)*(X 4)*(X 5)
-- local notation h : R  := (X 3)*(X 4)*(X 5)

#check R
#check f
#check g
#check h

lemma g_minus_h_eq_f : g - h = f :=
begin
  -- ring_exp,
  ring,
end
-- gives deterministic timeout (whether or not 'noncomputable theory' is used.)
-- with local notation gives "unknown identifier 'h'"
-- ring_exp only rewrites it as g + (-h)

#check g_minus_h_eq_f
   -- g - h = f
   -- correctly

lemma g_eq_h_plus_f : g = h + f :=
begin
  ring,
end
-- gives deterministic timeout

lemma g_eq_h_plus_f_one : g = (1:R)*h + (1:R)*f :=
begin
  ring_exp,
end
-- tactic failed.

I need to show that g *(X 0) belongs to the ideal, for which it is easy to show that h *(X 0) does, so I am trying to prove a lemma that g-h is in the ideal.

[Yakov Pechersky]

import data.mv_polynomial.basic
import data.mv_polynomial.comm_ring
import data.zmod.basic

open mv_polynomial
noncomputable theory

section

abbreviation R := mv_polynomial (fin 6) (zmod 101)
def f : R  := (X 0)*(X 1)*(X 2) - (X 3)*(X 4)*(X 5)
def g : R  := (X 0)*(X 1)*(X 2)
def h : R  := (X 3)*(X 4)*(X 5)

lemma g_minus_h_eq_f : g - h = f := rfl

lemma g_eq_h_plus_f : g = h + f :=
begin
  rw [f, g, h],
  ring
end

lemma g_eq_h_plus_f_one : g = (1:R)*h + (1:R)*f :=
begin
  rw [f, g, h],
  ring
end

end

[Yakov Pechersky]

I used def instead. I don't think ring sees through abbreviation.

[Manoj Kummini]

Thank you.