Zulip Chat Archive

Stream: maths

Topic: adding positive reals


view this post on Zulip Joseph Corneli (Jan 26 2019 at 18:41):

def nzreal := {r :  // r  0}
notation `*` := nzreal
constants nzc nzd : nzreal
#check nzc+nzd

failed to synthesize type class instance for
⊢ has_add ℝ*

Is this a place to use the canonical structures that Assia and Cyril told us about in Amsterdam? Seems to me like the kind of thing that would be a match for that sort of thinking.

Oh, that's nzreals but it's more or less the same question for posreals.

view this post on Zulip Johan Commelin (Jan 26 2019 at 19:01):

Well, you just defined a new type. So you will have to explain what addition should mean. Also, what should x + -x be?

view this post on Zulip Joseph Corneli (Jan 26 2019 at 19:02):

If I have learned correctly it should be 37

view this post on Zulip Joseph Corneli (Jan 26 2019 at 19:03):

actually a moderately useful idea in this setting

view this post on Zulip Joseph Corneli (Jan 26 2019 at 19:03):

though I suspect there are some downsides...

view this post on Zulip Joseph Corneli (Jan 26 2019 at 19:09):

namespace nzreal

def nzreal := {r :  // r  0}
notation `*` := nzreal
constants nzc nzd : nzreal
#check nzc+nzd

def add : nzreal  nzreal  
| x y := subtype.val x + subtype.val y

-- except this doesn't work
instance : has_add nzreal := nzreal.add
end nzreal

view this post on Zulip Neil Strickland (Jan 26 2019 at 19:10):

The following works:

import data.rat data.real.basic

def pos_rat := { q :  // q > 0}

instance pos_rat.add : has_add pos_rat :=
 ⟨λ q r,q.val + r.val,add_lt_add q.property r.property⟩⟩

def pos_real := { q :  // q > 0}

instance pos_real.add : has_add pos_real :=
 ⟨λ q r,q.val + r.val,
  @eq.subst  (λ z, z < q.val + r.val) (0 + 0) 0 (zero_add 0) (add_lt_add q.property r.property)⟩⟩

I am sure that the version for is suboptimal; I hope that someone more expert will clean it up.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 19:12):

-- except this doesn't work
instance : has_add nzreal := nzreal.add

This doesn't work because to make an instance of has_add X you have to supply a map X -> X -> X, and your map nzreal.add has type nzreal -> nzreal -> real.

view this post on Zulip Joseph Corneli (Jan 26 2019 at 19:13):

yeah, so this one isn't going to work without partial functions

view this post on Zulip Joseph Corneli (Jan 26 2019 at 19:15):

positives should be OK per @Neil Strickland (I will have to take some time to understand that code)

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 19:15):

@Neil Strickland you need a > 0 -> b > 0 -> a + b > 0. My instinct now (which was not at all my instinct a year ago) is that this result should be in any reasonable API for totally ordered abelian groups.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 19:16):

So the issue is finding the result. And until we have better search the best way to find the result is to guess the name. I guessed add_pos and pos_add and I hit tab a few times, and eventually I found it.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 19:16):

instance pos_real.add : has_add pos_real :=
 ⟨λ q r,q.val + r.val,add_pos q.property r.property⟩⟩

The reason you get away with this for the rationals, I suspect, is that 0 + 0 is definitionally equal to 0, but perhaps not for the reals.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 19:17):

example : (0 : ) + 0 = 0 := rfl -- works
example : (0 : ) + 0 = 0 := rfl -- fails

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 19:17):

The joys of decidable equality.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 19:20):

So when I was solving my first year undergraduate example sheets just over a year ago, I would run into things like this and think "oh I need to prove a,b>0 implies a+b>0, I know about add_lt_add, and I can definitely do it from there, so let's go" and I would write code like yours. Since then I have understood Mario's philosophy for mathlib, which perhaps came from his extensive use of metamath beforehand, which is that libraries should be really thorough. Anything which looks like a standard thing which a mathematician would assume without comment -- such a thing should be in the library already. Once you realise this, you stop trying to prove stuff for yourself and start looking for it instead.

view this post on Zulip Joseph Corneli (Jan 26 2019 at 19:24):

Thanks for these pointers. This seems to be a very sensible philosophy.

view this post on Zulip Neil Strickland (Jan 26 2019 at 19:49):

That makes sense, thanks. But I'm also interested in whether there is a better way to deal with the eq.subst thing. The following seems quite mysterious to me:

