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 for Leibnitz equality and for the definitional one, while in Coq the tradition is rather the contrary.
I suggest something 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 an error in the presentation of formal systems. It must be implicit, otherwise nothing makes sense
but if you want, yes, and ...
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 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: Dec 06 2023 at 13:01 UTC