Zulip Chat Archive

Stream: new members

Topic: chained inequalities ?


view this post on Zulip Dan Abolafia (Mar 29 2020 at 18:14):

It would be convenient to be able to write n < m <l instead of n < m ∧ m < l. Is that possible?

example

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 18:16):

It's not currently possible -- indeed I remember spending a very long time trying to work out what was going on in some code by an undergraduate until I finally realised that they had written this. Currently it compiles to something like (n < m) < l and then complains that it doesn't know what it means for a proposition to be less than a number. In fact given that the syntax is perfectly valid it might be hard to get what you want to work.

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 18:16):

PS take a look at https://leanprover-community.github.io/ and in particular note that there is a far more modern web editor at https://leanprover-community.github.io/lean-web-editor/

view this post on Zulip Dan Abolafia (Mar 29 2020 at 18:20):

Ah thanks for letting me know. https://leanprover.github.io/theorem_proving_in_lean/ should be updated then. I was using the web editor it links to in the examples.

view this post on Zulip Mario Carneiro (Mar 29 2020 at 21:55):

I recall @Sebastian Ullrich playing with syntax of this kind in lean 3 and lean 4

view this post on Zulip Reid Barton (Mar 29 2020 at 21:56):

Python has this syntax even though (n < m) < l is also perfectly sensible in Python.

view this post on Zulip Sebastian Ullrich (Mar 31 2020 at 10:57):

I don't quite recall anything about Lean 3, but in Lean 4 adding a specific chain is of course trivial:

macro_rules `($a < $b < $c) => `($a < $b  $b < $c)
#check 1 < 2 < 3
#check 1 < 2 < 3 < 4

This should probably be automated to auto-generate rules for pairs of operators, though maybe not all pairs? As an undergrad, I was actually shocked to learn that mathematicians write a ≠ b ≠ c and mean pairwise inequality by that. The following rule implements that, though with a good deal of duplicated clauses in the output.

macro_rules `($a  $b  $c) => `($a  $b  $a  $c  $b  $c)
#check 1  2  3  4  5  -- ((1≠2∧1≠3∧2≠3)∧(1≠2∧1≠4∧2≠4)∧3≠4)∧((1≠2∧1≠3∧2≠3)∧(1≠2∧1≠5∧2≠5)∧3≠5)∧4≠5 : Prop

view this post on Zulip Mario Carneiro (Mar 31 2020 at 11:09):

I would be curious whether the mathematicians in the chat agree or disagree with this interpretation of chained disequality

view this post on Zulip Mario Carneiro (Mar 31 2020 at 11:10):

(here, let's make it a poll: vote this comment up if you agree that chained disequality is pairwise, down if you think it should only be the adjacent pairs)

view this post on Zulip Johan Commelin (Mar 31 2020 at 11:15):

I just avoid it, because I think it's ambiguous...

view this post on Zulip Johan Commelin (Mar 31 2020 at 11:16):

On the other hand.... A    B    CA \iff B \iff C also means pairwise iff in maths, and that's not what it means in Lean...

view this post on Zulip Mario Carneiro (Mar 31 2020 at 11:19):

Well, for iff it could mean either pairwise or adjacent pairwise since they are the same

view this post on Zulip Mario Carneiro (Mar 31 2020 at 11:20):

Lean's interpretation, nested iff, is never what mathematicians mean (unless you put parentheses in)

view this post on Zulip Mario Carneiro (Mar 31 2020 at 11:21):

which reminds me of a funny theorem: iff is associative, but the proof requires classical logic

view this post on Zulip Kenny Lau (Mar 31 2020 at 11:23):

Rule 1: only write chained relation for transitive relations

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 11:28):

If I want to say a,b,ca,b,c are pairwise distinct I usually say abcaa\ne b\ne c\ne a.

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 11:29):

You only find yourself saying this sort of thing when you're doing Olympiad style problems though I think?

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:35):

I would never write abca \neq b \neq c.

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:38):

@Sebastian Ullrich is it still time to implore you and Leo to stop using     \implies when you mean \mapsto? It almost made it impossible for me to read the macro paper. We can get over Lean using \to when we would write     \implies, but writing     \implies instead of \mapsto is much much worse. What's wrong with \mapsto? I don't know any other interpretation of that symbol, and you can ascii art it if you really want to.

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:39):

I think that if mathematicians were offered to choose one notation to change in Lean 4 that would be this notation. Seriously, we don't care at all about CamelCase, we'll get used to it in one afternoon.

view this post on Zulip Sebastian Ullrich (Mar 31 2020 at 11:39):

What? It's \Rightarrow, not \Longrightarrow. Completely different.

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:40):

