sub_eq_sub_of_sub_eq_sub

Stream: maths

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

Right, this is the problem.

[Kenny Lau]

Smith normal form?

[Kevin Buzzard]

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"

[Kenny Lau]

sure

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

our problem is linear

[Kevin Buzzard]

exactly

[Kevin Buzzard]

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

[Kenny Lau]

I think we need to buy Coq

[Kevin Buzzard]

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

[Kevin Buzzard]

I think we need to port it.

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

those cost extra

[Kenny Lau]

I think we need to convince Elon Musk to do something

[Mario Carneiro]

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

[Kenny Lau]

(and add @[simp])

[Mario Carneiro]

lolno

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

I thought they were focusing on starcraft now

[Kevin Buzzard]

They finished that last week.

[Kevin Buzzard]

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 :-)