如何在Coq中使用Znumtheory库证明一个数是素数

嘿，我完全懂你在Coq里用Znumtheory证明3是素数时卡壳的点——处理H : 1 <= n < 3这个假设确实容易绕弯路，尤其是第一次上手prime_intro策略的时候。别担心，其实有个更简洁的方法能搞定这个区间拆分，不用反复手动destruct或者lt_eq_cases。

首先先回忆下prime_intro的作用：Znumtheory里的素数定义是大于1的数p，所有能整除p且满足1<=n<p的n只能是1或者p本身。所以prime_intro会把目标拆成两个子目标：一是证明3>1，二是证明所有满足1<=n<3且能整除3的n只能是1或3。

针对你头疼的区间假设H : 1 <= n < 3，推荐直接用interval_cases策略——它专门用来处理整数区间的假设，能一步把1<=n<3拆成n=1和n=2两种精确情况，比手动拆分高效太多。

下面是完整的证明示例，我会一步步标注：

Require Import Znumtheory ZArith Lia.

Lemma three_is_prime : prime 3.
Proof.
  apply prime_intro.
  (* 第一个子目标：证明3>1，用lia直接就能自动搞定 *)
  - lia.
  (* 第二个子目标：引入n、n整除3的假设，以及1<=n<3的约束 *)
  - intros n H_le H_div.
    (* 关键一步：用interval_cases直接拆分区间假设 *)
    interval_cases n.
    + 第一种情况n=1：直接左分支，证明n=1即可
      left; reflexivity.
    + 第二种情况n=2：此时2整除3是矛盾的，我们可以直接否定这个整除假设
      contradict H_div.
      lia. (* lia能自动识别2不整除3的矛盾 *)
Qed.

至于你之前尝试的lt_eq_cases+destruct为啥会得到无用的1 <n：其实lt_eq_cases会把1<=n拆成1<n或n=1，但1<n结合n<3只能推出n=2，但这个过程需要手动推导，远不如interval_cases一步到位来得直接。

下次遇到整数区间类的假设，都可以优先试试interval_cases，能省不少手动组合条件的功夫～

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