ation

Stream: general

[Alex J. Best]

I prepared a demo for mathematicians recently and in the process of trying to make it look more readable I noticed that there are many negations of relations that show up that we display using the not symbol. For many of these there exists a unicode symbol for the negation that we do not make use of.
For example we often talk of congruence using the symbol ≡ so that non-congruence is written as ¬ a ≡ b, I'd propose we add something like

local notation3 a " ≢ " b "[ZMOD " p "]" => ¬ a ≡ b [ZMOD p]

so we may use a ≢ b instead. In many cases these notations are already in the vscode extension.
if we do this I would be happy to investigate the correct way of adding this notation so that it has good properties (e.g. such as using binop if needed).

I propose we add some of these notations to mathlib, to make statements and goal states look closer to mathematics, and therefore clearer to new lean users but also ideally closer to our thought processes even if we are already used to using not everywhere (and easier to type!)
Note that I propose we add these as notations, not as defs like Ne, as its unclear if there are any practical advantages to having separate defs or notation typeclasses (such as like using namespaced lemmas in these situations), and adding defs seems an additional complication.
The disadvantage of these notations would likely be the lack of clarity for the end user about what the term the noation denotes actually is (this is the case with most notations of course), I would hope that a clear docstring that shows up on hover mitigates this.

In the below poll I've listed 3 options for how many of these we want to add based somewhat on how common they are in paper maths, I'd of course be happy if discussion took place before people start voting. Note that its hard to be precise about the difference between the two "add them" options, but it would be good to have some sense of whether people support this in limited situations or more widely.
I encourage you to look at these symbols also in vscode to get a feel for how they look with your font.

p.s. the thread title is an attempt at a joke, not a typo :wink:

[Alex J. Best]

/poll to what extent should we add notations for negations of existing notation to mathlib?
do not introduce any of these notations
introduce those most commonly seen in mathematics, e.g. a ≢ b [ZMOD p ], ∤ (this looks odd in my zulip but fine in vscode), ∉ ≇ ≄``⊈
introduce all possible notations allowed in unicode where we already make use of the unnegated symbol e.g. including the above but also things like ∄ ≰ ≮ ↛ ⋪ ↮ ↚

[Kevin Buzzard]

I'm very pro this idea.

[Martin Dvořák]

We already have ∉ afaik.

[Pedro Sánchez Terraf]

Alex J. Best said:

/poll to what extent should we add notations for negations of existing notation to mathlib?
do not introduce any of these notations
introduce those most commonly seen in mathematics, e.g. a ≢ b [ZMOD p ], ∤ (this looks odd in my zulip but fine in vscode), ∉ ≇ ≄``⊈
introduce all possible notations allowed in unicode where we already make use of the unnegated symbol e.g. including the above but also things like ∄ ≰ ≮ ↛ ⋪ ↮ ↚

I've voted for the more consistent one, but I would like it restricted to relations and not for quantifiers/binders.
EDIT: I was completely careless with my reading, and only realized about negated implications after reading Mario's message below.

[Eric Wieser]

I asked for this with Exists before, but it had some font issues

[Mario Carneiro]

I don't think there is a problem with defining these notations, but I would be against pretty printing and/or using many of them

[Mario Carneiro]

having every occurrence of ¬(a → b) get pretty printed as a ↛ b would be cool for about 5 minutes and would be a readability hazard thereafter

[Damiano Testa]

Could we have a math locale where these are in scope?

[Mario Carneiro]

I would prefer a recommendation along the lines "never pretty print using them, and use them 'tastefully' in code (when the usage is especially common in a sequence of theorems, or in a theorem intended mainly for presentation)"

[Damiano Testa]

With respect to negation, I am now used to the symbol, but I had to "refresh" it, when I first used Lean. Same for ∧ and ∨, btw.

[Damiano Testa]

In any case, while all these logic symbols are a hindrance to using Lean for mathematicians, they are definitely the least difficult of the problems, when faced with formalization! :smile:

