## Stream: maths

### Topic: sub_eq_sub_of_sub_eq_sub

#### Kevin Buzzard (Feb 04 2019 at 12:40):

example (α : Type*) [add_comm_group α] (a b c d : α) : a - b = c - d → a - c = b - d :=
sorry


abel turns this into a + gsmul (-1) b = c + gsmul (-1) d → a + gsmul (-1) c = b + gsmul (-1) d.

I can solve these things, e.g.

example (α : Type*) [add_comm_group α] (a b c d : α) : a - b = c - d → a - c = b - d :=
λ h, by rw (eq_add_of_sub_eq h); simp


and I can even PR these things to mathlib if there is a need, but I am not sure whether this is the right thing to do. Is there automation which can solve these goals? Should I just be proving them as I need them in the middle of goals? Is the result there already?

#### Kenny Lau (Feb 04 2019 at 12:43):

so we're looking at the free Z-module <a,b,c,d> and asking whether (a-c)-(b-d) is in the submodule generated by (a-b)-(c-d) or something like that?

#### Kenny Lau (Feb 04 2019 at 12:43):

is there some normal form of Z matrices that might solve this?

#### Kevin Buzzard (Feb 04 2019 at 12:43):

Right, this is the problem.

#### Kenny Lau (Feb 04 2019 at 12:43):

Smith normal form?

#### Kevin Buzzard (Feb 04 2019 at 12:43):

I would not expect ring to solve this because it's not "this is an identity in all commutative rings", it's "this element is in this ideal"

sure

#### Kevin Buzzard (Feb 04 2019 at 12:44):

So for rings we need Groebner bases, which we don't have, and would be a substantial project to write.

#### Kevin Buzzard (Feb 04 2019 at 12:44):

But for abelian groups I thought there was a chance it was easier / already there.

#### Kenny Lau (Feb 04 2019 at 12:45):

and this isn't "this element is in this ideal", it's "this element is in this submodule"

#### Kenny Lau (Feb 04 2019 at 12:45):

our problem is linear

exactly

#### Kevin Buzzard (Feb 04 2019 at 12:45):

No doubt the tactic I want has a name and is already in Coq.

#### Kenny Lau (Feb 04 2019 at 12:46):

I think we need to buy Coq

#### Kevin Buzzard (Feb 04 2019 at 12:46):

I'm sure MS could buy it, I bet it's cheaper than Nokia

#### Kevin Buzzard (Feb 04 2019 at 12:47):

I think we need to port it.

#### Mario Carneiro (Feb 04 2019 at 12:47):

you only need to be a nationwide university to pay for it

#### Kevin Buzzard (Feb 04 2019 at 12:48):

But we also need the army of people whose job it is to port all the tactics

those cost extra

#### Kenny Lau (Feb 04 2019 at 12:48):

I think we need to convince Elon Musk to do something

#### Mario Carneiro (Feb 04 2019 at 12:49):

For this theorem, sure you can add it if it's useful. I'd make it a biconditional

#### Kenny Lau (Feb 04 2019 at 12:49):

(and add @[simp])

lolno

#### Mario Carneiro (Feb 04 2019 at 12:50):

another one which might be useful (and we might already have) is a - b = c - d <-> a + d = b + c

#### Kevin Buzzard (Feb 04 2019 at 13:08):

<-> a + d = c + b <-> d + a = b + c <-> ...

#### Kevin Buzzard (Feb 04 2019 at 13:10):

I think we need to convince Elon Musk to do something

At AITP I'm going to try and get DeepMind interested. I don't know why they're focussing on medicine, we have to get the basics right first.

#### Mario Carneiro (Feb 04 2019 at 13:10):

I thought they were focusing on starcraft now

#### Kevin Buzzard (Feb 04 2019 at 13:11):

They finished that last week.

#### Kevin Buzzard (Feb 04 2019 at 13:12):

lol my proof doesn't port. I wanted r - ↑⌊r⌋ = s - ↑⌊s⌋ -> r - s = ↑⌊r⌋ - ↑⌊s⌋ but when I rewrite the r it goes in the floor too :-)

Last updated: May 18 2021 at 08:14 UTC