def pos_real := { q :  // 0 < q}

instance pos_real.add : has_add pos_real :=
 ⟨λ q r,q.val + r.val,
  begin
   let h0 := zero_add (0 : ),
   let h1 := (add_lt_add q.property r.property),
   let h2 : 0 < q.val + r.val := eq.subst h0 h1,
   let h3 : 0 < q.val + r.val := eq.subst h0 (add_lt_add q.property r.property),
   exact h3,
  end
  ⟩⟩

Note that I changed q > 0 to 0 < q, which eliminates some issues. But still Lean accepts h2 and rejects h3, even though h3 is just the result of inlining the definition of h1 in h2. The error message says:

term
  q.property
has type
  0 < @subtype.val  (λ (q : ), 0 < q) q
but is expected to have type
  0 < @subtype.val  (λ (q : ), 0 + 0 < q) q

I guess I could probably work out why that arises if I really had to. But I would be more interested to hear about any general strategies to avoid this kind of thing.

view this post on Zulip Neil Strickland (Jan 26 2019 at 20:03):

It's also interesting that Lean has no problem with this:

lemma real_add_pos {q r : } (hq : q > 0) (hr : r > 0) : q + r > 0 :=
 eq.subst (add_zero (0 : )) (add_lt_add hq hr)

So I guess that the problem with my pos_real.add is just with the implicit arguments to subtype.val, somehow.

view this post on Zulip Mario Carneiro (Jan 26 2019 at 20:09):

You should basically always use rw to write eq.subst terms like this

view this post on Zulip Mario Carneiro (Jan 26 2019 at 20:09):

the motive making is too messy to do by hand unless absolutely necessary

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:11):

The rule of thumb is: "eq.subst never works".

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:12):

There are countless threads with me moaning about the stupid triangle, which is , or \t, the notation for eq.subst. I can never get it to work.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:13):

That's why they wrote rw, which works great.

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:19):

universes u

def pos_of (α : Type u) [has_lt α] [has_zero α] : Type u :=
{ x : α // 0 < x }

namespace pos_of

variables (α : Type u)

instance [ordered_cancel_comm_monoid α] : add_semigroup (pos_of α) :=
{ add := λ x y, x.1 + y.1, add_pos x.2 y.2,
  add_assoc := λ x y z, subtype.eq $ add_assoc _ _ _ }

instance [ordered_semiring α] : semigroup (pos_of α) :=
{ mul := λ x y, x.1 * y.1, mul_pos x.2 y.2,
  mul_assoc := λ x y z, subtype.eq $ mul_assoc _ _ _ }

instance [linear_ordered_semiring α] : monoid (pos_of α) :=
{ one := 1, zero_lt_one,
  one_mul := λ x, subtype.eq $ one_mul _,
  mul_one := λ x, subtype.eq $ mul_one _,
  .. pos_of.semigroup α }

end pos_of

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:19):

Kenny can you see why Neil gets that weird error?

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:20):

Mario said it already

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:20):

"Mario Carneiro: the motive making is too messy to do by hand unless absolutely necessary"

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:20):

What's a motive?

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:20):

I literally can't see the difference between his h2 and h3 strategies

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:21):

Lean needs to guess what you are substituting with

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:21):

sure, but they are literally the same

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:22):

anyway see my mathlib-grade :tm: revamp

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:22):

yes but you cheated, you used add_pos

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:25):

universes u

def pos_of (α : Type u) [has_lt α] [has_zero α] : Type u :=
{ x : α // 0 < x }

namespace pos_of

variables (α : Type u)

instance [ordered_cancel_comm_monoid α] : add_semigroup (pos_of α) :=
{ add := λ x y, x.1 + y.1, add_pos x.2 y.2,
  add_assoc := λ x y z, subtype.eq $ add_assoc _ _ _ }

instance [ordered_semiring α] : semigroup (pos_of α) :=
{ mul := λ x y, x.1 * y.1, mul_pos x.2 y.2,
  mul_assoc := λ x y z, subtype.eq $ mul_assoc _ _ _ }

instance [linear_ordered_semiring α] : monoid (pos_of α) :=
{ one := 1, zero_lt_one,
  one_mul := λ x, subtype.eq $ one_mul _,
  mul_one := λ x, subtype.eq $ mul_one _,
  .. pos_of.semigroup α }

instance [linear_ordered_field α] : group (pos_of α) :=
{ inv := λ x, x.1⁻¹, (inv_eq_one_div x.1).symm  one_div_pos_of_pos x.2,
  mul_left_inv := λ x, subtype.eq $ inv_mul_cancel $ ne_of_gt x.2,
  .. pos_of.monoid α }

end pos_of

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:25):

why can't I use add_pos?

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:26):

because this whole thread started because Neil didn't know about add_pos and we're still stuck trying to work around it.

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:26):

just copy the proof of add_pos then

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:26):

import data.real.basic

def pos_real := { q :  // 0 < q}

instance pos_real.add : has_add pos_real :=
 ⟨λ q r,q.val + r.val,
  begin
   let h0 := zero_add (0 : ),
   exact (eq.subst h0 (add_lt_add q.property r.property) : 0 < q.val + r.val), -- stupid triangle doesn't work
  end
  ⟩⟩

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:28):

universes u
example (α : Type u) [ordered_cancel_comm_monoid α] {x y : α} (hx : 0 < x) (hy : 0 < y) : 0 < x + y :=
zero_add (0:α)  add_lt_add hx hy

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:29):

Right, so Neil got it to work with h2, the question is why what I wrote doesn't work.

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:30):

