adding positive reals

Stream: maths

[Joseph Corneli]

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.

[Johan Commelin]

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]

If I have learned correctly it should be 37

[Joseph Corneli]

actually a moderately useful idea in this setting

[Joseph Corneli]

though I suspect there are some downsides...

[Joseph Corneli]

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]

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]

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

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

[Joseph Corneli]

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

[Kevin Buzzard]

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

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]

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]

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

[Kevin Buzzard]

The joys of decidable equality.

[Kevin Buzzard]

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]

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

[Neil Strickland]

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]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kenny Lau]

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]

Kenny can you see why Neil gets that weird error?

[Kenny Lau]

Mario said it already

[Kenny Lau]

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

[Kevin Buzzard]

What's a motive?

[Kevin Buzzard]

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

[Kenny Lau]

Lean needs to guess what you are substituting with

[Kevin Buzzard]

sure, but they are literally the same

[Kenny Lau]

anyway see my mathlib-grade :tm: revamp

[Kevin Buzzard]

yes but you cheated, you used add_pos

[Kenny Lau]

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]

why can't I use add_pos?

[Kevin Buzzard]

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]

just copy the proof of add_pos then

[Kevin Buzzard]

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]

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]

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

[Kenny Lau]

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]

this works

[Kenny Lau]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and CS people call P the motive.

[Kevin Buzzard]

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

[Kevin Buzzard]

I think this stuff is hard to do well.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

For example, the triangle inequality is called abs_add.

[Kevin Buzzard]

and the binomial theorem is called add_pow :-)

[Joseph Corneli]

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]

by unfold posreal; apply_instance

[Joseph Corneli]

thanks!