Using linarith with my own class

Stream: maths

[Gihan Marasingha]

For teaching real numbers to my first-year undergraduates, I've written a class that contains the real number axioms and have used this to prove all the necessary basic results (x*0 = 0, no zero-divisors, uniqueness of supremum, the Archimedean property, etc.). I'd like to use this class for developing further facts (e.g. existence of square root of 2, results on convergence of sequences), but I can see this will be painful without linarith.

What do I need to do to use linarith with my own class?

[Rob Lewis]

You probably need an instance from your class to comm_ring.

[Shing Tak Lam]

The tactic docs seem to suggest you need a linear_ordered_comm_ring instance

[Kevin Buzzard]

import tactic

example (R : Type) [linear_ordered_comm_ring R]
  (x y : R) (h1 : x < y + 3) : x + 3 ≤ y + 7 :=
by linarith

works. I will grumpily comment that linarith doesn't work on pnat, as I discovered to my mild irritation at Xena yesterday :-)

[Gihan Marasingha]

OK, I'll have a go at that but I'm not sure about proving the decidable instances.

[Rob Lewis]

You can use docs#classical.prop_decidable for those.

[Kevin Buzzard]

A nice way to do these things is to slowly build up from the basics.

class linear_ordered_comm_ring (α : Type u) extends linear_ordered_ring α, comm_monoid α

so before you prove it's a linear_ordered_comm_ring you should prove it's a linear_ordered_ring and a comm_monoid, and keep working backwards like this until you find stuff which is true from the axioms you've assumed. The entire natural number game was built from me trying to find the most exotic structure which the naturals was (probably it's a linearly ordered semiring or whatever) and then just unravelling all the definitions of everything -- this approach informed which order I should be doing everything in.

[Gihan Marasingha]

I have everything working except trying to get an instance of mul_pos. Though I've written a lemma mul_pos' that I think does the right thing, when I try to use this to get the instance, I receive an error message,

type mismatch at field 'mul_pos'
  mul_pos'
has type
  ∀ (a b : ?m_1), 0 < a → 0 < b → 0 < a * b
but is expected to have type
  ∀ (a b : R), 0 < a → 0 < b → 0 < a * b

I could post the code but it's about 700 lines up to this point. Any suggestions or pointers are appreciated!

[Rob Lewis]

My guess is mul_pos' has an extra type class assumption, maybe unintended? #check @mul_pos' and show the state where you're trying to use it?

[Gihan Marasingha]

Ah yes, I have

mul_pos' : ∀ {α : Type u_1} [_inst_1 : ordered_semiring α] {a b : α}, 0 < a → 0 < b → 0 < a * b

[Gihan Marasingha]

Oh no, that was a mathlib function. I've renamed mine to bob to avoid confusion. I have

bob : ∀ {R : Type} [_inst_1 : myordered_field R] (a b : R), 0 < a → 0 < b → 0 < a * b

[Rob Lewis]

What's the context and goal when you try to apply bob?

[Gihan Marasingha]

This isn't in a tactic state, it's when I'm trying to do

instance : linear_ordered_comm_ring R :=
{ add := comm_group'.add,
  add_assoc := comm_group'.add_assoc,
  zero := comm_group'.zero,
  zero_add := zero_add,
  add_zero := add_zero,
  neg := comm_group'.neg,
  add_left_neg := neg_add,
  add_comm := comm_group'.add_comm,
  mul := myfield.mul,
  mul_assoc := myfield.mul_assoc,
  one := myfield.one,
  one_mul := one_mul,
  mul_one := myfield.mul_one,
  left_distrib := myfield.mul_add,
  right_distrib := add_mul,
  le := le,
  le_refl := le_refl,
  le_trans := le_trans,
  le_antisymm := anti_symm,
  add_le_add_left := add_le_add_left,
  zero_ne_one := myfield.zero_ne_one,
  mul_pos := bob,
  le_total := le_total,
  zero_lt_one := zero_lt_one,
  mul_comm := myfield.mul_comm,

}

[Gihan Marasingha]

bob works fine by itself.

[Rob Lewis]

Oh, so it's working now?

[Gihan Marasingha]

Well it doesn't work the sense that when I type the above code to try to show R is an instance of linear_ordered_comm_ring, I get the error message

type mismatch at field 'mul_pos'
  bob
has type
  ∀ (a b : ?m_1), 0 < a → 0 < b → 0 < a * b
but is expected to have type
  ∀ (a b : R), 0 < a → 0 < b → 0 < a * b

[Mario Carneiro]

with pp.all?

[Rob Lewis]

Okay, replace mul_pos := bob, with mul_pos := _, and show us the output. That's the context and goal at that point.

[Rob Lewis]

Maybe R is Type * instead of Type?

[Gihan Marasingha]

When I put in mul_pos := _, the only text in the Infoview window is:

type mismatch at field 'mul_pos'
  bob ?m_3
has type
  ∀ (b : ?m_1), 0 < ?m_3 → 0 < b → 0 < ?m_3 * b
