## Stream: general

#### 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,
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,
r : R
⊢ r = r
-/


#### 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.*.

#### 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.

#### 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.

#### 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.

#### Rob Lewis (Sep 03 2020 at 15:36):

No, it's failing before preprocessing even.

#### Reid Barton (Sep 03 2020 at 15:41):

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

#### 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

#### 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.

#### 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.

#### Rob Lewis (Sep 03 2020 at 15:44):

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

#### Rob Lewis (Sep 03 2020 at 15:45):

It's a reasonable generalization though.

#### Reid Barton (Sep 03 2020 at 15:45):

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

#### 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.

#### Reid Barton (Sep 03 2020 at 15:50):

abel is the second part, right?

#### 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, ...

#### 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.

#### 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.

#### Rob Lewis (Sep 03 2020 at 15:55):

Does it handle nat multiplication?

#### 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

#### 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!

#### Mario Carneiro (Sep 03 2020 at 16:17):

abel should be able to handle multiplication by constants

#### Kevin Buzzard (Sep 03 2020 at 22:41):

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

#### 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