Zulip Chat Archive

Stream: maths

Topic: adding negative reals


view this post on Zulip Joseph Corneli (Jan 28 2019 at 16:52):

After the successes with adding positive reals I thought I would try negative reals. But I'm now running into trouble. It was all looking nice up until the end.

import data.real.basic

namespace negreal
def negreal := {r :  // r < 0}
notation `` := negreal
constants negc negd : negreal

-- comparison with posreal: just supply `add_neg` instead of `add_pos`
instance negreal.add : has_add negreal :=
 ⟨λ q r,q.val + r.val, add_neg q.property r.property⟩⟩

-- We will use this fact in the lemma below
example : 0 < (1:) := zero_lt_one

lemma neg_one_lt_zero : -1 < (0:) :=
begin
have h0 : (0:) < 1 , from zero_lt_one,
apply neg_lt_zero.mpr,   -- -a < 0 ↔ 0 < a
exact h0,
end

instance negreal.one : has_one negreal := ⟨⟨(-1:), neg_one_lt_zero⟩⟩

example : negreal := (-1:)

I get:

failed to synthesize type class instance for
⊢ has_neg ℝ₋

But has_neg : Type u_1 → Type u_1 and the usual - would in fact kick me from negreal to posreal.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 16:53):

I am not sure that has_one was designed to represent numbers which we would usually call -1.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 16:55):

You have used has_one, so now Lean knows what you mean by 1:R-

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 16:55):

(you mean -1)

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 16:55):

but it doesn't know what you mean by -x if x is a negreal

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 16:55):

hence the error

view this post on Zulip Joseph Corneli (Jan 28 2019 at 16:56):

yeah.

What's interesting (resp., annoying) is that negreal is somehow just a copy of posreal with a different paint job.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 16:56):

negreal is exactly what you've defined it to be.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 16:57):

It's not _equal_ to posreal.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 16:57):

It does biject with posreal, but then again the naturals biject with the integers.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 16:58):

As an exercise, you should import data.equiv.basic and try and construct a term of type equiv posreal negreal. There's your paint job.

view this post on Zulip Joseph Corneli (Jan 28 2019 at 16:58):

cool! Will look. :painting:


Last updated: May 12 2021 at 08:14 UTC