Stream: maths

Topic: Using linarith with my own class

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?

Rob Lewis (Nov 20 2020 at 21:26):

You probably need an instance from your class to comm_ring.

Shing Tak Lam (Nov 20 2020 at 21:26):

The tactic docs seem to suggest you need a linear_ordered_comm_ring instance

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

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.

Rob Lewis (Nov 20 2020 at 21:34):

You can use docs#classical.prop_decidable for those.

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.

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!

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?

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


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


Rob Lewis (Nov 20 2020 at 23:20):

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

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 :=
zero := comm_group'.zero,
neg := comm_group'.neg,
mul := myfield.mul,
mul_assoc := myfield.mul_assoc,
one := myfield.one,
one_mul := one_mul,
mul_one := myfield.mul_one,
le := le,
le_refl := le_refl,
le_trans := le_trans,
le_antisymm := anti_symm,
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 (Nov 20 2020 at 23:21):

bob works fine by itself.

Rob Lewis (Nov 20 2020 at 23:22):

Oh, so it's working now?

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


Mario Carneiro (Nov 20 2020 at 23:24):

with pp.all?

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.

Rob Lewis (Nov 20 2020 at 23:25):

Maybe R is Type * instead of Type?

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

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
(@mth1001.myreal.myfield.to_comm_group'.{0} R
(@mth1001.myreal.myordered_field.to_myfield R _inst_1)))
(@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 (Nov 20 2020 at 23:35):

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

Rob Lewis (Nov 20 2020 at 23:35):

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

Rob Lewis (Nov 20 2020 at 23:36):

Maybe different * instances but < seems more likely.

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


Mario Carneiro (Nov 20 2020 at 23:39):

_inst_1 : myordered_field R

this looks suspicious

Mario Carneiro (Nov 20 2020 at 23:39):

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

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.

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)

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

Reid Barton (Nov 21 2020 at 00:04):

You need to provide the field lt_iff_le_not_le now too

Gihan Marasingha (Nov 21 2020 at 00:21):

Thanks everyone for your help. This works now!

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

Kevin Buzzard (Nov 21 2020 at 00:27):

Then you can use the .. trick.

Gihan Marasingha (Nov 21 2020 at 00:28):

Oooh, what's the .. trick?

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