Coq中eq_rect的定义、位置、来源及与等式关联的技术问询

Let's break down your questions clearly, as someone who's spent plenty of time digging into Coq's core logic:

What is eq_rect, and where is it defined? #

• What it is: eq_rect is the foundational induction principle for Coq's equality type eq. At its heart, it encodes the substitution principle (Leibniz's law): if two terms are equal, any property or structure that applies to one automatically applies to the other. Unlike hand-written lemmas, it's not defined manually—Coq generates it automatically when the inductive equality type eq is declared.

• Where it lives: The base equality type eq lives in the Coq.Init.Logic module, which is imported by default in almost all Coq sessions (so you don't need to explicitly Require it to access eq_rect). To see its type directly, just run this in your Coq environment:

  Check eq_rect.
  

Why isn't it in the official manual, and what's its exact statement? #

It's totally normal to not find eq_rect listed explicitly in the official manual—here's why: it's an automatically generated induction principle for an inductive type, not a hand-crafted primitive or lemma. Coq spits out a set of these principles for every inductive type (whether user-defined or part of the standard library), and the manual focuses on explaining the general mechanism of inductive types rather than documenting every auto-generated principle individually.

Exact statement of eq_rect #

First, let's recap the core definition of the equality type eq (from Coq.Init.Logic):

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

From this inductive definition, Coq automatically generates eq_rect with the following type signature:

eq_rect : forall (A : Type) (x : A) (P : A -> Type) (f : P x) (y : A), x = y -> P y

Let's unpack what each part means:

• A: Any type you're working with (e.g., nat, bool, or a custom data type).
• x: A term belonging to type A.
• P: A dependent predicate on A—it maps every term of A to some type (this could be a proposition like n > 5, or a data type like vector n).
• f: A witness that P x holds (either a proof if P x is a proposition, or an element if P x is a data structure).
• x = y: A proof that x and y are equal.
• The conclusion P y: We can "transport" the witness f from P x to P y using the equality x = y.

As a quick side note: You might also run into eq_ind and eq_rec in Coq. These are specialized variants of eq_rect:

• eq_ind: Tailored for when P maps to Prop (substitution for propositional properties).
• eq_rec: Tailored for when P maps to Set (substitution for data structures).
• eq_rect: The most general version, working for Type (which includes both Prop and Set).

内容的提问来源于stack exchange，提问作者Siddharth Bhat