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

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.

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

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 α

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

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

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

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

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

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

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

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)

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

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

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.

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

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

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.

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

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?

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

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

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