universes u
example (α : Type u) [ordered_cancel_comm_monoid α] {x y : α} (hx : 0 < x) (hy : 0 < y) : 0 < x + y :=
have h0 : _ := zero_add (0:α),
eq.subst h0 $ add_lt_add hx hy

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:30):

this works

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:33):

just follow standard procedures and you won't get into trouble :P

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:34):

Maybe it's just some higher order unification issue. Oh, I just remembered what a motive is. Oh so in fact that's exactly what Mario said.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:35):

Neil -- the issue with eq.subst is that Lean has to guess this implicit argument P which in general is impossible. Oh Ok so in fact I'm now there.

view this post on Zulip Neil Strickland (Jan 26 2019 at 20:35):

The library add_pos is just the obvious generalisation of my real_add_pos, so it is just a tiny proof term. The only issues are (a) why the elaborater gets confused in the subtype context, but not if we write add_pos as a separate definition, and (b) how should you find add_pos if you do not already know about it?

For (b), I tried #print ordered_semiring and #print ordered_ring and #print prefix ordered_semiring and #print ordered_monoid (but ordered_monoid does not exist). I did not try #find or #print ordered_group. I don't know if one can learn anything from that history.

view this post on Zulip Kenny Lau (Jan 26 2019 at 20:36):

@Kevin Buzzard we all know that a motive is a smooth projective variety with extra structures :P

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:37):

You're saying "I want the answer to be something like 0 < x -> 0 < y -> 0 < x + y and I want it to be this after we've taken all the 0+0's and replaced them with 0s. Now guess P."

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:37):

And Lean guesses 0 + 0 < x -> 0 + 0 < y -> 0 + 0 < x + y because that's one of many valid guesses.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:38):

and then it checks that q.property is 0 + 0 < q.val and it isn't, so it gives up. I think the CS guys call this "higher order unification" and they've proved that the general problem is undecidable. So Leo has to write some algorithm which works in as many simple cases as possible, but it can't be perfect.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:39):

Kenny, it's the cohomology of a smooth projective variety.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:40):

[NB by P I mean the P in #check @eq.subst]

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:41):

and CS people call P the motive.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:42):

https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#elaboration-hints

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:43):

I think this stuff is hard to do well.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 20:52):

import data.real.basic

def pos_real := { q :  // 0 < q}

instance pos_real.add : has_add pos_real :=
 ⟨λ q r,q.val + r.val,
  begin
   let h0 := zero_add (0 : ),
   exact @eq.subst  (λ x, x < q.val + r.val) _ _ h0 (add_lt_add q.property r.property)
  end
  ⟩⟩

There's how to do with eq.subst. I had to tell it P explicitly, because it has an algorithm which produces a P and it produces the wrong P and now you're doomed. Elaboration and unification are thorny issues -- there was a thread about them yesterday. I can't tell you why one works and another doesn't. Lean has to solve a puzzle -- "fill in all the { ... } stuff" -- and this is harder than it looks, I don't understand the arguments they use, and in higher order situations like this it's not surprising that they sometimes fail.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 21:12):

Neil -- the best way to find lemmas is to learn the knack. I found this very frustrating at first, but the algorithm is first to learn all the three letter acronyms for everything eg add, sub, div, dvd, neg, pos, lt, nonneg etc (ok so they're not all three letters) and all the tricks like symm, comm, antisymm etc, then guess what your lemma is called, or at least part of it, then make sure you've imported the file where the lemma might be if necessary, then type in the parts of the name that you guessed and then mash tabctrl-space and esc (at least in VS Code) and hope you find it in the list that appears (press ctrl-space to expand the definitions of the theorems which appear in the list).

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 21:13):

The lemma should be called add_pos_of_pos_of_pos but for things that come up a lot they tend to abbreviate them.

view this post on Zulip Kevin Buzzard (Jan 27 2019 at 00:12):

For example, the triangle inequality is called abs_add.

view this post on Zulip Kevin Buzzard (Jan 27 2019 at 00:13):

and the binomial theorem is called add_pow :-)

view this post on Zulip Joseph Corneli (Jan 28 2019 at 13:29):

anyway see my mathlib-grade :tm: revamp

@Kenny Lau that looks great but I'm not sure how to use it properly. Would you please tell me how I should adjust my example below to use your definitions?

-- ...
open pos_of

def posreal := pos_of 

notation `` := posreal

-- the following `instance` proofs seem superfluous given the definitions you created in the pos_of namespace, but how can I use your definitions?
instance posreal.add : has_add posreal :=
 ⟨λ q r, q.val + r.val, add_pos q.property r.property⟩⟩

instance posreal.one : has_one posreal := ⟨⟨(1:), zero_lt_one⟩⟩

example :  := (2 : ) + (3:)

view this post on Zulip Kenny Lau (Jan 28 2019 at 13:30):

by unfold posreal; apply_instance

view this post on Zulip Joseph Corneli (Jan 28 2019 at 13:34):

thanks!


Last updated: May 06 2021 at 18:20 UTC