Coq定理中parameters与indices的区别及声明语法差异问询

首先明确：你提到的“parameters”对应定理冒号前的参数，“indices”这里实际是forall绑定的量化变量（和归纳类型的indices是不同概念，我们聚焦定理声明的两种写法差异）。除了你发现的证明初始上下文差异外，还有以下核心区别：

1. 定理类型的本质结构差异 #

• 冒号前的参数是绑定到定理本身的全局参数，比如par的类型本质是nat -> (n < 1 -> n = 0)（隐式函数类型），调用时必须直接传入n的具体值，例如par 0会生成0 < 1 -> 0 = 0这一具体命题。
• forall绑定的变量是命题内部的量化变量，ind的类型是forall n:nat, n < 1 -> n = 0，调用时可以通过specialize (ind 0)指定变量，也可以直接apply ind让Coq自动推断n的实例。

2. 无法仅用intro/revert消除的场景 #

依赖类型下的作用域差异 #

当涉及依赖类型时，两种写法的调用逻辑完全不同：

(* 冒号前的参数：A是定理的全局依赖参数 *)
Lemma dep_par (A : Type) (x : A) : forall y : A, x = y -> y = x.

(* forall绑定：A是命题内部的量化变量 *)
Lemma dep_ind : forall (A : Type) (x : A) (y : A), x = y -> y = x.

在另一个依赖B:Type的证明中调用时，dep_par必须显式传入B和x:B，比如apply (dep_par B x)；而dep_ind可以直接apply dep_ind，Coq会自动根据当前上下文推断A、x、y的实例，无需手动指定。

类型类结合的场景 #

类型类的实例匹配逻辑也会因写法不同产生差异：

Class EqDec (A : Type) := eq_dec : forall x y : A, {x = y} + {x <> y}.

(* 冒号前的参数：EqDec实例是定理的绑定参数，需显式传入或上下文已有 *)
Lemma dec_par (A : Type) `{EqDec A} (x y : A) : x = y \/ x <> y.

(* forall绑定：EqDec实例是量化变量，Coq会自动搜索上下文匹配 *)
Lemma dec_ind : forall (A : Type) `{EqDec A} (x y : A), x = y \/ x <> y.

调用时，dec_par需要确保上下文存在EqDec A实例或手动传入；而dec_ind可以在任何有对应类型类实例的上下文中直接apply，Coq会自动完成实例搜索。

3. 自动化工具的偏好差异 #

• autorewrite：针对forall形式的定理，重写规则更容易自动匹配量化目标，因为无需先固定变量值；而冒号前参数的定理需要上下文已有对应变量，才能被autorewrite选中应用。
• auto/eauto：forall形式的定理更易被自动搜索到，因为auto会主动为量化变量尝试匹配上下文实例；冒号前参数的定理则需要上下文已存在对应参数，否则auto可能无法自动应用。

举个实际例子：

Definition double n := n + n.
Hint Rewrite double : double_db.

Lemma par_double (n : nat) : double n = n + n.
Proof. autorewrite with double_db. reflexivity. Qed.

Lemma ind_double : forall n : nat, double n = n + n.
Proof. autorewrite with double_db. reflexivity. Qed.

在后续证明中：

Lemma test : forall m, double m = m + m.
Proof.
  intro m.
  apply par_double.  (* 可行，但需要上下文已有m *)
  apply ind_double. (* 可行，无需提前绑定m *)
  auto with double_db. (* auto会自动应用ind_double，无需手动指定变量 *)
Qed.

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