## Stream: new members

### Topic: Defining the unit interval

#### Pedro Minicz (Jun 07 2020 at 02:49):

How to elegantly define the unit interval? I have kind of defined it using set, however, I find the result rather unwieldy.

import data.real.basic
import data.set.basic
import tactic

@[simp] def ge_zero : set ℝ := λ n, n ≥ 0
@[simp] def le_one : set ℝ := λ n, n ≤ 1

def I : set ℝ := ge_zero ∩ le_one


#### Pedro Minicz (Jun 07 2020 at 02:50):

There should be a way of easily defining it with quotients I think.

#### Mario Carneiro (Jun 07 2020 at 02:51):

The more idiomatic way to write your definition is:

def I : set ℝ := {x | 0 ≤ x ∧ x ≤ 1}


What's wrong with it?

#### Mario Carneiro (Jun 07 2020 at 02:51):

I don't see any reason for quotients to get involved, the unit interval is a subtype of the reals

#### Mario Carneiro (Jun 07 2020 at 02:52):

(This already exists BTW, it's called Icc 0 1)

#### Pedro Minicz (Jun 07 2020 at 03:04):

I'd like use relation a ~ b on ℝ defined as b - a ∈ ℤ to be my unit interval.

#### Pedro Minicz (Jun 07 2020 at 03:06):

As I understand, if I define I as a quotient on ℝ, instead of a set ℝ, I can have 0 : I, or am I mistaken?

#### Lucas Viana (Jun 07 2020 at 03:26):

I don't know if this topic came from mine (the message I deleted earlier), but I am having a similar problem in #new members > About measures

#### Lucas Viana (Jun 07 2020 at 03:28):

The thing I found neat about quotients is that I can define a function on the reals and lift it to the interval without having to redefine things like addition and multiplication (but maybe it is not so hard to do this in the subtype definition?)

#### Lucas Viana (Jun 07 2020 at 03:42):

Pedro Minicz said:

As I understand, if I define I as a quotient on ℝ, instead of a set ℝ, I can have 0 : I, or am I mistaken?

I think you could define it as a subtype (instead of a set), so you could have (a : I):

def I := {x : ℝ // x ∈ Icc (0:ℝ) (1:ℝ)}


but to have 0:I you would need I.has_zero

#### Mario Carneiro (Jun 07 2020 at 03:48):

Pedro Minicz said:

I'd like use relation a ~ b on ℝ defined as b - a ∈ ℤ to be my unit interval.

That's not the unit interval, that's S^1

#### Mario Carneiro (Jun 07 2020 at 03:49):

it is naturally bijective with [0, 1) but not [0, 1]

#### Mario Carneiro (Jun 07 2020 at 03:51):

To flesh out Lucas's suggestion:

import data.real.basic data.set.intervals.basic

def I : Type := set.Icc (0:ℝ) (1:ℝ)

instance : has_zero I := ⟨⟨0, by simp [zero_le_one]⟩⟩
instance : has_one I := ⟨⟨1, by simp [zero_le_one]⟩⟩

#check (0 : I)
#check (1 : I)


#### Pedro Minicz (Jun 07 2020 at 03:53):

I ended up settling for the following:

import data.real.basic
import data.set.basic
import tactic

@[simp] def R (a b : ℝ) : Prop := ∃ k : ℤ, ↑k = b - a

theorem R_equiv : equivalence R :=
begin
unfold equivalence,
unfold transitive,
split; try { split },
show reflexive R, from λ a, ⟨0, by simp [sub_self]⟩,
show symmetric R,
{ rintros a b ⟨k, hk⟩,
exact ⟨-k, by push_cast; linarith⟩ },
show transitive R,
{ rintros a b c ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩,
exact ⟨k₁ + k₂, by push_cast; linarith⟩ }
end

def I : Type := quotient (setoid.mk R R_equiv)


I'd like to see an expression 0.5 : I, but I couldn't manufacture it.

#### Mario Carneiro (Jun 07 2020 at 03:53):

You can't divide by 2 in R/Z though

#### Mario Carneiro (Jun 07 2020 at 03:53):

however you can use [[1/2]]

#### Pedro Minicz (Jun 07 2020 at 03:54):

Mario Carneiro said:

it is naturally bijective with [0, 1) but not [0, 1]

Yes, I realize this difference.

#### Mario Carneiro (Jun 07 2020 at 03:54):

You can also leverage the general theory of quotient groups here to define R/Z and get all the additive group structure

#### Pedro Minicz (Jun 07 2020 at 03:55):

Mario Carneiro said:

To flesh out Lucas's suggestion:

import data.real.basic data.set.intervals.basic

def I : Type := set.Icc (0:ℝ) (1:ℝ)

instance : has_zero I := ⟨⟨0, by simp [zero_le_one]⟩⟩
instance : has_one I := ⟨⟨1, by simp [zero_le_one]⟩⟩

#check (0 : I)
#check (1 : I)


Wow, those instances make a big difference! It suddenly looks so much nicer.

#### Pedro Minicz (Jun 07 2020 at 04:00):

Mario Carneiro said:

You can also leverage the general theory of quotient groups here to define R/Z and get all the additive group structure

Can I use something defined mathlib for that? I am not that familiar with it already. Or does the quotient I defined above suffice?

#### Mario Carneiro (Jun 07 2020 at 04:03):

import data.real.basic group_theory.quotient_group

show is_add_group_hom (int.cast_ring_hom ℝ), by apply_instance

def I : Type := quotient_add_group.quotient (set.range (coe : ℤ → ℝ))

def I.mk : ℝ → I := quotient_add_group.mk

#check (0 : I)
#check (I.mk (1/2) : I)


#### Mario Carneiro (Jun 07 2020 at 04:04):

The first instance should arguably be in mathlib, but I think it's in a precarious position because is_add_group_hom is deprecated

#### Pedro Minicz (Jun 07 2020 at 05:07):

In this context, we should have (0 : I) = 1, right?

import data.real.basic
import group_theory.quotient_group

instance : is_add_submonoid (set.range (coe : ℤ → ℝ)) :=
is_add_submonoid.mk ⟨0, rfl⟩ (by rintros a b ⟨ka, hka⟩ ⟨kb, hkb⟩; exact ⟨ka + kb, by push_cast; linarith⟩)

instance : is_add_subgroup (set.range (coe : ℤ → ℝ)) :=
is_add_subgroup.mk (by rintros a ⟨k, hk⟩; exact ⟨-k, by push_cast; linarith⟩)

def I : Type := quotient_add_group.quotient (set.range (coe : ℤ → ℝ))

def I.mk : ℝ → I := quotient_add_group.mk

instance : has_zero I := ⟨I.mk 0⟩
instance : has_one I  := ⟨I.mk 1⟩

example : (0 : I) = 1 :=
begin
apply quot.sound,
sorry
end


#### Mario Carneiro (Jun 07 2020 at 05:08):

Indeed.  change _ ∈ _, should make it clearer

#### Pedro Minicz (Jun 07 2020 at 05:09):

Wow, you are a wizard, hahaha. Thank you very much!

#### Mario Carneiro (Jun 07 2020 at 05:09):

example : (0 : I) = 1 := quot.sound ⟨1, by simp⟩


#### Pedro Minicz (Jun 07 2020 at 05:10):

I keep getting suck on steps like these, I can "see through" the definitions, but find myself unable to show it to Lean.

#### Mario Carneiro (Jun 07 2020 at 05:11):

In theory these should be simp lemmas, but in a hastily written development they may not be and then you have to use change tricks to force your way through the layers of definition

#### Mario Carneiro (Jun 07 2020 at 05:14):

in the proof I gave above, ⟨1, ... forces it even past _ \in set.range _ to \exists n : int, ... and provides the witness 1, after which the body of the exists is a simple theorem \u 1 = -0 + 1 which simp can handle

#### Lucas Viana (Jun 07 2020 at 14:16):

From this construction, how can I instantiate setoid \R?

#### Lucas Viana (Jun 07 2020 at 14:21):

Found it:

instance : setoid ℝ := quotient_add_group.left_rel (set.range (coe : ℤ → ℝ))


#### Mario Carneiro (Jun 07 2020 at 14:30):

that shouldn't be an instance, because it will be the one and only setoid real instance if so, and this particular instance has no claim to canonicality

#### Mario Carneiro (Jun 07 2020 at 14:31):

it can be a local instance but usually we just use a def

#### Mario Carneiro (Jun 07 2020 at 14:31):

arguably setoid shouldn't even be a class because this lack of uniqueness comes up so often

#### Lucas Viana (Jun 07 2020 at 14:41):

I just want to use the ⟦x⟧ notation, should I do:

notation ⟦ x ⟧ := I.mk x