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.
Proof.
intros * H.
apply (H (fun z => x = z)). reflexivity.
Qed.
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.
Proof.
induction n as [|n IHn]. { reflexivity. }
simpl. rewrite IHn. reflexivity.
Qed.
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.
not to mention, again, Curry-Howard(-Lambek).