function namespace

Stream: general

[Johan Commelin]

I fear this is impossible, but I don't actually know why. Could

1. X → Y be notation for function X Y, and
2. function X Y be an abbreviation for whatever Pi-type it should be.

Then we could write (hf : f.injective) if I'm not mistaken.

[Yury G. Kudryashov]

I'd love to have this. I don't know if it's easier to implement this in Lean, or in C++.

[Gabriel Ebner]

1) seems like a really bad idea, 2) is extremely easy to do, you just need to add a case for is_pi here: https://github.com/leanprover-community/lean/blob/675c47294a57c98e3215b6edd9e7efc80ec99475/src/frontends/lean/elaborator.cpp#L2728
I think we should also have this for Sort.

[Yury G. Kudryashov]

What do you mean by 1) and 2)?

[Yury G. Kudryashov]

Can we differentiate between pi and function here?

[Gabriel Ebner]

1) and 2) refer to Johan's questions.
Oh, function is supposed to be a non-dependent pi! My advice still stands: 1) is probably a bad idea, 2) is easy and should be done. You could differentiate between pis and non-dependent pis, for example you could try function.injective if it is non-dependent as well as pi.injective. I'm not sure if this difference is important. Do you want different definitions for pis and non-dependent pis?

[Johan Commelin]

But if we don't have 1), what is the benefit of 2)?

[Johan Commelin]

We can't write f.injective for f : X → Y in that case, right?

[Yury G. Kudryashov]

Gabriel pointed to C++ source file where we can hardcode "if you see a function, try function namespace".

[Yury G. Kudryashov]

Instead of doing this in Lean.

[Johan Commelin]

Aah, I see. We add a hack (-;

[Johan Commelin]

@Gabriel Ebner Can you also explain why 1) is a bad idea?

[Kenny Lau]

why not just write f : X \hom Y and f.injective

[Kenny Lau]

or whatever unicode variant of the arrow that hasn't been used

[Gabriel Ebner]

This is more a gut feeling. But adding definitions typically breaks stuff. For example defining (≥) as flip (≤) breaks the simplifier. I would imagine many similar things to happen if → was suddenly no longer a pi.

[Kenny Lau]

my point is, there's no need to change \to

[Yaël Dillies]

I see there already has been discussion about this, but it seems that my idea didn't come up.

[Yaël Dillies]

Could we have the identifier resolver (or whatever thing does this) try to append function. when we use dot notation on f : α → β?

[Yaël Dillies]

Dot notation-wise, this is the same as having α → β meaning function α β, but without needing to redefine it.

[Yaël Dillies]

I don't know whether we want that more generally on Pi-types.

[Eric Wieser]

Should it be function or pi?

[Eric Wieser]

Maybe the rule should be try one then the other?

[Yaël Dillies]

I guess it could try both?

[Eric Wieser]

In the same way that abbreviation foo : Type* = bar will do dot notation first on foo then on bar

[Anne Baanen]

We also have a couple of definitions on Pi by the way: docs#Pi.topological_space, docs#Pi.complete, ...

[Yakov Pechersky]

We have many objects that coerce to function arrows. How would dot notations operate on those?

[Anne Baanen]

Presumably it will work analogously to the current way dot notation works on coercions: ((f : A →foo B) : A → B).injective is function.injective ⇑f and f.injective is foo_hom.injective f.

[Johan Commelin]

What? Since when does function support dot-notation? :shock:
I must have been living under a rock.

[Yaël Dillies]

Wait what? This is exactly what I'm asking for!

[Anne Baanen]

The discussion is about whether to add dot notation, and how it should work. I don't think it actually works yet.

[Yaël Dillies]

Or is Anne's message supposed to be conditional?

[Yaël Dillies]

AH yes

[Johan Commelin]

/me should learn to read :see_no_evil:

[Anne Baanen]

Indeed:

example {α β : Type*} (f : α → β) : f.injective := _ -- error, `α → β` is not of the form `(C ...)`

[Anne Baanen]

Sorry for any confusion, hopefully the edit makes the hypothetical nature clearer

[Moritz Doll]

There is still no way to get dot notation for functions, right? I would also love to have something like this

import data.real.basic

variables {α : Type*}
variables (f : α → ℝ)

abbreviation foo := α → ℝ

lemma foo.test (f : α → ℝ) : Prop := sorry

#check f.test --fails of course

where the notation works for any α.

[Eric Wieser]

What's f on that last line? I don't see a variables.

[Moritz Doll]

edited. Sorry, I deleted one line too much from my other experiments

[Moritz Doll]

The context is that I want to refactor the with_seminorms part in analysis.seminorm.

[Eric Wieser]

Does (f : @foo α) work there?

[Moritz Doll]

#check (f : @foo α).test fails with the same error:

invalid field notation, type is not of the form (C ...) where C is a constant
  f
has type
  α → ℝ

[Eric Wieser]

I mean declare f with that type

[Moritz Doll]

yes, that works. Thank you. Why does that make a difference?

[Leonardo de Moura]

I didn't read the whole thread, but the following works in Lean 4.

def Function.injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂

theorem Function.injective.comp {g : β → φ} {f : α → β} (hg : g.injective) (hf : f.injective) : (g ∘ f).injective :=
  fun a₁ a₂ h => hf (hg h)

[Eric Rodriguez]

is there any other "special" namespaces? does pi/forall work for ∀ x, _?

[Leonardo de Moura]

@Eric Rodriguez No, but they can be added if there are useful in practice.

[Kyle Miller]

Great, I was going to ask about this -- I'll backport it to Lean 3.

[Kevin Buzzard]

Dot notation is something which I have really begun to love. Five minutes ago I just proved I \sub J from h : I = J using h.subset and about an hour ago I proved a <= b from h : a = b using h.le. Now I've "got the hang of it" I had started to get frustrated that I couldn't do the same trick with functions :-)

[Leonardo de Moura]

@Kyle Miller There is also a new form of dot notation in Lean 4 inspired by Swift that we are currently in love with. We can write

def f (x : Nat) : Except String Nat :=
  if x > 0 then
    .ok x  -- Sugar for `Except.ok x`
  else
    .error "x is zero" -- Sugar for `Except.error "x is zero"`

The namespace is inferred from the expected type.

[Kyle Miller]

@Leonardo de Moura Does that mean dot notation is whitespace sensitive now? In Lean 3 you can do x .foo, which can be potentially useful when you have long lines you need to split, but it's not so important since you can't really chain dot notation like you can method calls in most OO languages due to syntax.

[Yaël Dillies]

It already is, Kyle. You can add whitespaces to disambiguate chained dot notation and genuine namespacing.

[Kyle Miller]

@Yaël Dillies That might be one kind of chained "method call" (for nullary methods), but Lean doesn't support anything like x.foo(a,b).bar(c,d,e).baz(), which is what I was referring to. It's common to see this sort of chaining where each additional method call gets its own line.

[Eric Rodriguez]

fond memories of C#'s LINQ

[Eric Rodriguez]

13-year old me loved that stuff

[Sebastian Ullrich]

@Kyle Miller That's x.foo a b |>.bar c d e |>.baz in Lean 4

[Leonardo de Moura]

@Kyle Miller Yes, it is. However, in Lean 4, the projection notation never allowed whitespaces between x and .foo.

[Kevin Buzzard]

Lean 4 is going to be so cool :-)