# Zulip Chat Archive

## Stream: maths

### Topic: adding positive reals

#### 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 `nzreal`

s but it's more or less the same question for `posreal`

s.

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

#### Joseph Corneli (Jan 26 2019 at 19:02):

If I have learned correctly it should be 37

#### Joseph Corneli (Jan 26 2019 at 19:03):

actually a moderately useful idea in this setting

#### Joseph Corneli (Jan 26 2019 at 19:03):

though I suspect there are some downsides...

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

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

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

.

#### Joseph Corneli (Jan 26 2019 at 19:13):

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

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

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

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

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

#### Kevin Buzzard (Jan 26 2019 at 19:17):

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

#### Kevin Buzzard (Jan 26 2019 at 19:17):

The joys of decidable equality.

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

#### Joseph Corneli (Jan 26 2019 at 19:24):

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

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

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

#### Mario Carneiro (Jan 26 2019 at 20:09):

You should basically always use `rw`

to write `eq.subst`

terms like this

#### Mario Carneiro (Jan 26 2019 at 20:09):

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

#### Kevin Buzzard (Jan 26 2019 at 20:11):

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

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

#### Kevin Buzzard (Jan 26 2019 at 20:13):

That's why they wrote `rw`

, which works great.

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

#### Kevin Buzzard (Jan 26 2019 at 20:19):

Kenny can you see why Neil gets that weird error?

#### Kenny Lau (Jan 26 2019 at 20:20):

Mario said it already

#### Kenny Lau (Jan 26 2019 at 20:20):

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

#### Kevin Buzzard (Jan 26 2019 at 20:20):

What's a motive?

#### Kevin Buzzard (Jan 26 2019 at 20:20):

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

#### Kenny Lau (Jan 26 2019 at 20:21):

Lean needs to guess what you are substituting with

#### Kevin Buzzard (Jan 26 2019 at 20:21):

sure, but they are literally the same

#### Kenny Lau (Jan 26 2019 at 20:22):

anyway see my mathlib-grade :tm: revamp

#### Kevin Buzzard (Jan 26 2019 at 20:22):

yes but you cheated, you used `add_pos`

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

#### Kenny Lau (Jan 26 2019 at 20:25):

why can't I use add_pos?

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

#### Kenny Lau (Jan 26 2019 at 20:26):

just copy the proof of add_pos then

#### 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 ⟩⟩

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

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

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

#### Kenny Lau (Jan 26 2019 at 20:30):

this works

#### Kenny Lau (Jan 26 2019 at 20:33):

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

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

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

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

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

#### 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 `0`

s. Now guess `P`

."

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

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

#### Kevin Buzzard (Jan 26 2019 at 20:39):

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

#### Kevin Buzzard (Jan 26 2019 at 20:40):

[NB by `P`

I mean the `P`

in `#check @eq.subst`

]

#### Kevin Buzzard (Jan 26 2019 at 20:41):

and CS people call `P`

the motive.

#### Kevin Buzzard (Jan 26 2019 at 20:42):

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

#### Kevin Buzzard (Jan 26 2019 at 20:43):

I think this stuff is hard to do well.

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

#### 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 ~~tab~~ctrl-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).

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

#### Kevin Buzzard (Jan 27 2019 at 00:12):

For example, the triangle inequality is called `abs_add`

.

#### Kevin Buzzard (Jan 27 2019 at 00:13):

and the binomial theorem is called `add_pow`

:-)

#### 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:ℝ₊)

#### Kenny Lau (Jan 28 2019 at 13:30):

by unfold posreal; apply_instance

#### Joseph Corneli (Jan 28 2019 at 13:34):

thanks!

Last updated: May 06 2021 at 18:20 UTC