Zulip Chat Archive

Stream: general

Topic: linarith for ordered_add_comm_group


view this post on Zulip Reid Barton (Sep 03 2020 at 15:21):

How hard would it be to extend linarith to handle ordered_add_comm_group?

import tactic.linarith

variables {R : Type*}

example [linear_ordered_comm_ring R] (r : R) : r  r := by linarith   -- ✓
example [linear_ordered_comm_ring R] (r : R) : r = r := by linarith   -- ✓

example [ordered_add_comm_group R] (r : R) : r  r := by linarith
/-
error: invalid type ascription, term has type
  ?m_3 ≤ ?m_4
but is expected to have type
  r ≤ r
state:
R : Type u_1,
_inst_1 : ordered_add_comm_group R,
r : R
⊢ r ≤ r
-/

example [ordered_add_comm_group R] (r : R) : r = r := by linarith
/-
error: invalid apply tactic, failed to synthesize type class instance
state:
R : Type u_1,
_inst_1 : ordered_add_comm_group R,
r : R
⊢ r = r
-/

view this post on Zulip Reid Barton (Sep 03 2020 at 15:21):

The documentation does claim it needs linear_ordered_comm_ring, though I didn't find any other occurrences of even comm_ring under tactic.linarith.*.

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:33):

By default linarith calls ring for verification. There's an option to plug in an alternate verifier so you might be able to get around that. But it also sets up the problem for the verifier using mul, not smul, which is a more disruptive change.

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:33):

I think the error you're seeing is probably just an artifact but it will hit real trouble at the verification stage.

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:34):

Oh, or maybe not, that error could be coming from when it builds the problem for the verifier.

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:36):

No, it's failing before preprocessing even.

view this post on Zulip Reid Barton (Sep 03 2020 at 15:41):

so I'm guessing the answer is "not that easy"?

view this post on Zulip Reid Barton (Sep 03 2020 at 15:42):

I only need it for 4 very easy problems but it would be nice to do all of them in a single line

view this post on Zulip Reid Barton (Sep 03 2020 at 15:43):

or more precisely, I only have 4 easy problems to take care of but it would be nice if I could do all of them in a single line.

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:44):

In this case it's failing at apply le_of_not_gt since an ordered_add_comm_group isn't a linear order.

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:44):

It's certainly much harder than doing your four easy problems separately ;)

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:45):

It's a reasonable generalization though.

view this post on Zulip Reid Barton (Sep 03 2020 at 15:45):

oh whoops. Actually my orders are linear too, but now things are getting complicated

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:48):

I think the minimum you need for linarith should be a linear_ordered_add_comm_gorup and an efficient tactic for normalizing things in this structure that understands scalar multiplication by nats.

view this post on Zulip Reid Barton (Sep 03 2020 at 15:50):

abel is the second part, right?

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:53):

Then you need to make sure all the lemmas it uses are satisfied by this type class, change the parsing stage to read smul, change the verification step to generate something using smul, ...

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:54):

linarith will identify atoms up to ring equivalence right now, so you'll lose that if you go purely to groups, which means you might have to check if the target type is a ring and pick a strategy based on that.

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:55):

I'm not really sure how the power/efficiency of abel compares to ring, to be honest.

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:55):

Does it handle nat multiplication?

view this post on Zulip Reid Barton (Sep 03 2020 at 15:56):

well, I took a quick look at the source and it contained things like nsmul and gsmul so I'm guessing it does

view this post on Zulip Rob Lewis (Sep 03 2020 at 15:59):

Okay. So my point is, it's doable, but medium effort and I won't be able to do it myself any time soon. But I'm willing to review a PR!

view this post on Zulip Mario Carneiro (Sep 03 2020 at 16:17):

abel should be able to handle multiplication by constants

view this post on Zulip Kevin Buzzard (Sep 03 2020 at 22:41):

abel should be able to handle comm_groups and not just add_comm_groups!

view this post on Zulip Scott Morrison (Sep 03 2020 at 22:53):

Just to be clear here: when Mario says "should" in 'abel should be able to handle multiplication by constants' he means "does", while when Kevin says "should" in 'abel should be able to handle comm_groups' he means "wouldn't it be nice if".


Last updated: May 08 2021 at 03:17 UTC