Coq中无基例归纳类型的归纳证明有效性疑问

定义与定理代码 #

Inductive my_s : Type :=
  | loop (s : my_s).

Theorem p_of_s : forall (x : my_s) (p : my_s -> Prop),
  p x.
Proof.
  intros s.
  induction s as [s' IHs'].
  - intro p.
    apply IHs'.
Qed.

应用IHs'前的证明状态 #

s' : my_s
IHs' : forall p : my_s -> Prop, p s'
p : my_s -> Prop
----------------------------
p (loop s')

关键解析 #

你觉得IHs'和目标不匹配，是忽略了归纳假设IHs'的全称量化特性：它对所有my_s -> Prop类型的谓词都成立，不是只绑定当前上下文里的那个p。

当执行apply IHs'时，Coq会自动推导合适的谓词来实例化IHs'中的全称量词。这里它会把IHs'里的通用谓词替换成fun x => p (loop x)——也就是把原谓词p包装了一层，让它接受loop x作为参数。

实例化后的IHs'就变成了p (loop s')，和目标完全一致，自然就能完成证明。

本质上，归纳假设的全称性允许我们灵活调整谓词的形式，适配目标里的递归结构，而不是只能直接匹配s'本身。

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