Zulip Chat Archive

Stream: new members

Topic: Defining the unit interval


view this post on Zulip 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

view this post on Zulip Pedro Minicz (Jun 07 2020 at 02:50):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 07 2020 at 02:52):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 07 2020 at 03:49):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 07 2020 at 03:53):

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

view this post on Zulip Mario Carneiro (Jun 07 2020 at 03:53):

however you can use [[1/2]]

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 07 2020 at 04:03):

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)

view this post on Zulip 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

view this post on Zulip 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)

@[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

view this post on Zulip Mario Carneiro (Jun 07 2020 at 05:08):

Indeed. change _ ∈ _, should make it clearer

view this post on Zulip Pedro Minicz (Jun 07 2020 at 05:09):

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

view this post on Zulip Mario Carneiro (Jun 07 2020 at 05:09):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Lucas Viana (Jun 07 2020 at 14:16):

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

view this post on Zulip Lucas Viana (Jun 07 2020 at 14:21):

Found it:

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 07 2020 at 14:31):

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

view this post on Zulip 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

view this post on Zulip Lucas Viana (Jun 07 2020 at 14:41):

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

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

Instead?

view this post on Zulip Lucas Viana (Jun 07 2020 at 14:42):

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


Last updated: May 11 2021 at 12:15 UTC