Please :pray:

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:41):

Where does this crazy use of \Rightarrow comes from anyway?

view this post on Zulip Sebastien Gouezel (Mar 31 2020 at 11:42):

It's javascript syntax, right?

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:42):

Even the weird use of := in the equation compiler was better.

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:43):

Oh, great. We already have Coq developers coming here to tell us Lean is the PHP of proof assistants and now they'll be able to add it's also javascript.

view this post on Zulip Marc Huisinga (Mar 31 2020 at 11:46):

the camelCase / PascalCase change is actually pretty cool, you get less name collisions between functions/variables and types!

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:47):

I think it's not yet clear whether lemma names will keep their snake case. I saw a lemma using PascalCase at some point. But this is completely irrelevant compared to \mapsto.

view this post on Zulip Sebastian Ullrich (Mar 31 2020 at 11:50):

So merely for historical context, Lean's syntax is somewhat inspired by ML, which has fn ... => and case ... =>

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:51):

I thought Lean was only getting good ideas from the past, without being hampered by backward compatibility?

view this post on Zulip Sebastian Ullrich (Mar 31 2020 at 11:56):

Actually, to be more specific this is 1:1 Coq syntax, which of course is itself derived from ML

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:57):

So maybe we should send Kevin to the Coq mailing lists to write that Coq is the javascript of proof assistants.

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:58):

In the mean time one get one more cheap way to make sure mathematicians will never be tempted to use Coq instead of Lean: use \mapsto.

view this post on Zulip Marc Huisinga (Mar 31 2020 at 11:58):

Patrick Massot said:

I don't know any other interpretation of that symbol, and you can ascii art it if you really want to.

⊢>

view this post on Zulip Sebastian Ullrich (Mar 31 2020 at 12:00):

I'm not sure yet I want to commit to this discussion, but as for , I don't see any satisfactory ASCII syntax. |-> is terrible.

view this post on Zulip Patrick Massot (Mar 31 2020 at 12:01):

Do you really need ASCII?

view this post on Zulip Patrick Massot (Mar 31 2020 at 12:01):

What's the point?

view this post on Zulip Patrick Massot (Mar 31 2020 at 12:01):

If it's only for the very early bootstrapping then you could use the ugly |-> in a couple of files.

view this post on Zulip Marc Huisinga (Mar 31 2020 at 12:02):

i think => is one of the most commonly typed symbols in lean4

view this post on Zulip Sebastian Ullrich (Mar 31 2020 at 12:02):

Writing in this chat without copying from Emacs, for example. I think people regularly use ASCII in this case.

view this post on Zulip Patrick Massot (Mar 31 2020 at 12:02):

Sure (at the moment since there is not yet any maths written in Lean 4), but could it be typed in unicode?

view this post on Zulip Patrick Massot (Mar 31 2020 at 12:03):

Sebastian, there are plenty of browser extensions allowing to use any editor to edit textarea inputs.

view this post on Zulip Sebastian Ullrich (Mar 31 2020 at 12:04):

To be honest, I've thought about reverting the paper syntax back from to =>, since that is what we're actually writing. fun isn't very mathematical for a start, so maybe => is simply more adequate.

view this post on Zulip Patrick Massot (Mar 31 2020 at 12:06):

fun x ↦ f(x) would be understood immediately, although we don't write "fun" on paper.

view this post on Zulip Patrick Massot (Mar 31 2020 at 12:07):

And I agree the paper would be less painful to read with ascii art => which somehow indicates this is not \Rightarrow.

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 12:08):

Mathematicians are missing lots of symbols -- we don't have \subset or subseteq or \le and we just write the shortcuts in the chat. Shortcut it to \R or something and forget it?     \implies means something important in maths.

view this post on Zulip Sebastian Ullrich (Mar 31 2020 at 12:12):

So... everyone would be semi-happy to happy with ASCII fun ... =>? You are very welcome to introduce x ↦ f(x) as alternative syntax.

view this post on Zulip Patrick Massot (Mar 31 2020 at 12:13):

Having xf(x)x \mapsto f(x) being the primary syntax would be much much better. Because every new user will end up meeting the WTF version by navigating files or reading papers.

view this post on Zulip Johan Commelin (Mar 31 2020 at 12:23):

Let me give a big vote for \mapsto, aka .

view this post on Zulip Marc Huisinga (Mar 31 2020 at 13:34):

do you like \mapsto for term mode proofs, too? in my mind, \mapsto is reserved for functions over data

view this post on Zulip Patrick Massot (Mar 31 2020 at 13:36):

Here the Lean 3, assume fact, ... is much more natural. \mapsto would indeed feel weird, but \Rightarrow would be worse!

