Zulip Chat Archive

Stream: general

Topic: function namespace


view this post on Zulip Johan Commelin (May 07 2020 at 07:05):

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.

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 07:17):

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

view this post on Zulip Gabriel Ebner (May 07 2020 at 07:56):

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.

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 08:00):

What do you mean by 1) and 2)?

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 08:04):

Can we differentiate between pi and function here?

view this post on Zulip Gabriel Ebner (May 07 2020 at 08:14):

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?

view this post on Zulip Johan Commelin (May 07 2020 at 08:18):

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

view this post on Zulip Johan Commelin (May 07 2020 at 08:18):

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

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 08:20):

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

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 08:20):

Instead of doing this in Lean.

view this post on Zulip Johan Commelin (May 07 2020 at 08:20):

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

view this post on Zulip Johan Commelin (May 07 2020 at 08:20):

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

view this post on Zulip Kenny Lau (May 07 2020 at 08:21):

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

view this post on Zulip Kenny Lau (May 07 2020 at 08:22):

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

view this post on Zulip Gabriel Ebner (May 07 2020 at 08:22):

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.

view this post on Zulip Kenny Lau (May 07 2020 at 08:22):

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


Last updated: May 13 2021 at 06:15 UTC