如何在Coq中对CompCert定义的int类型实现类nat式归纳证明？

问题背景 #

1. CompCert中的int类型定义如下：

Record int: Type := mkint { intval: Z; intrange: -1 < intval < modulus }.

2. 需要证明定理foo，由于P1、P2存在递归关系且实际场景中i为正整数，尝试采用归纳策略，当前代码如下：

From compcert Require Import Integers.

Parameter P1 : int -> Prop.
Parameter P2 : int -> Prop.

Theorem foo: 
    forall i: int,
    (P1 i) -> (P2 i).
Proof.
    destruct i. induction intval.
    admit.
    induction p.
Abort.

3. 当前对p归纳会生成BinNums.Zpos (BinNums.xI p)和BinNums.Zpos (BinNums.xO p)两种难以处理的情况，希望能像nat类型那样，通过(P1 i)→(P2 i)推导(P1 (i+1))→(P2 (i+1))，寻求解决思路。

解决思路 #

1. 转成自然数做标准归纳 #

既然只处理正整数的int，可以先把int的数值部分转成nat，复用nat的S归纳结构：

• 先提取int的intval，利用intrange证明它是正整数（intval > 0）；
• 用Z.to_nat将正整数转为nat，对这个nat做归纳，就能得到n和S n的对应关系，也就是原问题里的i和i+1。

示例代码片段：

Proof.
  intros i Hp1.
  destruct i as [v Hrange].
  assert (v_pos : v > 0) by omega.  (* 用omega自动推导正整数条件 *)
  pose (n := Z.to_nat v).
  revert i Hp1 Hrange v_pos.
  induction n as [|n IHn]; intros i Hp1 Hrange v_pos.
  (* 基础情况：n=0对应v=0，结合v_pos可推导矛盾或按P1/P2逻辑处理 *)
  (* 归纳步骤：n=S n'对应v = Z.of_nat n' + 1，可关联i和i+1的递归关系 *)
  ...
Qed.

2. 自定义正int的步进归纳原理 #

如果不想转nat，可以为正int定制一个类似nat的归纳原理，直接支持i到i+1的步进推导：

Lemma int_pos_induction :
  forall (P : int -> Prop),
  P (mkint 1 (by omega)) ->  (* 基础情况：最小正int *)
  (forall i : int, 0 < intval i < modulus - 1 -> P i -> P (mkint (intval i + 1) (by omega))) ->  (* 步进归纳 *)
  forall i : int, 0 < intval i < modulus -> P i.
Proof.
  intros P Hbase Hstep i Hpos.
  destruct i as [v Hrange].
  assert (v_pos : 0 < v < modulus) by omega.
  induction (Z.to_nat (v - 1)) as [|n IHn].
  - (* v=1，直接用基础情况Hbase *)
    apply Hbase.
  - (* v = (Z.of_nat n + 1) + 1，调用步进归纳Hstep *)
    let i_prev := mkint (v - 1) (by omega) in
    apply Hstep with (i := i_prev).
    * omega.
    * apply IHn.
      omega.
Qed.

之后证明foo时直接调用这个归纳原理：

Proof.
  intros i Hp1.
  apply int_pos_induction with (P := fun i => P1 i -> P2 i).
  - (* 基础情况：证明P1 1 -> P2 1 *)
    ...
  - (* 归纳步骤：假设P1 i -> P2 i，推导P1 (i+1) -> P2 (i+1) *)
    intros i Hrange HIH Hp1_next.
    ...
Qed.

3. 利用Z库的正整数归纳策略 #

Coq的Z库提供了针对正整数的专用归纳策略，比如Z.pos_ind或良基归纳Z.lt_wf_ind，可以直接对intval使用：

Proof.
  destruct i as [v Hrange].
  assert (v_pos : v > 0) by omega.
  induction v using Z.pos_ind.
  - (* v=1的基础情况 *)
    ...
  - (* 归纳步骤：基于所有小于v的正整数的归纳假设，推导当前v的情况，可结合v-1关联i+1逻辑 *)
    ...
Qed.

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