chained inequalities ?

Stream: new members

[Dan Abolafia]

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

example

[Kevin Buzzard]

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]

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]

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]

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

[Reid Barton]

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

[Sebastian Ullrich]

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]

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

[Mario Carneiro]

(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]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

Rule 1: only write chained relation for transitive relations

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

I would never write $a \neq b \neq c$.

[Patrick Massot]

@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]

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]

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

[Patrick Massot]

Please :pray:

[Patrick Massot]

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

[Sebastien Gouezel]

It's javascript syntax, right?

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Sebastian Ullrich]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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]

Do you really need ASCII?

[Patrick Massot]

What's the point?

[Patrick Massot]

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

[Marc Huisinga]

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

[Sebastian Ullrich]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Sebastian Ullrich]

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]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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]

Having $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]

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

[Marc Huisinga]

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

[Patrick Massot]

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

[Marc Huisinga]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

So I see this as an improvement.

[Mario Carneiro]

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

[Sebastian Ullrich]

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]

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]

↦, 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]

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

[Patrick Massot]

What's the problem with ↦ in match?

[Patrick Massot]

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]

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]

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

[Johan Commelin]

That's because in maths you write

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

[Sebastian Ullrich]

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]

@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]

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]

Still, I would think

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

is pretty intuitive.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Yaël Dillies]

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: