Zulip Chat Archive

Stream: maths

Topic: Using linarith with my own class


view this post on Zulip Gihan Marasingha (Nov 20 2020 at 21:10):

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?

view this post on Zulip Rob Lewis (Nov 20 2020 at 21:26):

You probably need an instance from your class to comm_ring.

view this post on Zulip Shing Tak Lam (Nov 20 2020 at 21:26):

The tactic docs seem to suggest you need a linear_ordered_comm_ring instance

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 21:29):

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 :-)

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 21:33):

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

view this post on Zulip Rob Lewis (Nov 20 2020 at 21:34):

You can use docs#classical.prop_decidable for those.

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 21:39):

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.

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:09):

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!

view this post on Zulip Rob Lewis (Nov 20 2020 at 23:14):

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?

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:15):

Ah yes, I have

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

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:19):

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

view this post on Zulip Rob Lewis (Nov 20 2020 at 23:20):

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

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:20):

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,

}

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:21):

bob works fine by itself.

view this post on Zulip Rob Lewis (Nov 20 2020 at 23:22):

Oh, so it's working now?

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:23):

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

view this post on Zulip Mario Carneiro (Nov 20 2020 at 23:24):

with pp.all?

view this post on Zulip Rob Lewis (Nov 20 2020 at 23:25):

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

view this post on Zulip Rob Lewis (Nov 20 2020 at 23:25):

Maybe R is Type * instead of Type?

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:32):

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

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:33):

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

view this post on Zulip Rob Lewis (Nov 20 2020 at 23:35):

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

view this post on Zulip Rob Lewis (Nov 20 2020 at 23:35):

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

view this post on Zulip Rob Lewis (Nov 20 2020 at 23:36):

Maybe different * instances but < seems more likely.

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:38):

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)

view this post on Zulip Mario Carneiro (Nov 20 2020 at 23:39):

_inst_1 : myordered_field R

this looks suspicious

view this post on Zulip Mario Carneiro (Nov 20 2020 at 23:39):

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

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:45):

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

view this post on Zulip Mario Carneiro (Nov 20 2020 at 23:45):

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)

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 23:52):

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)?

view this post on Zulip Reid Barton (Nov 21 2020 at 00:04):

You need to provide the field lt_iff_le_not_le now too

view this post on Zulip Gihan Marasingha (Nov 21 2020 at 00:21):

Thanks everyone for your help. This works now!

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 00:26):

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 :-)

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 00:27):

Then you can use the .. trick.

view this post on Zulip Gihan Marasingha (Nov 21 2020 at 00:28):

Oooh, what's the .. trick?

view this post on Zulip Bryan Gin-ge Chen (Nov 21 2020 at 01:19):

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.


Last updated: May 11 2021 at 17:39 UTC