Shorthand definitions

Stream: general

[Wouter Smeenk]

I am trying to define a structure where I have 4 parameters (x y u v). I then want to define row1 and col1 based on those parameters. But in order to do this properly I need some shorthands in order to define those (p q r s and a to i). Is there a easier way to do this? I currently have this but it seems very cumbersome:

import Mathlib

namespace MagicSquares

structure PolyParams where
  x : ℤ
  y : ℤ
  u : ℤ
  v : ℤ

namespace PolyParams

@[simp] def p := u * x - v * y
@[simp] def q := u * y + v * x
@[simp] def r := u * y - v * x
@[simp] def s := u * x + v * y

@[simp] def e := (x^2 + y^2) * (u^2 + v^2)

@[simp] def b := (r * q + s * p) - (r * p - s * q)
@[simp] def h := (r * q + s * p) + (r * p - s * q)

-- TODO define rest of definitions properly
@[simp] def i := r
@[simp] def a := r

@[simp] def d := r
@[simp] def f := r

@[simp] def g := r
@[simp] def c := r

end PolyParams

structure Poly extends PolyParams where
  row1 : toPolyParams.a + toPolyParams.b + toPolyParams.c = 3 * toPolyParams.e
  col1 : toPolyParams.a + toPolyParams.d + toPolyParams.g = 3 * toPolyParams.e

[Eric Wieser]

This is an interesting question, but I suspect those definitions are not working in the way you expect them to

[Eric Wieser]

(fortunately I think they end up as what you wanted anyway, but not necessarily for the reason you expect)

[Wouter Smeenk]

How do you think they are working?

[Aaron Liu]

You are defining them by adding functions, which adds them pointwise

[Eric Wieser]

Indeed: the + in your definitions is not addition over the integers

[Wouter Smeenk]

Oke, that is indeed not ideal. What would be a better way to define it? Also is there a way to do this in one structure instead of splitting it over two?

[Eric Wieser]

Splitting structures like this is a pretty reasonable approach