## Stream: maths

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

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 (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
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}

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

⟨λ 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


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}

⟨λ q r,⟨q.val + r.val,
begin
let h0 := zero_add (0 : ℝ),
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 :=


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 Carneiro: the motive making is too messy to do by hand unless absolutely necessary"

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


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

⟨λ 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 :=


#### 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:α),


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 0s. 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}

⟨λ 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 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 (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?
⟨λ 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