Zulip Chat Archive

Stream: maths

Topic: sub_eq_sub_of_sub_eq_sub


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Feb 04 2019 at 12:43):

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

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 12:43):

Right, this is the problem.

view this post on Zulip Kenny Lau (Feb 04 2019 at 12:43):

Smith normal form?

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Feb 04 2019 at 12:44):

sure

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 12:44):

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

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Feb 04 2019 at 12:45):

our problem is linear

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 12:45):

exactly

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 12:45):

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

view this post on Zulip Kenny Lau (Feb 04 2019 at 12:46):

I think we need to buy Coq

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 12:46):

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

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 12:47):

I think we need to port it.

view this post on Zulip Mario Carneiro (Feb 04 2019 at 12:47):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 04 2019 at 12:48):

those cost extra

view this post on Zulip Kenny Lau (Feb 04 2019 at 12:48):

I think we need to convince Elon Musk to do something

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 04 2019 at 12:49):

(and add @[simp])

view this post on Zulip Mario Carneiro (Feb 04 2019 at 12:49):

lolno

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 13:08):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 04 2019 at 13:10):

I thought they were focusing on starcraft now

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 13:11):

They finished that last week.

view this post on Zulip 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