Stream: Miscellaneous

Topic: Symbols for Leibniz, definitional, and syntactic equalities

Kazuhiko Sakaguchi (Nov 26 2021 at 02:29):

Are there any (standard) symbols for Leibniz, definitional, and syntactic equalities to distinguish in writing? Maybe =, ≡, and ≣ for each?

Meven Lennon-Bertrand (Nov 26 2021 at 10:06):

I fear this is not widely agreed upon… the Agda people often use $\equiv$ for Leibnitz equality and $=$ for the definitional one, while in Coq the tradition is rather the contrary.

Enrico Tassi (Nov 26 2021 at 10:21):

I suggest something $=_\beta$ for conversion, and $=$ for syntactic equality.
I don't think having to count the number of lines helps the reader, esp with small fonts

Pierre-Marie Pédrot (Nov 26 2021 at 10:23):

syntactic equality is actually α-conversion, so if you annotate conversion with β (which is only part of the rules btw) you should also annotate syntactic equality with α

Enrico Tassi (Nov 26 2021 at 10:23):

Also, I would use the small symbol for the most precise equality, and add sub/super scripts to include (quotient over) more staff, like computations or proofs

Enrico Tassi (Nov 26 2021 at 10:24):

ok, I consider $\alpha$ an error in the presentation of formal systems. It must be implicit, otherwise nothing makes sense

Enrico Tassi (Nov 26 2021 at 10:25):

but if you want, yes, $=_{\beta\alpha}$ and $=_\alpha$ ...

Paolo Giarrusso (Nov 26 2021 at 10:54):

Agree with Enrico, I'd only mention alpha if you're dealing with (non-hygienic) metaprogramming like macros in your metatheory

Kenji Maillard (Nov 26 2021 at 10:55):

Though conversion (at least in Coq and Agda) contains much more than $\beta$ nowadays, no ?

Paolo Giarrusso (Nov 26 2021 at 10:56):

Yes, but please don't add the Greek alphabet to your subscripts by default :-|

Karl Palmskog (Nov 26 2021 at 10:56):

you can add a subscript regexp maybe? E.g., =_{[\alpha-\omega]}

Paolo Giarrusso (Nov 26 2021 at 10:56):

BTW, even the idea that propositional equality is Leibniz equality seems Coq-specific, I've never heard it in Agda (and I'm honestly a bit skeptical for Coq)

Pierre-Marie Pédrot (Nov 26 2021 at 10:59):

@Paolo Giarrusso what do you mean exactly? Do you call Leibniz equality something else? I think that it should be restricted to the impredicative encoding of equality, which is weaker than propositional equality without UIP, but that's just an opinion.

Paolo Giarrusso (Nov 26 2021 at 11:01):

I guess we're talking of the same encoding, and yes that's more clearly Leibniz

Paolo Giarrusso (Nov 26 2021 at 11:05):

actually, that opinion seems supported by the literature: https://homepages.inf.ed.ac.uk/wadler/papers/leibniz/leibniz.pdf proves Leibniz equality and identity types are isomorphic under a bunch of assumptions — hence, a priori, they must be different definitions.

Paolo Giarrusso (Nov 26 2021 at 11:06):

and to clarify for others: I assume Pierre-Marie's talking about such an encoding of Leibniz equality:

image.png

which seems much closer to what Leibniz said:

Leibniz asserted the identity of indiscernibles: two objects are equal if and only if they satisfy the same properties

Paolo Giarrusso (Nov 26 2021 at 11:08):

Ah, the identification has ~30 years of history in the Coq literature: > Further, it is well known that Leibniz equality (a =. b) implies Martin-Löf identity (a ≡ b) and vice versa. Indeed, the former is sometimes taken as the name of the latter (Pfenning & Paulin-Mohring, 1989; Coq Developers, 2017). Here, to avoid confusion, we stick to calling each by its own name as defined above.

Paolo Giarrusso (Nov 26 2021 at 11:08):

But TLDR: "propositional equality" is probably less ambiguous (and more common than "identity type" IMHO)

Stefan Monnier (Nov 26 2021 at 15:15):

BTW, I don't quite understand the OP's question: I'd understand it in a non-Coq-specific context when talking about the symbols used in a paper, but within Coq code, I can't quite see how I could even talk about an equality more discerning than Leibniz's. Unless we're talking about Coq code used to model some other system (or something like MetaCoq)?
What am I missing?

Kenji Maillard (Nov 26 2021 at 15:18):

I would expect the OP to be interested in metaprogramming (tactics) in Coq so the choice of equality is relevant (for performance/correctness/etc).

Enrico Tassi (Nov 26 2021 at 17:40):

wild guess: paper on https://github.com/math-comp/algebra-tactics

Kazuhiko Sakaguchi (Nov 29 2021 at 06:40):

Thanks for the useful comments. To be clear, my main purpose to use syntactic equality is unfolding notations.

Last updated: Dec 06 2023 at 13:01 UTC