## 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 ?

#### 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: Aug 14 2022 at 11:02 UTC