如何在Coq中定义无间隙的自然数列表？

要定义无间隙的自然数列表，核心是保证列表包含某个连续自然数区间内的所有数（顺序无关）。比如[2,1,3]覆盖了1到3的所有自然数，因此有效；而[5,1,3]缺少2和4，无法形成连续区间，因此无效。

以下是具体的实现步骤：

1. 导入依赖库 #

首先导入Coq的列表处理库，方便使用基础的列表操作：

Require Import List Nat.
Import ListNotations.

2. 定义辅助函数 #

我们需要几个基础辅助函数来获取列表的最小值、最大值，以及判断元素是否存在于列表中：

（1）非空列表的最小值 #

Fixpoint list_min (l : list nat) : nat :=
  match l with
  | [] => 0  (* 空列表返回0，实际后续谓词会排除空列表 *)
  | [n] => n
  | n :: m :: tl => min n (list_min (m :: tl))
  end.

（2）非空列表的最大值 #

Fixpoint list_max (l : list nat) : nat :=
  match l with
  | [] => 0
  | [n] => n
  | n :: m :: tl => max n (list_max (m :: tl))
  end.

（3）元素存在性判断 #

直接用Coq标准库的In谓词即可，不过可以明确写出：

(* 标准库已有In谓词，这里仅作说明 *)
Check In : nat -> list nat -> Prop.

3. 定义无间隙列表的谓词 #

现在可以定义核心谓词NoGaps，它满足两个条件：

• 列表非空；
• 所有介于列表最小值和最大值之间的自然数，都存在于列表中。

Definition NoGaps (l : list nat) : Prop :=
  l <> [] /\
  forall n : nat,
    (list_min l <= n <= list_max l) -> In n l.

4. 验证示例 #

我们可以用Coq的Example语句验证题目中的例子：

（1）有效列表示例 #

Example valid_list : NoGaps [2;1;3].
Proof.
  unfold NoGaps.
  split.
  - discriminate.  (* 证明列表非空 *)
  - intros n H.
    destruct n as [|n] eqn:En.
    + inversion H.  (* n=0小于min=1，不满足前提 *)
    + destruct n as [|n] eqn:En'.
      * simpl in H. rewrite En' in H. reflexivity.  (* n=1，在列表中 *)
      * destruct n as [|n] eqn:En''.
        -- simpl in H. rewrite En'' in H. reflexivity.  (* n=2，在列表中 *)
        -- simpl in H. rewrite En'' in H. reflexivity.  (* n=3，在列表中 *)
        -- inversion H.  (* n>=4大于max=3，不满足前提 *)
Qed.

（2）无效列表示例 #

Example invalid_list : ~NoGaps [5;1;3].
Proof.
  unfold NoGaps. intro H.
  destruct H as [H_nonempty H_forall].
  apply H_forall with (n := 2).
  split.
  - compute. reflexivity.  (* list_min [5;1;3] = 1 <= 2 *)
  - compute. reflexivity.  (* 2 <= list_max [5;1;3] =5 *)
  -- compute. discriminate.  (* 2不在列表中，矛盾 *)
Qed.

补充说明 #

• 如果需要支持空列表，可以修改NoGaps谓词，将l <> []改为True，但通常“无间隙”针对非空列表更有意义；
• 上述定义不要求列表有序，只关注元素是否覆盖连续区间，符合题目中的例子要求；
• 可以进一步优化辅助函数，比如使用更高效的方式计算min/max，或者添加对重复元素的处理（重复元素不影响无间隙判断，比如[2,2,1,3]依然有效）。

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