adding negative reals

Stream: maths

[Joseph Corneli]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(you mean -1)

[Kevin Buzzard]

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

[Kevin Buzzard]

hence the error

[Joseph Corneli]

yeah.

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It's not _equal_ to posreal.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

cool! Will look. :painting: