如何用Coq策略风格证明互归纳类型定理？以~TypeA为例

问题背景 #

给定以下互归纳命题：

Inductive TypeA : Prop :=
  | ConstructorA : TypeB -> TypeA
with TypeB : Prop :=
  | ConstructorB : TypeA -> TypeB. 

已有函数式风格的~TypeA证明：

Fixpoint TypeA_is_empty' (a : TypeA) : False :=
  match a with 
  | ConstructorA b' => TypeB_is_empty' b'
  end
with TypeB_is_empty' (b : TypeB) : False :=
  match b with 
  | ConstructorB a' => TypeA_is_empty' a'
  end.

尝试用策略风格的互定理证明时，遇到循环依赖或语法报错问题。

报错原因解释 #

使用Lemma ... with ...编写互定理时出现Cannot find common (mutual) inductive premises or coinductive conclusions in the statements.错误，原因是：
Coq的互定理（mutual theorems）机制要求参与互证的定理满足以下条件之一：

• 所有定理的结论是互共归纳定义的类型
• 所有定理的前提包含同一组互归纳定义的类型

用户之前的目标是~TypeA（等价于TypeA -> False），其结论是False（非互归纳/共归纳类型），且Coq无法自动识别TypeA与TypeB作为前提的互归纳关联，因此无法触发互定理的处理逻辑。

正确的策略风格互定理证明方法 #

将定理改写为直接量化互归纳类型的形式（即forall a:TypeA, False和forall b:TypeB, False），这样前提是互归纳类型，Coq可以识别为互定理，再用策略完成证明：

Lemma TypeA_is_empty : forall a : TypeA, False
with TypeB_is_empty : forall b : TypeB, False.
Proof.
- intros a. inversion a as [b]. apply TypeB_is_empty.
- intros b. inversion b as [a]. apply TypeA_is_empty.
Qed.

-- 如需~TypeA，可直接定义
Definition TypeA_not : ~TypeA := TypeA_is_empty.

证明说明 #

1. 用with关键字绑定两个互证的定理，Coq会自动处理它们之间的递归依赖
2. 第一个子证明：对任意a:TypeA，通过inversion拆解构造子得到b:TypeB，直接调用TypeB_is_empty完成证明
3. 第二个子证明：对任意b:TypeB，同理拆解得到a:TypeA，调用TypeA_is_empty完成证明

另一种方法是先生成互归纳原理，再用策略证明：

-- 生成互归纳原理
Scheme TypeA_ind_mut := Induction for TypeA Sort Prop
with TypeB_ind_mut := Induction for TypeB Sort Prop.

Theorem TypeA_is_empty : ~TypeA.
Proof.
  unfold not. intros a.
  apply TypeA_ind_mut with (Q := fun b => False).
  - intros b. apply TypeB_is_empty.
  - intros a. apply TypeA_is_empty.
Qed.

Theorem TypeB_is_empty : ~TypeB.
Proof.
  unfold not. intros b.
  apply TypeB_ind_mut with (P := fun a => False).
  - intros b. apply TypeB_is_empty.
  - intros a. apply TypeA_is_empty.
Qed.

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