## Stream: maths

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

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

#### Kevin Buzzard (Jan 28 2019 at 16:55):

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

(you mean -1)

#### Kevin Buzzard (Jan 28 2019 at 16:55):

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

hence the error

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

#### Kevin Buzzard (Jan 28 2019 at 16:56):

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

#### Kevin Buzzard (Jan 28 2019 at 16:57):

It's not _equal_ to posreal.

#### Kevin Buzzard (Jan 28 2019 at 16:57):

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

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

#### Joseph Corneli (Jan 28 2019 at 16:58):

cool! Will look. :painting:

Last updated: May 12 2021 at 08:14 UTC