Defining the unit interval

Stream: new members

[Pedro Minicz]

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]

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

[Mario Carneiro]

The more idiomatic way to write your definition is:

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

What's wrong with it?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Pedro Minicz]

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

[Pedro Minicz]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

however you can use [[1/2]]

[Pedro Minicz]

Mario Carneiro said:

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

Yes, I realize this difference.

[Mario Carneiro]

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

[Pedro Minicz]

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]

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]

import data.real.basic group_theory.quotient_group

instance coe_int_is_add_group_hom : is_add_group_hom (coe : ℤ → ℝ) :=
show is_add_group_hom (int.cast_ring_hom ℝ), by apply_instance

@[derive add_group]
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]

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]

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⟩)

@[derive add_group]
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]

Indeed. change _ ∈ _, should make it clearer

[Pedro Minicz]

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

[Mario Carneiro]

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

[Pedro Minicz]

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]

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]

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]

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

[Lucas Viana]

Found it:

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Lucas Viana]

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

notation `⟦` x `⟧` := I.mk x

Instead?

[Lucas Viana]

This looks simpler indeed (the other way would return more complicated expressions)