but is expected to have type
  ∀ (a b : R), 0 < a → 0 < b → 0 < a * b

I have variables {R : Type} [myordered_field R].

[Gihan Marasingha]

And with pp.all, it's:

type mismatch at field 'mul_pos'
  @mth1001.myreal.bob ?m_1 ?m_2 ?m_3
has type
  ∀ (b : ?m_1),
    @has_lt.lt.{0} ?m_1 (@mth1001.myreal.has_lt ?m_1 ?m_2)
      (@has_zero.zero.{0} ?m_1
         (@mth1001.myreal.has_zero.{0} ?m_1
            (@mth1001.myreal.myfield.to_comm_group'.{0} ?m_1 (@mth1001.myreal.myordered_field.to_myfield ?m_1 ?m_2))))
      ?m_3 →
    @has_lt.lt.{0} ?m_1 (@mth1001.myreal.has_lt ?m_1 ?m_2)
      (@has_zero.zero.{0} ?m_1
         (@mth1001.myreal.has_zero.{0} ?m_1
            (@mth1001.myreal.myfield.to_comm_group'.{0} ?m_1 (@mth1001.myreal.myordered_field.to_myfield ?m_1 ?m_2))))
      b →
    @has_lt.lt.{0} ?m_1 (@mth1001.myreal.has_lt ?m_1 ?m_2)
      (@has_zero.zero.{0} ?m_1
         (@mth1001.myreal.has_zero.{0} ?m_1
            (@mth1001.myreal.myfield.to_comm_group'.{0} ?m_1 (@mth1001.myreal.myordered_field.to_myfield ?m_1 ?m_2))))
      (@has_mul.mul.{0} ?m_1 (@mth1001.myreal.has_mul ?m_1 (@mth1001.myreal.myordered_field.to_myfield ?m_1 ?m_2)) ?m_3
         b)
but is expected to have type
  ∀ (a b : R),
    @has_lt.lt.{0} R
      (@preorder.to_has_lt.{0} R
         (@partial_order.to_preorder.{0} R
            (@ordered_add_comm_group.to_partial_order.{0} R
               (@ordered_add_comm_group.mk.{0} R
                  (@mth1001.myreal.comm_group'.add.{0} R
                     (@mth1001.myreal.myfield.to_comm_group'.{0} R
                        (@mth1001.myreal.myordered_field.to_myfield R _inst_1)))
                  (@mth1001.myreal.comm_group'.add_assoc.{0} R
                     (@mth1001.myreal.myfield.to_comm_group'.{0} R
                        (@mth1001.myreal.myordered_field.to_myfield R _inst_1)))
                  (@mth1001.myreal.comm_group'.zero.{0} R
                     (@mth1001.myreal.myfield.to_comm_group'.{0} R
/- Plus many more lines -/

[Rob Lewis]

That looks like you've put in mul_pos := bob _, not mul_pos := _.

[Rob Lewis]

But now my guess is, you have two different < instances.

[Rob Lewis]

Maybe different * instances but < seems more likely.

[Gihan Marasingha]

Oh thanks! I misread what you wrote. The context and goal are:

context:
R : Type,
_inst_1 : myordered_field R
⊢ ∀ (a b : R),
    ordered_add_comm_group.lt 0 a → ordered_add_comm_group.lt 0 b → ordered_add_comm_group.lt 0 (a * b)

[Mario Carneiro]

_inst_1 : myordered_field R

this looks suspicious

[Mario Carneiro]

you are constructing a ring instance, why is a field instance already in the context?

[Gihan Marasingha]

Perhaps I'm going about this entirely the wrong way, but I've created a hierarchy of classes, comm_group', myfield, myordered_field, myreal_field. I'm trying to show, given variables {R : Type} [myordered_field R] that R is an instance of linear_ordered_comm_ring`.

[Mario Carneiro]

Ah, now I'm on board with Rob's idea too. I see mth1001.myreal.has_lt so apparently you have a has_lt instance, but you didn't supply it in the big structure instance (there is no lt := (<) in the list)

[Gihan Marasingha]

OK. I added lt := lt' to the list. This gives the error message

exact tactic failed, type mismatch, given expression has type
  ?m_1 ↔ ?m_1
but is expected to have type
  a < b ↔ a ≤ b ∧ ¬b ≤ a

Is this because my definition lt' is actually λ {R : Type} [_inst_1 : myordered_field R] (x y : R), myordered_field.pos (y - x)?

[Reid Barton]

You need to provide the field lt_iff_le_not_le now too

[Gihan Marasingha]

Thanks everyone for your help. This works now!

[Kevin Buzzard]

Like I said, instead of trying to build it all at once, it's much easier to build all the instances from the very bottom :-)

[Kevin Buzzard]

Then you can use the .. trick.

[Gihan Marasingha]

Oooh, what's the .. trick?

[Bryan Gin-ge Chen]

Basically, if you're constructing a structure of type T and p : U where T extends U, you can use .. p within the curly braces to fill in missing fields from p. There's a brief mention in TPiL here.