Coq's equality is not Leibniz (?)

Using Rocq
1

Hello guys,

I just don’t understand why the docs (*) say that the built-in equality is Leibniz, when it seems evident to me that it’s plain definitional equality, i.e. x = y iff x and y are “convertible”, whence eq_refl applies:

Inductive eq (A : Type) (x : A) : A -> Prop :=
  eq_refl : eq x x.

For comparison, here is how I’d write Leibniz equality:

Definition leibniz_eq (A : Type) (x y : A) : Prop :=
  forall (p : A -> Prop), p x <-> p y.

What am I missing?

Julio

(*) “Reasoning with equalities”
https://coq.inria.fr/refman/proofs/writing-proofs/equality.html
but it’s also in many other places.

2

They’re equivalent:

Definition leibniz_eq (A : Type) (x y : A) : Prop :=
  forall (p : A -> Prop), p x <-> p y.

Lemma to A x y : x = y -> leibniz_eq A x y.
Proof.
  intros e. destruct e.
  unfold leibniz_eq. tauto.
Qed.

Lemma from A x y : leibniz_eq A x y -> x = y.
Proof.
  intros e.
  destruct (e (fun z => z = y)) as [_ e'].
  apply e';reflexivity.
Qed.

it seems evident to me that it’s plain definitional equality, i.e. x = y iff x and y are “convertible”

In the empty context (no axioms, no hypotheses) this is true (by canonicity). Also in an empty context a proof of leibniz_eq _ x y can only typecheck if x and y are convertible (since leibniz_eq and eq are equivalent).

However for instance if you have a context x : nat, y : nat, e : x = y the variables x and y don’t become convertible.
Similarly if you do eg Axiom x : nat. Axiom e : x = 0. the axiom x does not become convertible to 0.

1 Like
3

They’re equivalent [proofs follow]

Ah, wonderful… :slight_smile: Still “convertibility” seems fundamental, to those proofs (there is a rewrite behind that tauto) and not only to those proofs, as that’s indeed how the core language works fundamentally: so, I’d venture, the docs should rather say << in Coq the two notions boil down to being equivalent, since “convertibility” is essential to the core language, so there is in fact no Leibniz equality proper >>, i.e. rather explain that “Leibniz equality” is only truly relevant to contexts where that is the only fundamental tool available… no? Instead, the docs as well as comments in the standard lib do the exact opposite: they systematically call it Leibniz equality, which I am finding quite misleading.

it seems evident to me that it’s plain definitional equality, i.e. x = y iff x and y are “convertible”

However for instance if you have a context x : nat, y : nat, e : x = y the variables x and y don’t become convertible.

Whence, maybe I am still missing something (about the terminology to begin with), but I wouldn’t agree there: we can rewrite with that… IOW, by the very way inductive definitions work, eq/eq-refl provide a concrete representation of the underlying unification (as “convertibility”) mechanism.

4

Whence, maybe I am still missing something (about the terminology to begin with),

Convertibility (synonymously definitional equality) are about
https://coq.github.io/doc/master/refman/language/core/conversion.html
In a context with e : x = y it is not in general true that a term of type P x also has type P y, so x and y are not convertible.

5

In a context with e : x = y it is not in general true that a term of type P x also has type P y , so x and y are not convertible.

Sorry, I don’t understand how that applies, I was saying e is a proof that x and y are “convertible”, in particular with this in mind:

<< Equality is determined by converting both terms to a normal form, then verifying they are syntactically equal (ignoring differences in the names of bound variables by alpha-conversion. >> https://coq.github.io/doc/master/refman/language/core/conversion.html

Besides, here is another theorem, now saying that those P x and P y are in fact provably equal from that assumption:

Lemma eq_to_peq (U V : Type) (x y : U) :
  x = y -> forall (p : U -> V), p x = p y.
Proof.
  intros E p.
  rewrite E.
  apply eq_refl.
Qed.

[Edit: I have slightly adjusted the theorem statement.]

6

Besides, here is another theorem, now saying that those P x and P y are in fact provably equal from that assumption:

Provably equal is not the same as convertible so that’s irrelevant.

Equality is determined by converting both terms to a normal form, then verifying they are syntactically equal

The normal forms of variables x and y are x and y respectively, which are not syntactically equal. Therefore they are not convertible.

7

Provably equal is not the same as convertible so that’s irrelevant.

Since “equal” in Coq is “convertible”, I think that was quite relevant.

The normal forms of variables x and y are x and y respectively, which are not syntactically equal.

Yes, but nobody had said that x = y for arbitrary x and y, so I am not even sure we are talking about the same thing.

Never mind, I think I have made up my mind on this issue: and I just wish the docs were more to the point…

Thanks for your feedback, very much appreciated.

8

It is true that “equal means convertible” but for ground terms only: i.e. terms that have a normal form with no open variable in it. But during the process of an interactive proof you are “inside” a proof, with variables that are in the “proof environment” and have no ground term attached. And then equality is not conversion anymore.

In this environment

x y: nat
H: x = y
=============
P x y    <<--- x and y are free here

H states that we consider only cases where x and y are replaced by convertible terms, but x and y are not convertible themselves.
We could imagine a proof assistant where having x = y in the environent would make x and y convertible but this leads to a whole world of problems that expert could describe better than me.

1 Like
9

I just fail to understand that point: the only constructor for eq is eq_refl, which in turn means that we do have a proof that x and y unify, which in turn and more precisely in this context is called x and y are convertible.

Maybe I do need that expert explanation: not only I fail to see your point (unless it’s some terminological nitpicking that is above my rookie head: but no irony or scorn meant, I am really not understanding you), even more I fail to see how any of that justifies calling Coq’s equality Leibniz (!), which to me it patently isn’t: in fact, if anything, your observation seems to make things even more restrictive…

10

This is not true, I think you are not using the usual definition for “convertible”.

11

Indeed. “x and y are convertible” is not a property about natural numbers, or about nat. It is a property about two coq terms, so in fine about coq itself.

12

OK, eventually I see what you mean, and it’s a fine technical point: just, I wouldn’t read H that way. Allow me to try and rephrase the whole thing:

<< Coq has conversion rules that can be used to determine if two terms are equal by definition in CIC, or convertible. >>

I read that as: “equality” in CIC, whence the built-in eq in Coq, is synonym / realized-as / corresponds to “convertibility” (with the specific meaning/semantics as documented).

And I read H, by definition of eq as an inductive with the one constructor eq_refl as carrier of (specific) evidence, as stating that, whatever x and y are in the context, H is the assumption that we have a proof (evidence) that x and y (themselves) “unify”, i.e. are “convertible”… as well as e.g. rewrite is defined in those terms, etc.

And, you rightly object that “no, not x and y themselves, just the terms x and y stand for…” (pardon the simple paraphrase, conducive to my argument…), which I find literally correct but simply beside the point re the meaning / (operational) semantics of eq and how it can ever ever be called a Leibniz equality…!?

(Not to mention, the docs seem to say otherwise in almost as many places, maybe again, depending on the level of discourse… And, the equivalence proved initially by @SkySkimmer, which, maybe wrongly, but I have proposed is evidence that there is no Leibniz, namely Extensionality, at all in the core language: aka it’s a purely intensional language… but here I start speculating.)

13

1 = 0 is just a type (or a formula, if you do not care about the isomorphism). When you have it in your context as H: 1 = 0, it just means that you assume the existence of an element H of type 1 = 0 (or a proof of the formula). Does that mean that there really exists an element of type 1 = 0? Certainly not, since 0 and 1 are not convertible.

So, Coq’s equality is indeed Leibniz’ equality; if you have 1 = 0 in your context, from any formula P 1, you can deduce a formula P 0. Nothing more. In particular, “being convertible” is a property of the meta-logic, so you cannot replace P by is_convertible_to 1.

As already mentioned, it is only in the empty context that equality and convertibility conflate. But one hardly ever works in an empty context. In fact, more often than not, I perform my proofs ad absurdo, which means that I work in a context where all things are equal but certainly not convertible.

1 Like
14

If you mean Curry-Howard, yes, in fact I very much do, which is the reason why I feel entitled to literally read that formula as (a concrete representation of) the proposition “x (represents an object that) is equal to (an object represented by) y”, then the assumption to mean we assume having proof of it.

Does that mean that there really exists an element of type 1 = 0? Certainly not, since 0 and 1 are not convertible.

1 and 0 are not equal either, where I don’t see the relevance of that remark at all, indeed we assume false things at least as often as we assume true ones, which doesn’t change the meaning of propositions per themselves: e.g. in that example I’d say we are literally assuming that (we have proof that) “1 is equal to 0”.

So, Coq’s equality is indeed Leibniz’ equality; if you have 1 = 0 in your context, from any formula P 1, you can deduce a formula P 0. Nothing more. In particular, “being convertible” is a property of the meta-logic, so you cannot replace P by is_convertible_to 1.

OK, great, we are getting to the bottom of it: and to that I’d (humbly) counter that no, that is not Leibniz, indeed Leibniz is exactly the other way round, i.e. that from forall P, P x = P y we get x = y, while indeed I’d say the above is (substitution by) plain convertibility in action.

15

While 1 and 0 are never convertible, they can be equal, depending on the context. In particular, when doing a proof by contradiction, they are necessarily equal.

Do not confuse a property of the meta-logic (being convertible) with a property of the logic (being equal). As shown already multiple times in this thread, two objects can be equal without being convertible.

No, since 1 and 0 are not convertible, the ability to substitute 1 by 0 in P 1 is not due to plain convertibility.

16

The way you snip and reply instead of reasoning seems typical avoidance. Not only at this point I just disagree with you, I also must notice that you have especially avoided the Leibniz vs not Leibniz issue all along, and any other observations of mine. So, with all due respect, at this point I think you are plain wrong and the docs a plain mess… but I will also keep investigating this, there are indeed disciplines/niches where “up” is “down” just because they are using their own secret language, so that this is a terminological issue (where I think you are missing the point, though) remains a possibility.

17

I am not avoiding the Leibniz issue. I just know that it is impossible to convince you and thus that I am going to waste my time. But let me humor you one very last time.

A relation L is said to be Leibniz’ equality if it satisfies the following property: “Given any x and y, L x y if and only if, given any predicate P, P(x) if and only if P(y).”

But note that, if you know that, for any predicate P, you have “P(x) if and only if P(y)”, then just replace P with “R x”, and you get a proof of “R x y” from a proof of “R x x”. So, this direction of the implication is not really interesting, since you can use any reflexive relation R here, not just the equality L. (And since Coq’s inductive relation “eq” is obviously reflexive by definition, this is the case.)

So, what people really want from a relation that is supposed to be Leibniz’ equality is the other direction, that is the ability to perform a substitution of x by y inside any predicate P from a proof of “L x y”. So yes, Coq’s equality is Leibniz’ equality, since it makes it possible to perform such a substitution.

And it does so, even when the arguments are not convertible!

2 Likes
18

Which is pretty much what I said: but by all means, if you see fit. :wink:

A relation L is said to be Leibniz’ equality if it satisfies the following property: “Given any x and y, L x y if and only if, given any predicate P, P(x) if and only if P(y).”

One issue I am raising has indeed to do with the bi-implication:

<< Formally, the two principles can be expressed in the following way:

  1. The indiscernibility of identicals: forall x y, x = y -> forall F, F x <-> Fy
    For any x and y, if x is identical to y, then x and y have all the same properties.
  2. The identity of indiscernibles: forall x y, (forall F, F x <-> Fy) -> x = y
    For any x and y, if x and y have all the same properties, then x is identical to y.

Principle 1 is generally regarded as an a priori logical truth.
Principle 2, on the other hand, is controversial… >>
https://en.wikipedia.org/wiki/Identity_of_indiscernibles#Identity_and_indiscernibility

The latter I’d call a Leibniz/extensional equality, not the first, and lumping them under one and the same name I’d indeed call self-defeating to say the least.

And another and even more pressing issue is Coq’s reference documentation, which should be a technical reference manual, but altogether fails to even make clear, of the infinitely many possible levels of discourse that indeed there are, the one that is in fact relevant (to the programmer), i.e. the operational semantics and only the operational semantics that is attached to the language constructs…

And no, I am not humouring you…

19

Principle 2, on the other hand, is controversial

I think the statements need to be made more precise to explain why F z := x = z is not a valid instantiation, otherwise I can’t see how it can be controversial regardless of what some >50 years old citation says.

20

Isn’t the key here that coq admits the following rule:

eq X Y
---------
X = Y

That seems to me to be what makes eq “Leibniz”, and it is specifically enabled by the I in CIC , which is why it can be “controversial” in earlier accounts of equality ?

–
Ian