Zulip Chat Archive

Stream: new members

Topic: chained inequalities ?


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

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.

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/

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.

Mario Carneiro (Mar 29 2020 at 21:55):

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

Reid Barton (Mar 29 2020 at 21:56):

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

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

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

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)

Johan Commelin (Mar 31 2020 at 11:15):

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

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...

Mario Carneiro (Mar 31 2020 at 11:19):

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

Mario Carneiro (Mar 31 2020 at 11:20):

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

Mario Carneiro (Mar 31 2020 at 11:21):

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

Kenny Lau (Mar 31 2020 at 11:23):

Rule 1: only write chained relation for transitive relations

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.

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?

Patrick Massot (Mar 31 2020 at 11:35):

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

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.

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.

Sebastian Ullrich (Mar 31 2020 at 11:39):

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

Patrick Massot (Mar 31 2020 at 11:40):

Please :pray:

Patrick Massot (Mar 31 2020 at 11:41):

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

Sebastien Gouezel (Mar 31 2020 at 11:42):

It's javascript syntax, right?

Patrick Massot (Mar 31 2020 at 11:42):

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

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.

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!

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.

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 ... =>

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?

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

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.

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.

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.

⊢>

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.

Patrick Massot (Mar 31 2020 at 12:01):

Do you really need ASCII?

Patrick Massot (Mar 31 2020 at 12:01):

What's the point?

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.

Marc Huisinga (Mar 31 2020 at 12:02):

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

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.

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?

Patrick Massot (Mar 31 2020 at 12:03):

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

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.

Patrick Massot (Mar 31 2020 at 12:06):

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

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.

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.

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.

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.

Johan Commelin (Mar 31 2020 at 12:23):

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

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

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!

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.

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.

Marc Huisinga (Mar 31 2020 at 13:50):

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

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

Mario Carneiro (Apr 06 2020 at 21:15):

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

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.

Patrick Massot (Apr 06 2020 at 21:28):

So I see this as an improvement.

Mario Carneiro (Apr 06 2020 at 21:29):

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

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, ...

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.

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.

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.

Patrick Massot (Apr 07 2020 at 13:46):

What's the problem with ↦ in match?

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.

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.

Kevin Buzzard (Apr 07 2020 at 14:42):

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

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}

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.

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 :)

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.

Johan Commelin (Apr 07 2020 at 14:51):

Still, I would think

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

is pretty intuitive.

Kevin Buzzard (Apr 07 2020 at 14:51):

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

Johan Commelin (Apr 07 2020 at 14:52):

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

Yaël Dillies (Apr 19 2022 at 16:25):

Marc Huisinga said:

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

... but you get more collisions between typeclasses and categories :sad:


Last updated: Dec 20 2023 at 11:08 UTC