Ring for vector spaces

Stream: Is there code for X?

[Patrick Johnstone]

I use ring a lot as in

example (x y z: ℝ)
        : x + y + z = x + (y + z)
        :=
begin
  ring,
end

But if I try

example (x y z: euclidean_space ℝ (fin 10))
        : x + y + z = x + (y + z)
        :=
begin
  ring,
end

ring fails. Is there a way to get ring to work for Euclidean space vectors?

[Eric Rodriguez]

Does abelwork?

[Alex J. Best]

What ring structure would you want on the euclidean space? I doubt that instance is defined in mathlib.

[Yaël Dillies]

Maybe you just want pointwise addition/multiplication? In that case, you should use fin 10 → ℝ.

[Patrick Johnstone]

abel works thanks

[Patrick Johnstone]

OK next question (related). How about linarith?

example (x y z w : ℝ) (h : x+y=z+w)
  : z-x=y-w
  := by linarith

Works.

example (x y z w : euclidean_space ℝ (fin 10)) (h : x+y=z+w)
  : z-x=y-w
  := by linarith

Fails.

[Heather Macbeth]

See a message I just wrote in another stream, replacing ring with abel

[Heather Macbeth]

Essentially, figure out for yourself the coefficients linarith would have used:

import analysis.inner_product_space.pi_L2

example (x y z w : euclidean_space ℝ (fin 10)) (h : x + y = z + w) :
  z - x = y - w :=
begin
  rw ← sub_eq_zero at h ⊢,
  have h' := congr_arg (λ x, -x) h,
  convert h';
  abel,
end

[Heather Macbeth]

By the way, do you really need to be working with euclidean_space? You might find you have fewer distracting details if you assume {x y z w : V} where

variables {V : Type*} [inner_product_space ℝ V]

[Patrick Johnstone]

That's OK but seems more low-level than I was hoping for. Does Linarith just not work unless it's basically the reals or some similar "ordered field"?

[Patrick Johnstone]

Also why do you need to use ";" after convert?

[Heather Macbeth]

Patrick Johnstone said:

Also why do you need to use ";" after convert?

In this case you probably don't, but it makes the technique more general (it allows it to work for a system of 10 equations rather than just one).

[Heather Macbeth]

Patrick Johnstone said:

Does Linarith just not work unless it's basically the reals or some similar "ordered field"?

Right, I think it's ordered commutative semirings.

[Patrick Johnstone]

Is the problem with eucliean_space \R (fin 10) for linarith that it is not "totally ordered"?

[Heather Macbeth]

It sure isn't!

[Patrick Johnstone]

Ok and there isn't a linarith for equalities only? That doesn't need the commutative semiring to be ordered? That would seem to simplify things only trying to prove equalities.

[Heather Macbeth]

Please read the thread I linked above. Basically you're asking a for a "Grobner basis tactic", which doesn't exist currently in Lean, but which you can approximate by providing the coefficients yourself -- I indicated an efficient syntax for doing this.