Coq's equality is not Leibniz (?)

I am not raising any issue of “controversy”, that was just part of the quote: that quote was only to make clear what definitions we are actually talking about, where we differ, and that << [t]he latter I’d call a Leibniz/extensional equality (whether one finds Leibniz equality acceptable or not, which is beside the point here), not the first, and lumping them under one and the same name I’d indeed call self-defeating to say the least. >>

Indeed, talking of “rules”, my only remaining doubt at this point is about the details of the “conversion to normal form” part of primitive equality, and whether that changes anything.

  • The meta-property that you call “identity of indiscernibles”, which I prefer not to write in Coq syntax:

    In any well formed typing context, if there is a type A and 2 terms x
    and y such that if ∀ P: A -> Prop, P x <-> P y is provable then
    so is x = y.

    is not true for the CIC and for Coq, and moreover (afaik) cannot be expressed in Coq since “being provable” would be a statement about the logic itself.


  • The following property (i.e. type), which looks very much the same but means something totally different:

    ∀ A: Type, ∀x y:A, ((∀P: A -> Prop, P x <-> P y) -> (x = y)

    is obviously expressible in Coq and is provable as stated above by @SkySkimmer.

Deciding which one of these two properties designate the real original intended meaning of what Herr Leibniz had in mind is beyond my knowledge (and my interest to be honest). Some very precise reading of his writings would maybe help, or not. I guess we can call each of them an equality inspired by his work without betraying anything or anyone. Maybe we can call the former the meta-leibniz equality or the “semantic” one and the other the syntactic leibniz equality or the “inner” leibniz equality.

Definition provable P := inhabited P, wasn’t that the whole point? Indeed, if you can’t write it in Coq, it is altogether irrelevant… :slight_smile: not to mention, again, Curry-Howard(-Lambek).

More to the point: the second one looks to me like a formalization of the first, i.e. the opposite of “something totally different”. And I remain puzzled that it is provable in Coq without further assumptions… but I still haven’t done that deep dive (it might take me some time, I am not working on this stuff full time…).

the second one looks to me like a formalization of the first, i.e. the opposite of “something totally different”.

As I said it looks like it but it is not. At all. Theorems in Coq are terms but they are not about terms. In other words: terms are the syntax, values are the “semantics”. Inside Coq the expression forall x:A must be understood as “for all values of the type A” and NOT as “for all terms of type A (in any well formed typing environment)”. These two statements live in completely different universes.

This is particularly easy to see for simple inductive types, because values are easy to characterize intuitively. The following lemma states that any value of type nat is either of the form 0 or S of something.

Lemma natShape: forall x:nat, x = 0 \/ exists z:nat, x = S z.
  destruct x.
  - left;reflexivity.
  - right. eauto.

But this is not true for terms of type nat.
Here is the counter-example:
In the CIC type environment [x:A], the term x (a CIC variable) has type nat, it is not 0 or (S ...) and It is not convertible to anything of the form 0 or (S ...).

Semantics is important (operational semantics specifically, as long as programming needs are concerned), or what does it even mean to say that “Coq’s equality is Leibniz”? OTOH, |- A -> B is (provably in Coq [or, at least “do-ably”, again cfr. an operational semantics]) equivalent to A |- B, indeed in both cases we can do destruct/inversion/induction on x, so, with all due respect, to me you are making distinctions that do not exist while conflating things that should be kept distinct.

Let us move forward.

The proof assistant community seems to find legitimate to call “Leibniz Equality” a relation R defined in a proof assistant if you can prove the following statement in the same proof assistant: ∀x y:A, R x y <-> (∀P: A -> Prop, P x <-> P y).

You don’t. OK.

Now is there any interesting question beyond the “don’t use the name in vain” problem?

1 Like

I am raising an issue of substance, not of terminology, for how I’d insist that that terminology is inappropriate: should be called IndiscID_iff_IDIndisc [*], then for one thing it could be easier to see that there being an equivalence is quite extraordinary, given that IndiscID and IDIndisc are supposed to express opposite principles (intensionality vs extensionality), and/or we/I must have messed something up at some level. [*] Indeed no, it should be called IndiscID_and_IDIndisc: but the “puzzle” remains
the same, that both directions hence principles hold.

Overall, I am essentially after a clear line between intensional/extensional and constructive/classical. (I also lump extensional with classical, and this is possibly where we/I, especially I, go wrong: maybe it’s finer than that.) I thought Coq was strictly constructive and intensional and the rest needs axioms, then I have discovered it maybe isn’t, or maybe not in the ways I thought, or to the extent I thought…?

And understanding that is quite crucial to me, in order to use Coq to write my own programs: not to mention, neither you or anybody is compelled to reply, nor maybe I would be here to begin with if there was a clearly documented operational semantics for the language, aka a reference manual proper, so if you don’t find anything to work with here, by all means be my guest and stop posting: I had and still have the same intention, study a bit more before coming back instead of just repeating myself…

I can give some answers.

First: I agree the manual isn’t great and it frustrates me too, but it’s slowly improving. There are better sources for learning; if you want a reference, Conversion rules — Coq 8.18.0 documentation and Typing rules — Coq 8.18.0 documentation define conversion and typing. Convertibility is the closest thing to an operational semantics — in fact, usually op.sem. also specifies the order operation happens (“reduction order”), but that has no effect on the final results.

Different tactics (cbv, lazy, vm_compute) use different reduction orders to normalize terms.

If there are issues of substance, they can be phrased in concrete terms — about Coq statements to prove or disprove, or about Coq metatheorems about Coq typechecking itself (which are harder to prove — even if MetaCoq makes it possible). We use theorem provers because English words can be very ambiguous, including “Leibniz”, intensionality and extensionality; philosophers have a very hard job, we try to keep things simpler.

I don’t know why identity_of_indiscernibles is considered controversial by philosophers, but your statements are easy to prove in Coq, even if other logics might differ:

Lemma indiscernibility_of_identicals: forall {A : Type} (x y : A), x = y -> forall F, F x <-> F y.
Proof. intros * -> *. apply iff_refl. Qed.

Lemma identity_of_indiscernibles : forall {A : Type} (x y : A), (forall F, F x <-> F y) -> x = y.
  intros * H.
  apply (H (fun z => x = z)). reflexivity.

FOL would affect identity_of_indiscernibles’s proof, since we can’t quantify over F inside the logic. But if you can prove F x <-> F y for any predicate F, then you can pick F z := (x = z), obtain x = x <-> x = y, and finish as above.

I looked at part of Max Black’s paper, but his objection seems that (1) either (fun z => x = z) : A -> Prop isn’t a valid property or (b) “if you want to call [this] a property, I suppose I can’t prevent you” but the property becomes obvious (sure, it’s a tautology) and useless (disagree, we use tautologies). I’m happy to call identity_of_indiscernibles a triviality. Excluding fun z => x = z from “properties” / predicates seems neither possible in Coq, nor worthwhile. (The text keeps objecting to things that are perfectly meaningful in formal logic, probably because human languages aren’t well-suited to reasoning; like much continental philosophy, if it has value I can’t appreciate it so I stopped).

I also lump extensional with classical, and this is possibly where we/I, especially I, go wrong: maybe it’s finer than that.

“Extensional” is extremely overloaded (CoqAndAxioms · coq/coq Wiki · GitHub and extensionality in nLab list examples, tho nlab isn’t easy reading) but many meanings are quite distinct from classical. For instance, propositional extensionality holds in classical logic, but also in homotopy type theory (and its versions in Coq). OTOH, in “normal” Coq, postulating excluded middle does not imply propositional extensionality as far as I can tell (also from CoqAndAxioms · coq/coq Wiki · GitHub, The Logic of Coq · coq/coq Wiki · GitHub and sources).

given that IndiscID and IDIndisc are supposed to express opposite principles (intensionality vs extensionality), and/or we/I must have messed something up at some level.

That sounds surprising be right — if IndiscID is a logical truth, it should hold in both intensional and extensional theories.

Coq uses a version of intensional type theory (even if you import classical axioms); extensional type theory exists but remains constructive, because it only makes equality “more extensional” by collapsing (a) convertibility/definitional equality/judgmental equality and (b) propositional equality (what Coq calls “Leibniz equality”). This collapsing is called “equality reflection”. Since that was a source of confusion earlier, I can add a different example. More concretely, extensional type theory (ETT) would allows you to write something “similar” to the following (tho with large caveats, see at the end):

Definition add_1_is_comm_ett (n : nat) : n + 1 = 1 + n := eq_refl.

However, in Coq that’s not legal:

Fail Definition add_is_comm_bad (n : nat) : n + 1 = 1 + n := eq_refl.

that command fails because n + 1 and 1 + n are not convertible, that is, their equality isn’t “simple enough” for the Coq’s kernel typechecker to prove automatically — more formally, that equality isn’t provable via the few conversion rules Conversion rules — Coq 8.18.0 documentation.

You can “fix” that via a rewrite, but that produces a different term — here using eq_ind_r:

Require Import Arith.
Definition add_1_is_comm (n : nat) : n + 1 = 1 + n.
Proof. rewrite Nat.add_comm. reflexivity. Qed.
Print add_is_comm.

add_1_is_comm = 
fun n : nat =>
eq_ind_r (fun n0 : nat => n0 = 1 + n) eq_refl (Nat.add_comm n 1)
	 : forall n : nat, n + 1 = 1 + n


and if you wonder how “the real proof” works, it’s short:

Definition add_1_is_comm_scratch (n : nat) : n + 1 = 1 + n.
  induction n as [|n IHn]. { reflexivity. } 
  simpl. rewrite IHn. reflexivity.
Print add_is_comm_scratch.

add_1_is_comm_scratch = 
fun n : nat =>
nat_ind (fun n0 : nat => n0 + 1 = 1 + n0) eq_refl
  (fun (n0 : nat) (IHn : n0 + 1 = 1 + n0) =>
   eq_ind_r (fun n1 : nat => S n1 = S (S n0)) eq_refl IHn
   S n0 + 1 = 1 + S n0) n
	 : forall n : nat, n + 1 = 1 + n


If you replace Qed with Defined, then for any closed number n, add_1_is_comm_scratch n will reduce to eq_refl — but add_1_is_comm_scratch can’t, since eq_refl : n + 1 = 1 + n is ill-typed when n isn’t known.

If extensional type theory (ETT) can accept Definition add_is_comm (n : nat) : n + 1 = 1 + n := eq_refl. , why does Coq use intensional type theory (ITT)? Well, one trouble with ETT is that eq_refl has type a = b if there’s any proof that a and b are equal, however hard the proof is. That makes typechecking undecidable, so users must fill in proofs anyway, but outside terms; other differences are more technical. In the end, implementing ETT is possible, and both approaches have fans, but ITT is much more robust and (relatively) popular.

Thanks Paolo, that is much nearer to the explanations I was after. It’s obvious that “the Tower of Babel” is good part of the problem, but of course I am rather after what is substantial to these distinctions. I’ll need some time to parse and digest all you have written: I might even try few comments on the philosophical issues, I do have a background in philosophy…

probably because human languages aren’t well-suited to reasoning

On the contrary (said a “philosopher”), formal languages are only suitable to syntactic manipulation, while reasoning proper is all and only prelogical, aka informal. In practice, as anyway quite well known, we can meta-formalize ad libitum: reasoning proper is in the ultimately and necessarily irreducible component of any such progression.

In simple terms, the machine computes, we reason: before and after the fact, i.e. we translate informal problems into formal constructs, and we interpret back the results of derivations/computations into solutions to the initial problems.

But I must warn you that what I have just said, while not only philosophically but down to cybernetically correct, it’s also counter the received/dominant philosophical and logical tradition of at least the last three centuries now…

As for Max Black, for the little I have read, philosophical is the rigour (intellectual honesty as a prerequisite), but his point is very concrete though not purely syntactical: he provides a counter-model (a counter-example) to IdentOfIndisc, which is to say that IdentOfIndisc is false in general.

propositional extensionality holds in classical logic, but also in homotopy type theory

Indeed (IIUC), the Univalence Axiom is an extensional principle. And then I am not sure I want it, as the following is a distinction that I (and I’d say we) do need to preserve (for the specific use case of concrete systems if not for generality):

Operationally, two functions are equivalent if they compute the same result for the same input (i.e. extensional equality as value equality), they are identical if they are identical as terms up to alpha-equivalence (i.e. intensional equality as identity of programs).

I mean, we need to be able to distinguish and reason about programs.

Coq uses a version of intensional type theory

Thanks: I am slowly slowly getting there (e.g. appreciating the distinction reduction vs conversion) but I still need to study quite a bit, about type theory in particular. Will post again if I have anything to ask/discuss or more simply to close my question.

Eventually, I have decided to close this question: there are finer details it might take me years to fully sort out, but I think the answers and comments provided above were in fact pretty enough to narrow this down and then maybe keep investigating.

Among others, I’ll mark @SkySkimmer’s initial reply as an answer: in particular, and contrary to what I had been saying above, I must concede that the fact that both IndiscOfIdent and IdentOfIndisc are provable in plain Coq is rather reasonable justification to call Coq’s built-in equality Leibniz… :slight_smile:

Thanks again everybody for your feedback and explanations, very much appreciated.

Keep up the good work!

1 Like