带构造函数命名参数的Coq证明：mapCCoption定理证明受阻问题

云上老周

2026-4-30

解决Coq中mapCCoption定理的证明问题

我完全懂你卡在这儿的原因！BB和CC这俩归纳类型的核心差异，就是参数绑定的位置：BB把类型构造器m作为归纳类型本身的参数，而CC把m放在了构造函数的参数列表里。这就导致解构CC option a时，Coq没法自动保留m就是option这个关键信息——得我们手动帮它补上这个约束才行。

问题本质

当你对x : CC option a执行destruct x as [m1 a1 o]时，Coq会把m1当成一个任意的Type -> Type变量，但实际上从x的类型我们能确定m1必须等于option，a1必须等于a。缺少这两个等式约束，后续的证明自然就推进不下去了。

完整证明方案

我们可以用inversion策略（或者带eqn参数的destruct）来提取这些关键等式，把丢失的类型信息找回来。这里提供两种简洁的实现方式：

方法1：用`inversion`直接解构

Theorem mapCCoption (a : Type) (b : Type) (f : a -> b) (x : CC option a) : CC option b.
Proof.
  inversion x as [m1 a1 o Hm Ha].
  (* Hm: m1 = option，Ha: a1 = a —— 这两个等式帮我们恢复了丢失的类型信息 *)
  apply (cc option b).
  destruct o as [a0|].
  - exact (Some (f a0)).
  - exact None.
Qed.

方法2：带`eqn`的`destruct` + 等式分析

如果你更习惯用destruct，可以通过eqn参数保存解构后的构造等式，再用inversion分析这个等式：

Theorem mapCCoption (a : Type) (b : Type) (f : a -> b) (x : CC option a) : CC option b.
Proof.
  destruct x as [m1 a1 o] eqn:Hx.
  (* Hx记录了x的构造方式：x = cc m1 a1 o *)
  inversion Hx as [].
  (* inversion自动替换了目标和上下文里的m1、a1，现在它们被固定为option和a *)
  apply (cc option b).
  destruct o as [a0|].
  - apply (Some (f a0)).
  - apply None.
Qed.