如何在Coq中证明列表所有元素均大于等于指定值

数值比较子目标消去 #

对于10 <= 12的子目标，直接使用线性算术战术lia即可自动证明：

• 首先确保导入了算术库，在文件头部添加 Require Import Lia.
• 在子目标位置直接运行 lia 即可完成该目标的消去，不需要额外步骤。

如果不想导入Lia库，也可以用 auto with arith 或者手动构造证明项，lia是效率最高的方案。

结合最小值函数完成全列表元素证明 #

核心思路：构造最小值通用引理 #

你需要先为自己编写的最小值Fixpoint补充一条通用性质引理，建立「列表最小值 <= 所有列表元素」的关系，假设你的最小值函数定义为list_min : list nat -> nat，引理声明如下：

Lemma list_min_le_any_element : forall (l : list nat) (x : nat), In x l -> list_min l <= x.

该引理用列表归纳即可证明：对列表l做归纳，空列表分支因为不存在属于空列表的元素，直接矛盾；非空分支拆分元素属于表头/表尾两种情况，结合你定义list_min时的比较逻辑，搭配lia即可完成证明。

针对当前目标的证明步骤 #

1. 先证明你的固定列表的最小值结论：list_min (20 :: 75 :: 123 :: 12 :: nil) = 12，直接用reflexivity或者compute; reflexivity即可完成。
2. 处理nth索引的合法性：通常nth的证明会带前提i < length l（即索引在列表长度范围内），如果你的场景里default_value也满足>=10，可以单独处理索引越界的分支。
3. 对合法索引i，nth i l default属于列表l，应用上面的list_min_le_any_element引理，可得list_min l <= nth i l default。
4. 代入最小值等于12的结论，可得12 <= nth i l default，结合已经证明的10 <=12，通过不等关系的传递性即可得到10 <= nth i l default。
5. 如果你的目标是实数域的INR 10 <= INR (nth i l default)，应用Coq标准库的INR_le引理，即可将自然数的不等关系提升到实数域，完成最终目标。

简化方案（针对固定短列表） #

如果不需要通用证明，只针对当前长度为4的列表，可以直接拆分索引i的所有情况：

destruct i as [ | [ | [ | [ | i ]]]]; compute; lia.

直接枚举i=0/1/2/3/大于等于4的所有情况，自动计算每个分支的nth结果，用lia自动完成所有不等关系证明，不需要额外定义最小值引理。

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