linarith for ordered_add_comm_group

Stream: general

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Rob Lewis]

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

[Rob Lewis]

No, it's failing before preprocessing even.

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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

[Rob Lewis]

It's a reasonable generalization though.

[Reid Barton]

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

[Rob Lewis]

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]

abel is the second part, right?

[Rob Lewis]

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]

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]

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

[Rob Lewis]

Does it handle nat multiplication?

[Reid Barton]

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]

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]

abel should be able to handle multiplication by constants

[Kevin Buzzard]

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

[Scott Morrison]

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