Coq中定理应用的精确规则及相关示例疑问

算力阿峰

2026-5-8

Coq定理应用的精确规则与你的示例疑问解答

Coq中的定理（Lemma/Example/Theorem本质都是依赖类型的函数），应用时必须严格遵循以下规则：

定理的类型签名是一个依赖类型的函数，你传入的每一个参数必须精确匹配签名中对应位置的类型要求——包括依赖于前面参数的类型。
命题（Prop）和命题的证明项是两回事：命题是类型（比如0=2的类型是Prop），而证明项是该类型的实例（比如intros H得到的H就是0=2这个类型的一个项，代表“0=2成立的证据”）。
对于带forall/->/<->的定理，应用时需要依次传入所有隐式/显式参数，或者让Coq通过上下文自动推断（用_表示让Coq自动补全）。

先看你的xxx的类型：

Example xxx: (0 = 2) -> (0 = 3). (* xxx的类型是：(0=2) → (0=3) *)

这个定理是一个函数：它接受一个类型为0=2的项（也就是0=2的证明证据），返回一个0=3的证明。

apply (xxx H)能成功，是因为H是intros H得到的，H的类型就是0=2——它是0=2这个命题的证明项，完全匹配xxx的参数要求。
apply (xxx (0=2))失败，是因为(0=2)本身是一个命题（类型是Prop），但xxx需要的是一个类型为0=2的证明项，不是命题本身。Coq的报错其实是在说：你传入的东西类型是Prop，但我需要的是0=2这个具体类型的项（也就是它的证明）。

当你把xxx定义为：

Example xxx: (0 = 2) <-> (0 = 3). (* xxx的类型是：(0=2 ↔ 0=3) *)

在Coq中，<->是双向蕴含，本质上等价于(0=2 → 0=3) ∧ (0=3 → 0=2)——也就是一个合取命题。所以xxx本身是一个合取命题的证明项，而不是一个直接的蕴含函数。

你直接写apply (xxx H)失败，是因为xxx的类型不是(0=2)→(0=3)，而是(0=2→0=3) ∧ (0=3→0=2)。要使用它的正向蕴含，你需要先提取合取的左半部分，比如：

apply (proj1 xxx) in H.
(* 或者手动传参：apply (proj1 xxx H). *)

proj1是从合取命题P ∧ Q中提取P的证明的函数，proj1 xxx就会得到类型为(0=2)→(0=3)的函数，再传入H就符合要求了。

我们一步步拆解这个调用：

proj1的类型：forall P Q : Prop, P ∧ Q → P。它是一个函数：接受两个命题P、Q，再接受一个P∧Q的证明项，返回P的证明项。
In_map_iff的类型：forall (A B : Type) (f : A→B) (l : list A) (y : B), In y (map f l) ↔ exists x, f x = y ∧ In x l。这个<->同样等价于双向蕴含的合取，所以In_map_iff的返回值是一个合取命题的证明项。

你写的In_map_iff _ _ _ _ _里的_是让Coq自动推断参数：
根据上下文的H : In n (map (fun m => m*0) ns)，Coq会自动推断出：

所以In_map_iff _ _ _ _ _的最终类型是：

In n (map (fun m => m*0) ns) ↔ exists x, (x*0 = n) ∧ In x ns

也就是一个合取命题P ∧ Q的证明，其中P是In n (map ... ns) → exists x, ...，Q是反向的蕴含。

当你把In_map_iff _ _ _ _ _传给proj1 _ _时，proj1会自动推断P和Q就是上面的双向蕴含的两个方向，proj1 _ _ (In_map_iff ...)的类型就变成了：

In n (map (fun m => m*0) ns) → exists x, (x*0 = n) ∧ In x ns

这是一个函数，最后传入H（In n (map ... ns)的证明项），就得到了exists x, (x*0 = n) ∧ In x ns的证明项——也就是后面destruct要处理的存在量词证据。

简单来说，这个调用就是：用proj1从In_map_iff给出的双向蕴含中提取正向的蕴含函数，再用H作为参数调用这个函数，得到存在量词的证明。

内容的提问来源于stack exchange，提问作者wt.cc