如何在Coq中证明递归定义函数的性质：alignof_correct引理求解

你的问题核心在于type和fieldlist是互递归定义的，单独对type做归纳无法覆盖alignof_fields的递归调用场景，需要先证明一个针对fieldlist的辅助引理，再通过互递归归纳完成主引理的证明。

步骤1：定义互递归引理 #

由于两个函数互相依赖，我们需要同时声明主引理和辅助引理，再一起证明：

Lemma alignof_correct : forall (ty : type), (alignof ty > 0)%Z.
Lemma alignof_fields_correct : forall (fld : fieldlist), (alignof_fields fld > 0)%Z.

步骤2：完成互递归证明 #

使用split同时处理两个引理的归纳证明：

Proof.
  split.
  - (* 证明主引理 alignof_correct *)
    intros ty. induction ty.
    simpl. (* alignof展开为alignof_fields fld *)
    apply alignof_fields_correct. (* 直接调用辅助引理 *)
  - (* 证明辅助引理 alignof_fields_correct *)
    intros fld. induction fld.
    + (* Fnil 情况 *)
      simpl. (* alignof_fields Fnil = 1 *)
      apply Z.gt_pos. (* 调用ZArith库引理：正整数1大于0 *)
    + (* Fcons _ ty fld' 情况 *)
      simpl. (* 展开为Z.max (alignof ty) (alignof_fields fld') *)
      apply Z.max_gt_0. (* ZArith库引理：两个正数的最大值也是正数 *)
      split; assumption. (* 分别调用主引理结论和fieldlist的归纳假设 *)
Qed.

关键细节说明 #

• 互递归结构的性质证明必须同时处理所有递归分支，Coq的split命令支持同时完成多个引理的证明，解决循环依赖问题。
• 用到的ZArith库核心引理：
  • Z.gt_pos：所有正整数都大于0
  • Z.max_gt_0：若a>0且b>0，则Z.max a b > 0

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