[Mario Carneiro]

on the subject of "things we could do but probably shouldn't", it's also possible to just use unicode combining slash as an alternative to ¬ for anything! Viva la n̷egation

[Mario Carneiro]

Damiano Testa said:

In any case, while all these logic symbols are a hindrance to using Lean for mathematicians, they are definitely the least difficult of the problems, when faced with formalization! :smile:

It's interesting that you say this, because mathematicians are usually the ones pushing the extensive use of unicode

[Damiano Testa]

I really like unicode, but all the logic symbols are completely unfamiliar, or at least were to me.

[Alex J. Best]

Mario Carneiro said:

having every occurrence of ¬(a → b) get pretty printed as a ↛ b would be cool for about 5 minutes and would be a readability hazard thereafter

Right, this is essentially what I was thinking of when I added the second option in the poll, I would agree myself that in the case of implies it is not particularly helpful to display the not implies symbol in the goal state. Adding the notations but not the delaborators in this case is a good suggestion though.

[Damiano Testa]

I had to dig up several mnemonics to remember what ¬, ∧ and ∨ meant. The implication arrows were ok, since they are fairly similar to the more familiar notation.

[Mario Carneiro]

Like I said, I really think we should try to use unicode 'tastefully'. The more entropy you put in each character, the higher the cognitive load when scanning text and also the better eyesight you need to have to distinguish characters. This is a serious issue, especially with stuff like | vs \| or -> vs -->

[Mario Carneiro]

most of the rest of the programming world (even the parts that have embraced unicode) has already cottoned on to this issue with unicode 'confusables', and I'm pretty sure we have to disable some warnings that vscode would normally give for lean text because we blatantly violate recommendations in this area

[Mario Carneiro]

now, negated symbols are not really the worst offenders here, but for example I would have difficulty differentiating ↛ and ⇝ at a comfortable viewing distance

[Mario Carneiro]

(actually, on zulip it's hard to even notice that the second arrow is squiggled)

[Eric Wieser]

Let's not forget that how these things render on GitHub is also important; we have to care about fonts in vscode, zulip, and GitHub, many of which are presumably platform-dependent.

[Eric Wieser]

(Unfortunately android still seems to be a lost cause... Maybe I need to find some strings to pull...)

[Jireh Loreaux]

Yeah, the lack of Unicode support on Zulip for Android is painful

[Pedro Sánchez Terraf]

I edited my message below and retracted my vote. My updated opinion is something like the second option but excluding all logical connectives and quantifiers: $\forall$ , $\exists$, $\to$, etc.
I'm making a new option, but perhaps this is just noise.

[Alex J. Best]

I think thats actually quite close to what I had in mind for the second one to begin with, which is why I put exists and rightarrow as examples for the last option. As far as I know there isn't a unicode not for all symbol either.

[D. J. Bernstein]

Damiano Testa said:

In any case, while all these logic symbols are a hindrance to using Lean for mathematicians, they are definitely the least difficult of the problems, when faced with formalization! :smile:

I wouldn't underestimate this hindrance. Consider, e.g., Appendix C.3 of https://cr.yp.to/papers/lprrr-20230317.pdf presenting a formalization of that paper's main theorem and comparing it line by line to the original statement of the theorem. In this context, unfamiliar notation generally requires explanation (e.g., the appendix says /\ is conjunction; there are a few corners of mathematics where this is standard notation modulo typography, but most mathematicians don't use it) and imposes a translation load on the reader that would have been avoided by familiar notation (e.g., and). Writing this comparison didn't add much to the time spent writing proofs, but for the _reader_ the proof-reading time is unimportant while the theorem-reading time is important.

[D. J. Bernstein]

For the specific question at hand, I think that a pretty-printer replacing ¬(... relation symbol ...) with a slashed relation symbol is an improvement in readability for most mathematicians, whether or not the relation symbol was familiar in the first place.