notation challenge

Stream: general

[Damiano Testa]

Dear All,

I have a tricky notationquestion. I am working on the "positive/non-negative" elements of a Type X (of course, X has zero and lt/le). Everything works smoothly and my question is about the notation. Ideally, I would like

• the type of non-negative elements of X to be X≥0 (in analogy with nnreal);
• the type of positive elements of X to be X>0 (naturally).

The closest I could get is to have |X≥0 and |X>0 to work (see below).

Is it possible to drop the | entirely?

Thanks!

import data.real.nnreal

/--  The elements of a type that are in relation with a fixed element.  The main examples are
the positive/non-negative elements of a Type with an order. -/
def rel_with {α : Type*} (o : α) (r : α → α → Prop) : Type* := { a : α // r o a }

-- Ideally, I would like to drop the vertical bar `|` from the notation.
notation `|`:1024 α:1 `≥0`:1 := rel_with (0 : α) (≤)
notation `|`:1024 α:1 `>0`:1 := rel_with (0 : α) (<)

/- Check: works with `pnat`. -/
lemma pnat_eq_new : pnat = |ℕ>0 := rfl
lemma natp_eq_new : ℕ+ = |ℕ>0 := rfl

/- Check: works with random Types with `0` and `<`. -/
variables {X : Type*} [has_zero X] [has_lt X]
#check (|X>0 : Type*)  --works

variables {Y : Type*} [has_zero Y] [linear_order Y]
#check (|Y>0 : Type*)  --works
#check (|Y≥0 : Type*)  --works

variables {R : Type*} [ordered_add_comm_monoid R]
#check (|R>0 : Type*)  --works
#check (|R≥0 : Type*)  --works

/- Check: works with `ℝ≥0`. -/
/-  A new name, since otherwise `ℝ≥0` could ambiguously refer to the actual nnreals or the
ones defined using `rel_with`. -/
def myr : Type := ℝ
instance myr.has_zero : has_zero myr := { zero := (0 : ℝ) }
instance myr.has_le : has_le myr := { le := ((≤) : ℝ → ℝ → Prop) }

open_locale nnreal
/- Check: works with `ℝ≥0`. -/
lemma nnreal_eq_myn : ℝ≥0 = |myr≥0 := rfl

[Floris van Doorn]

My guess would be that it's not possible, since it's not really possible to distinguish X≥0 from ge on Type*.

There is another problem with this notation (even with |), and that is that ≥0 and >0 become tokens, which means that if we write ≥0 and >0 anywhere in a file that imports this, it will not be interpreted as two tokens:

def rel_with {α : Type*} (o : α) (r : α → α → Prop) : Type* := { a : α // r o a }
notation `|`:1024 α:1 `≥0`:1 := rel_with (0 : α) (≤)

example : 1≥0 := sorry -- syntax error
example : ∀x≥0, x = x := sorry -- syntax error

[Damiano Testa]

Floris,

thank you for your comments! I might have learned what a token is!

If this makes sense, I think that what I had in mind then was a "dependent" notation where _>0 is the token and _ is filled in by the symbol for the Type in question. Once I say it like this, I realize that this is probably too much to ask for...

[Damiano Testa]

On the other hand, this is a good way to enforce that the order relations are separated by spaces...

[Yaël Dillies]

Actually I guess that's pretty fine because we supposedly always use ≤ and <. If the Unicode index modifier proposition goes through, then you will be able to write subscripts ≥ and >.

[Damiano Testa]

ah, subscript ≥0 would look even better!

[Yaël Dillies]

Another idea is to use ≥₀ and >₀.

[Yaël Dillies]

Looks a bit weird, but I think it's fine!

[Yaël Dillies]

Is that already a notation somewhere?

[Damiano Testa]

Yaël, I like your suggestion a lot (until > and ≥ can be subscripts as well)! Now the remaining issue is the prefix | that I would like to avoid.

[Damiano Testa]

Here is the updated notation:

def rel_with {α : Type*} (o : α) (r : α → α → Prop) : Type* := { a : α // r o a }

notation `|`:1024 α:1 `≥₀`:1 := rel_with (0 : α) (≤)
notation `|`:1024 α:1 `>₀`:1 := rel_with (0 : α) (<)

/- Check: works with `pnat`. -/
lemma pnat_eq_new : pnat = |ℕ>₀ := rfl
lemma natp_eq_new : ℕ+ = |ℕ>₀ := rfl

/- Check: works with a random Types with `0` and `<`. -/
variables {X : Type*} [has_zero X] [has_lt X]
#check (|X>₀ : Type*)  --works

variables {Y : Type*} [has_zero Y] [linear_order Y]
#check (|Y>₀ : Type*)  --works
#check (|Y≥₀ : Type*)  --works

variables {R : Type*} [ordered_add_comm_monoid R]
#check (|R>₀ : Type*)  --works
#check (|R≥₀ : Type*)  --works

How do people feel about this?

[Yaël Dillies]

Does it not pick up the correct thing by itself when you remove the |?

[Damiano Testa]

This seems to mess up the already defined notation for pnat and nnreal:

def rel_with {α : Type*} (o : α) (r : α → α → Prop) : Type* := { a : α // r o a }

notation α`≥₀` := rel_with (0 : α) (≤)
notation α`>₀` := rel_with (0 : α) (<)

#check ℕ>₀  --works
#check ℕ≥₀  --works

-- however this does not
lemma pnat_eq_new : pnat = ℕ>₀ := rfl
-- not a rfl-lemma, even though marked as rfl
-- and
-- invalid pre-numeral, universe level must be > 0

(I get the same error when I try the nnreal "rfl".)

[Yaël Dillies]

Okay I just don't know how notations work :sad:

[Damiano Testa]

Me neither, but thank you very much for your suggestions!

[Damiano Testa]

Looking for trouble: this does not work for the same reason as the one above

notation α`🐙` := rel_with (0 : α) (<)

#check ℕ🐙  --works

-- however this does not
lemma pnat_eq_new : pnat = ℕ🐙 := rfl

so the > symbol was not actually relevant.

[kana]

It doesn't work because of priority,
check this

notation α`🐙` := α ∧ α
set_option pp.notation
#check ℕ = ℕ🐙
-- ℕ = ℕ ∧ ℕ = ℕ : Prop

Just add more priority

notation α`🐙`:1024 := α ∧ α

[Damiano Testa]

kana, thank you so much! This does indeed work!!

notation α`>₀`:1024 := rel_with (0 : α) (<)

#check ℕ = ℕ>₀  --works

lemma pnat_eq_new : { n : ℕ // 0 < n } = ℕ>₀ := rfl  --also works!

[Floris van Doorn]

I suggest using 1025 or higher as number, so that option ℕ>₀ is option (ℕ>₀) and not (option ℕ)>₀

[Damiano Testa]

So, as long as subscripts for ≥ and > are available, I think that my current favourites are ≥₀ and >₀. Any further thoughts?

[Floris van Doorn]

The 0 really looks like it's modifying the inequality though, but maybe that's the best we can do for now...

[Damiano Testa]

On paper, I would write $\mathbb{N}_{\ge 0}$, for sure...

[Floris van Doorn]

yeah, that would be nice

[Eric Wieser]

Another way you can play this game:

notation α `ː`:1025 f := subtype (f : α → Prop)

#check ℕ = ℕː(>0)  --works

lemma pnat_eq_new : { n : ℕ // 0 < n } = ℕː(>0) := rfl  --also works!

[Eric Wieser]

Or even

-- I doubt this is a good idea
instance : has_coe_to_fun Type* := ⟨_, λ α (p : α → Prop), subtype p⟩
lemma pnat_eq_new' : { n : ℕ // 0 < n } = ℕ(>0) := rfl

[Damiano Testa]

Eric, those are good suggestions as well! I think that I still prefer the other options, mostly since it involves fewer characters when writing the type.

[Yaël Dillies]

Do you ultimately want to yet the notation ℕ+ out of existence?

[Eric Wieser]

The advantage of the subtype approach is the notation works for (<0), (>1), and even even!

[Damiano Testa]

I do not have in mind of replacing old notation, I simply wanted to have a convenient way of talking about positive/non-negative elements for the order refactor. I want to be able to say easily that multiplying by the non-negative elements is monotone, by the positive one is strictly monotone and so on. Of course, I can say it without the notation, but accompanying this by a clear symbol seems useful!

[Damiano Testa]

Eric, I actually like your suggestion, though I think that maybe both should be available: I see myself using more often the >0 case than the general one and it would be nice if that one had a short, informative notation, in my opinion.

[Damiano Testa]

For instance, this works (which is great!):

open_locale nnreal

lemma nnreal_eq_new : ℝ≥0 = ℝː(≥0) := rfl  --also works!

Maybe, it makes sense to replace the notation for nnreal so that it picks this one up?

Floris' objection was that you could not then use 1>0, though, really this is bad form for two reasons:

• it uses >;
• it does not leave spaces around >.

What do you think?

[Damiano Testa]

Concretely, how about making these definitions:

notation α `ː`:1025 f := subtype (f : α → Prop)
notation α `≥0`:1025 := subtype ((≥0) : α → Prop)
notation α `>0`:1025 := subtype ((>0) : α → Prop)

and then there is no need to define nnreal as a special entity: it already means the right thing.

[Patrick Massot]

I really think we should be able to keep writing ∀ ε > 0. I don't mind being forced to use spaces around > but I'm afraid this will create inconsistencies and confusing error messages.

[Damiano Testa]

Actually, Patrick, at the moment the spaces seem to be ignored, so also using them causes problems. Back to looking for a solution!

[Damiano Testa]

Hmm, maybe I take it back. This works:

import data.real.basic

notation α `ː`:1025 f := subtype (f : α → Prop)
notation α `≥0`:1025 := subtype ((≥0) : α → Prop)
notation α `>0`:1025 := subtype ((>0) : α → Prop)

instance : has_zero ℝ≥0 := ⟨⟨0, rfl.le⟩⟩

lemma eps {ε : ℝ≥0} (h : ε > 0) : 0 < ε := h

Note that these are all the imports and there is no open_locale nnreal.

[Damiano Testa]

The error here

example {ε : ℝ} : ε>0 := sorry

is

type expected at
  ε
term has type
  ℝ

[Eric Rodriguez]

notation tokens ignore spaces iirc, like if you write notation α` ≥0 `:1025 := <blah> it just basically tells the pretty-printer to use the spaces around it when displaying it, but lets you type it in without them

[Damiano Testa]

Indeed, these two give errors:

example {ε : ℝ} : ε>0 := sorry -- error
example {ε : ℝ} : ε >0 := sorry -- error

while

example {ε : ℝ} : ε > 0 := sorry -- ok
example {ε : ℝ} : ε> 0 := sorry -- ok

do not

[Damiano Testa]

The conclusion is that if you maintain > and 0 separate by a space, you split the token and you do not pick up the subtype notation.

I personally find this acceptable, though I maybe not everyone does...

[Damiano Testa]

Unless I am mistaken, there seem to be 45 uses of >0 in the current master (many of which in doc-strings) and, the only uses of ≥0 are in ℝ≥0 (possibly continuing to ℝ≥0∞).

[Damiano Testa]

Here is a proposal (and note that I do not feel strongly in favour, although it does seem nice notation and somewhat useful).

Define

notation α `ː`:1025 f := subtype (f : α → Prop)
notation α `≥0`:1025 := subtype ((≥0) : α → Prop)
notation α `>0`:1025 := subtype ((>0) : α → Prop)

and get rid of the special notation for nnreal, since now it is a special case of this one.

Also, this will enforce using > 0 and ≥ 0, rather than >0 and ≥0 (emphasis on the space), when you really mean the inequality, as the alternative would give an obscure error.

Feel free to thumbs up if you like, thumbs down if you do not!

[Damiano Testa]

I attempted this change and the main issue that I found was that it got tricky to use the nnreal namespace, since Lean would often want it to be subtype instead. This (and especially Mario's thumb down), makes me skeptical of this approach.

I still might give a try to Eric's

notation α `ː`:1025 f := subtype (f : α → Prop)

for types of non-negative/positive elements.

Mario, what do you think about this?

[Kyle Miller]

This idea to have new notation for subtype is fascinating, especially since it can pair well with slices of relations and other predicates. For what it's worth, it seems that & is free to use, and it's somewhat mnemonic:

notation α `&`:1025 f := subtype (f : α → Prop)

def posnat := ℕ&(≥1)
-- "natural and greater than or equal to 1"
def evennat := ℕ&even
-- "natural and even"

[Kyle Miller]

Or, dual to @Eric Wieser's suspect idea, I'll throw in my own:

instance {α : Type*} : has_coe_to_sort (α → Prop) := ⟨_, λ f, subtype f⟩

def posreal : Type := (≥(1:ℝ))

(please don't do this :smile:)

[Mario Carneiro]

I think that using ≥0 alone to mean subtype is way too implicit. Everyone knows that it means "greater than or equal to zero" so this overloading is going to cause confusion. : is problematic because it is used to mean typing in binders and in type ascription. & is sufficiently strange that I would only want it to be a local notation so that the reader is constantly reminded what it means

[Mario Carneiro]

I think the best notation is {x // x≥0}

[Mario Carneiro]

for particular subtypes that have names like ennreal it makes sense to have a dedicated notation, but subtype already has a notation

[Kyle Miller]

Mario Carneiro said:

: is problematic because it is used to mean typing in binders and in type ascription

I'd thought so, too, but you have to zoom in to ː or get your text editor to tell you it's MODIFIER LETTER TRIANGULAR COLON

[Damiano Testa]

I am happy to use the & in a special locale. Eventually, my hope would be to use this under the hood, for proving the basic stuff about inequalities, but that it would be seen as an explicit positivity assumption in "externally applied" lemmas.