view this post on Zulip Marc Huisinga (Mar 31 2020 at 13:42):

judging from many of the questions here of people working through TPIL, assume is perhaps too natural - beginners seem to struggle with disconnecting their intuitions about assumptions from the formal meaning of assume in lean. it's also pretty verbose, to the degree where i always see people using \lam over assume in practice.

view this post on Zulip Patrick Massot (Mar 31 2020 at 13:48):

It's true that I use \lambda in practice, because it doesn't mean anything, so why not using it both for introduction and function creation. The situation is very different with hijacking \Rightarrow because it already means something.

view this post on Zulip Marc Huisinga (Mar 31 2020 at 13:50):

i think lean4 also tries to get rid of the comma in most places

view this post on Zulip Mario Carneiro (Mar 31 2020 at 13:52):

In ML, lists are written [a; b; c], while [a,b,c] means [(a,b,c)]. This really throws me off

view this post on Zulip Mario Carneiro (Apr 06 2020 at 21:15):

Looks like got removed, leaving only the ascii syntax => for lambda. The drama continues

view this post on Zulip Patrick Massot (Apr 06 2020 at 21:28):

I think it's more important not to use everywhere for something else than implication than to use unicode.

view this post on Zulip Patrick Massot (Apr 06 2020 at 21:28):

So I see this as an improvement.

view this post on Zulip Mario Carneiro (Apr 06 2020 at 21:29):

I still don't understand what's wrong with ,

view this post on Zulip Sebastian Ullrich (Apr 07 2020 at 10:17):

Mathematicians might not like the arrows, meanwhile computer scientists constantly complained to Leo that Lean's programming syntax looks wonky, including that weird comma that is without precedent from other languages. That's why Lean 4's (programming) syntax is now much closer to other programming and ITP languages. See also naming convention, Agda-like dependent arrows, ...

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 10:33):

Ever since Kenny told me I had to use \le and not \subseteq for ideals of a ring, I knew we were going to have to start adapting.

view this post on Zulip Scott Morrison (Apr 07 2020 at 10:43):

↦, what's not to love? It's an arrow, making computer scientists happy, and it's the arrow that mathematicians already use for lambdas, making mathematicians happy.

view this post on Zulip Sebastian Ullrich (Apr 07 2020 at 13:33):

Well, what about match? It uses the same => in Lean 4, since := makes zero sense at that position.

view this post on Zulip Patrick Massot (Apr 07 2020 at 13:46):

What's the problem with ↦ in match?

view this post on Zulip Patrick Massot (Apr 07 2020 at 13:47):

Anyway, I hope you and Leo didn't spend too much time discussing this. Notations are important, but much less than moving Lean 4 forward.

view this post on Zulip Sebastian Ullrich (Apr 07 2020 at 14:41):

Patrick Massot said:

What's the problem with ↦ in match?

In match it has no precedent in either programming or math! IOW: it looked plain silly to us.

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 14:42):

I'm sure that whatever happens, we'll be able to parse our way out :-)

view this post on Zulip Johan Commelin (Apr 07 2020 at 14:43):

That's because in maths you write

f(x)={37if x=00otherwise.f(x) = \begin{cases} 37 & \text{if $x = 0$} \\ 0 & \text{otherwise.} \end{cases}

view this post on Zulip Sebastian Ullrich (Apr 07 2020 at 14:47):

Well, this discussion did lead to a change, so it wasn't completely moot. Specifically, it makes sure the category people can still use that Unicode arrow without breaking match. But regarding fun x ↦, I'll just reiterate that I'm fine with somebody declaring an alternative math syntax x ↦ to the programming syntax fun x =>, but I'm very much not fine with creating an unholy mix of the two and making it the default.

view this post on Zulip Sebastian Ullrich (Apr 07 2020 at 14:48):

@Johan Commelin I feel like the hardest part of defining that in Lean 4 will be coming up with a reasonable approximation to the big curly bracket :)

view this post on Zulip Johan Commelin (Apr 07 2020 at 14:50):

In this case, I prefer what the computer scientists do (i.e., put the conditions first and the definitions afterwards). Of course mathematicians can have pretty sophisticated cases that aren't constructors of an inductive type.
But for inductive types, the way match works is fine for me.

view this post on Zulip Johan Commelin (Apr 07 2020 at 14:51):

Still, I would think

def f : nat  nat
| 0      37
| (n+1)  0

is pretty intuitive.

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 14:51):

I just learnt that ```latex exists from this thread :-)

view this post on Zulip Johan Commelin (Apr 07 2020 at 14:52):

You just have to remember that should be read out loud as "maps to"


Last updated: May 16 2021 at 05:21 UTC