跳到正文
Hacker News· birdculture·· 9 天前AI 评分22

Isabelle/HOL、Lean、HOL4 与 Agda 四大定理证明器对比评测

Comparison of Isabelle/HOL, Lean, HOL4, and Agda: A Tale of Four Theorem Provers

AI 导读

一位作者在 Isabelle/HOL、Lean、HOL4 和 Agda 中分别形式化验证了素数无穷性的欧几里得证明，并据此比较四款定理证明器的使用体验。Lean 与 Agda 属依赖类型系统，Isabelle/HOL 与 HOL4 为 LCF 风格；Isabelle/HOL 的 sledgehammer 自动化最强，Agda 几乎无自动化，Lean 的 simp 与 grind 表现不及前者。

正文 · AI 翻译

2026-10-10

A Wren.

目录

以上（哇，好长的标题）

在其中我比较了 Lean、Isabelle/HOL、Agda 和 HOL4，仅对“公平性”略有顾及。

我们到底在比较什么？

以上四个都是定理证明应用；也就是说，它们的目的是用计算机形式化数学。 广义上讲，Lean 和 Agda 都是基于依赖类型的系统，利用 Curry-Howard 对应通过复杂的类型系统来证明定理，而 Isabelle/HOL 和 HOL4 是 LCF 风格的系统，带有一个包含基本规则（例如 forall x, x = x）的小型“证明内核”，所有证明都必须通过它来构造。 两种基础各有优缺点，其中一些将会讨论。

基于什么？

我在所有四个系统中都形式化了一个素数无穷性的证明；也就是说，命题“对于任意数 n，存在一个大于 n 的素数”。所形式化的确切证明是欧几里得的“通常”构造，如果你想看，可以在 Wikipedia 上找到；见此处。

所有证明在结构上看起来相似（大部分如此，我们稍后会谈到），因此是用户体验造成了差异。为透明起见，在这个实验之前，我最熟悉 Isabelle/HOL 和 Agda，并在一定程度上作为本次评审的一部分学习了 HOL4 和 Lean。

比较时间！

以下是一堆观点和一些有些随意的分类。请不要期待无偏见的评审。如果你只想要证明比较，跳到证明比较；如果你只想要更多观点，读下面的内容，然后跳到任意排名。观点先来。

我并不声称以下任何证明是完美的！它们实际上可能相当平庸。

总体相似点/差异

我们可以通过几个类别来对这些定理证明器进行分组。我们有上面提到的：

  • LCF 风格：Isabelle/HOL、HOL4
  • 依赖风格：Lean、Agda

但还有：

交互性

  • 高交互性：Isabelle/HOL、Lean
  • 低交互性：HOL4、Agda

推理：Isabelle/HOL 和 Lean 都在你输入时提供“实时更新”，并且它们的结构化证明可以通过“向下箭头”逐步查看中间步骤。相比之下，已完成的 HOL4 和 Agda 证明作为完全组合好的项存在，如果你想检查其内部，必须手动拆解。当然，HOL4 和 Agda 都可以随时向你显示当前状态和相关信息。

自动化

  • 高自动化：Isabelle/HOL、HOL4
  • 中等自动化：Lean
  • 低自动化：Agda

Isabelle/HOL 有 sledgehammer，它会调用许多外部证明生成方法（SAT/SMT 求解器、各种一阶逻辑求解器等）。对于任何看起来可做但烦人的目标，sledgehammer 都有很大机会能解决它——这很好，因为它能省去你的工作，但它生成的证明也晦涩难懂，这或许不太理想。HOL4 也有一个等价物叫 HolyHammer，但我直到写这篇文章时才发现它的存在。算了。Isabelle/HOL 和 HOL4 都对许多自动简化和证明方法有很好的支持，例如在尝试处理复杂假设时非常方便。如果没有简化介入把一切拆解成小块，可能不太清楚如何继续。

Lean 有不错的自动化，但达不到 Isabelle/HOL 或 HOL4 的水平。它的 simp 效率远没有那么高，而虽然 grind 是一种非常巧妙的方法，有时能与 sledgehammer 媲美，但很多时候它相当无用，原因我也不明白。sledgehammer 和 grind 都是全有或全无；如果它们不能解决目标，就不会取得任何进展。这与 simp（三者中都有）或更专门的工具如 auto（Isabelle/HOL）或 gvs（HOL4）形成对比，后者可以取得一些进展，然后（理想情况下）把上下文留在更好的状态。Lean 没有同样好的部分自动化，这有点遗憾，因为根据我的经验，那才是真正更重要的。值得注意的是，Lean 和 Isabelle/HOL 都有一个 try（在 Isabelle/HOL 中，有/无 sledgehammer 时分别为 try/try0；在 Lean 中为 try?/exact?/rw?），它会用各种自动化方法和直接求解尝试来“试一试”你的目标。据我所知，HOL4 没有等价物，这很不幸，因为它相当方便。

Agda 基本上没有自动化。你能得到的唯一简化是基于函数输入可以计算出来的部分。坦白说，这有点糟糕。很难把事情做完，因为有太多手动调整必须考虑。我个人不喜欢。

基础

Isabelle/HOL 和 HOL4 的基础都极其经典，这意味着它们接受排中律（∀ P. ¬P ∨ P），并且两者都公理化了希尔伯特 epsilon，这也导致了选择公理。这似乎对自动求解器有非常积极的影响，因为它们经常依赖双重否定消除（¬¬P --> P）等定律，而这等价于排中律。Lean 理论上是构造性的（因此默认没有排中律），但一些“好的”证明自动化需要排中律，而且使用 Lean 时采用经典方式似乎是常态，所以我就这么做了。例如 grind 就直接假设你在使用它。这确实有一个缺点，例如 Lean 在处理存在量词等方面不那么好。

Agda 默认是构造性的，而且在 Agda 世界里保持证明的构造性似乎是常态，所以我也这么做了。这样做的一大好处是，在证明素数有无穷多个之后，我实际上可以生成它们！我可以给我的证明一个数字，它就会输出一个比该数字大的素数。缺点是这样做极其慢：

  • 0: 2（瞬间）
  • 1: 3（瞬间）
  • 2: 7（瞬间）
  • 3: 5（瞬间）
  • 4: 11（四分之一秒）
  • 5: 7（四分之一秒）
  • 6: 71（3秒）
  • 7: 61（10秒）
  • 8: 19（40秒）

如果你看了上面的证明结构，这可能是合理的；我们考虑 (n + 1)! + 1，所以在那个证明内部，它是在检查大约 ~360,000 附近的数的素性；这会有点慢。应该指出，这种构造并不是为了快，但它也是最自然的。是否值得放弃 LEM 和良好的证明自动化？你决定。

依赖类型作为基础 vs LCF

我更倾向于 LCF，因为它似乎更适合自动化，而且我不明白携带证明项有什么意义（经典逻辑太有用了！）。如果你强烈反对，请发邮件到 contact AT blueberrywren.dev，如果我喜欢你的论点，我会把它贴在这里。

交互模式

Lean 和 Isabelle/HOL 都是通过交互方式使用的。Lean 有其他编辑器的模式，但强烈推荐使用 VSCode，而 Isabelle/HOL 有自己的编辑器（jEdit），它也几乎强制使用。这没问题；我理解他们为什么这样做，因为交互式开发很难做到通用。两者都做到了。

HOL4 通过 Emacs 模式或 Vim 模式进行交互，并且有键绑定允许将文本复制到正在运行的 HOL4 REPL 中或从中复制出来。这听起来很奇怪，因为它确实如此，但它工作得出奇地好。我已经是 Emacs 用户，所以对我来说没什么变化。

Agda 也通过 Emacs 模式进行交互，但一切都在你的文件中发生；你可以使用键绑定来刷新状态、添加证明目标等。它也能正常工作。

如上所述，Lean/Isabelle/HOL 方法的优势在于可以看到进行中的证明，而 Agda 则不能。

文档

Isabelle/HOL 和 HOL4 都有极好的定理搜索机制；前者有一个编辑器面板 + find_theorems，后者有 DB.find/DB.match。这些允许按名称和模式搜索定理，例如我可以搜索形式为 _ < SUC _ 的引理。这太方便了！很多时候你知道你想要的东西的形状，但可能不知道引理本身。

Lean 有 leansearch 和 loogle，它们很有趣，但它们：

  1. 不是内置的。
  2. 不够好。

这有点糟糕。exact? 和 rw? 存在，作为“这里有一些你可能能做的事情”，但它们远没有那么灵活。

Agda，也许如预期的那样，没有等价物。一个人必须成为禅浏览 Agda 标准库正确部分的大师。

证明比较

注意：这并不是真正为其中任何一个做的教程，尽管我会在开始时做一些解释。它主要是为了让读者比较它们，看看在不同语言中大致等价的陈述证明是什么样子。

让我们进入证明！我们将逐段进行，探索证明的各个部分并边走边解释。在此之前，一些有点有趣的统计数据：

  • Isabelle/HOL：117 行代码，19 个证明。
  • Lean：155 行代码，12 个证明。
  • HOL4：190 行代码，16 个证明。
  • Agda：264 行代码，45 个证明（29 个，不计 where 块）

这些远非完全可比，但仍然很有趣。

我们从定义整除性开始。在 Agda 中，我们作弊并使用标准库版本，这样我们可以得到关于计算除数的证明，我不想重做这些。

Isabelle/HOL：

definition divides :: "nat ⇒ nat ⇒ bool" where
  "divides n k = (∃j. j * n = k)"

Lean：

@[grind]
def divides (n k : Nat) : Prop :=
  ∃q, k = n * q

HOL4：

Definition divides_def:
  divides n k = ∃q. q * n = k
End

Agda（看起来，在标准库中）：

record _∣_ (m n : ℕ) : Set where
  constructor divides
  field quotient : ℕ
        equality : n ≡ quotient * m

所以，基本上是一样的。然后有几个关于整除性的引理被证明了（divides k 0、divides k k等）。我们要展示的一个是divides n k ==> divides n j ==> divides n (k - j)，因为它在一些定理证明器中有点意思。在以下所有内容中，乘/减引理本质上陈述了a * (b - c) = a * b - a * c。

Isabelle/HOL：

lemma divides_diff: "divides x k ⟹ divides x n ⟹ divides x (k - n)"
  using divides_def by (metis diff_mult_distrib)

证明搜索过程metis完成了大部分工作。

Lean：

theorem divides_sub (n j k : Nat) (h1 : divides n k) (h2 : divides n j)
  : divides n (k - j) := by
  obtain ⟨q1, h1⟩ := h1
  obtain ⟨q2, h2⟩ := h2
  unfold divides
  exists (q1 - q2)
  grind [Nat.mul_sub]

我们进行一些解包，然后将q1 - q2识别为另一项（使得n * (q1 - q2) = k - j）。然后用适当的引理进行grind就能让我们达到目的。

HOL4：

Theorem divides_sub:
  divides n k ⇒ divides n j ⇒ divides n (k - j)
Proof
  rpt strip_tac
  >> metis_tac[RIGHT_SUB_DISTRIB, divides_def]
QED

像Isabelle/HOL一样，当提供适当的引理时，metis_tac就能搞定它。

Agda：

divides-sub : ∀ {i j k} → i ∣ j → i ∣ k → i ∣ (j ∸ k)
divides-sub {i} (divides-refl q₁) (divides-refl q₂) = divides (q₁ ∸ q₂) (sym (*-distribʳ-∸ i q₁ q₂))

非常相似。divides-refl是divides _ refl的缩写，就像在Lean中一样，我们必须手动指出q₁ ∸ q₂。

对我来说有趣的是，Lean的证明在某种程度上如此痛苦。尽管Lean有相当不错的自动化，但我不得不在那个上投入比任何其他都多的努力！找到适当的引理稍微更痛苦，而且公平地说，这还是在我在纠结语法的时候。

接下来我们需要定义一列数字的乘积，看起来如下：

Isabelle/HOL：

fun prod_list :: "nat list ⇒ nat" where
"prod_list [] = 1" | 
"prod_list (x # xs) = x * prod_list xs"

Lean：

@[simp, grind]
def prod_list (xs : List Nat) : Nat :=
  match xs with
  | [] => 1
  | x :: xs => x * prod_list xs

simp和grind标记旨在帮助自动证明方法，它们确实做到了！

HOL4：

Definition prod_list_def:
  (prod_list [] = 1) ∧
  (prod_list (x :: xs) = x * prod_list xs)
End

Agda：

prod-list : List Nat → Nat
prod-list [] = 1
prod-list (x ∷ xs) = x * prod-list xs

在HOL4中定义东西有点意思，因为你只是将主体定义为一个证明！那个定义产生一个定理prod_list_def，它字面上就是

val it = ⊢ prod_list [] = 1 ∧ ∀x xs. prod_list (x::xs) = x * prod_list xs: thm

!

在Agda证明中，我们还做了大量工作来设置将成为素性判定程序的东西。这是因为稍后我们希望问“这是素数吗？”，而没有LEM来说“它必须是素数或不是素数”，我们需要写一个算法来为我们决定这个。

回到正轨，我们需要展示一些关于prod list函数的引理。其中一个有趣的是如下，我们证明所述列表中的一个数字将整除该列表的乘积。

Isabelle/HOL：

lemma divides_prod_list: "x ∈ set xs ⟹ divides x (prod_list xs)"
  apply (induct xs)
   apply simp
  apply auto
   apply (case_tac xs; simp add: divides_def)
  apply (case_tac xs; simp)
  apply (rule mult_divide_l)
  by assumption

非常隐式；很难看出发生了什么，但基本结构在那里。对列表进行归纳，做一些分类讨论，应用一个关于divides _ (_ * _)的引理。

Lean：

theorem divides_prod_list : ∀ xs x, x ∈ xs -> divides x (prod_list xs) := by
  intros xs x mem
  induction xs with
  | nil => grind
  | cons y ys ih =>
    by_cases h : (x = y)
    · rw [h]
      simp
      exists (prod_list ys)
    · cases mem with
      | head => grind
      | tail =>
        rename_i a
        have ⟨h, hq⟩ := ih a
        simp at *
        rw [hq]
        exists (y * h)
        grind

相当大。我们必须相当手动地解构成员关系，这有点麻烦。不过这是一个相当直接的证明。

HOL4：

Theorem divides_prod_list:
  x ∈ set xs ⇒ divides x (prod_list xs)
Proof
  Induct_on ‘xs’
  >- fs[]
  >- (fs[]
      >> rpt strip_tac
      >- (fs[prod_list_def, divides_def]
          >> qexists_tac ‘prod_list xs’
          >> simp[])
      >- (fs[divides_def, prod_list_def]
          >> qexists_tac ‘h * q’
          >> rev_drule EQ_SYM
          >> strip_tac
          >> fs[]))
QED

也不疯狂，尽管没有注释（我没写:P）很难看出确切结构。这是一个好时机指出HOL4证明字面上就是SML项！没有更多了！组合子>>和>-（分别用于将后者应用于前者的所有子目标，以及应用于前者的一个子目标）只是组合其他函数的中缀函数！全都是SML！你通过REPL与HOL4交互，所以你动态地构建东西，但之后你必须把你的函数拼凑起来。一旦你知道这一点，就更清楚发生了什么；我们进行归纳，处理第一种情况，然后对MEM x (h ∷ xs)进行简化给我们两个目标（分别是x = h和x ≠ h, MEM x xs）

Agda：

prod-list-divides : ∀ xs x → x ∈ xs → x ∣ prod-list xs
prod-list-divides [] x ()
prod-list-divides (y ∷ xs) x (here refl) = divides (prod-list xs) (*-comm y (prod-list xs))
prod-list-divides (y ∷ xs) x (there p) with prod-list-divides xs x p
... | divides q eq rewrite eq = divides (y * q) (sym (*-assoc y q x))

非常显式，但也相当简洁。对列表成员关系进行匹配相当直观，因为Emacs中的Agda模式包括一个命令C-c C-c，可以自动对基本上所有东西进行情况分割。

虽然在Isabelle/HOL和HOL4中更加隐式（一个常见主题），但这四个证明都采取询问我们关心的值是在列表头部还是后面某处的形式，这决定了我们在整除性中填入什么。

然后，素性！

Isabelle/HOL：

definition prime :: "nat ⇒ bool" where
  "prime p = ((p > 1) ∧ (∀x. divides x p ⟶ x = p ∨ x = 1))"

Lean：

@[simp, grind]
def prime (n : Nat) : Prop :=
  (n > 1) ∧ (∀k, divides k n -> k = 1 ∨ k = n)

HOL4：

Definition prime_def:
  prime n = ((1 < n) ∧ (∀k. divides k n ⇒ k = 1 ∨ k = n))
End

Agda：

record Prime (n : Nat) : Set where
  constructor isprime
  field
    gt1 : n > 1
    div : ∀ k → k ∣ n → k ≡ 1 ⊎ k ≡ n

在Agda中，我们还将合数的含义定义为一个“正面”定义，而不仅仅是“非素数”；这使得使用它容易得多。

下一个“有趣的”证明是证明每一个大于 1 的非素数都有一个素因子。在 Agda 中，这是合数定义的一部分，所以我们不必费心把它包含进来。从现在开始，我们会稍微加快速度，所以我不会解释每一个代码片段。你们自己对比一下吧。

Isabelle/HOL：

lemma prime_factor: "¬(prime k) ⟹ k > 1 ⟹ ∃p. prime p ∧ divides p k"
  apply (induct k rule: measure_induct[of "id"]; simp)
  apply (rotate_tac 1)
  apply (subst (asm) prime_def)
  apply clarsimp
  apply (case_tac "prime xa")
   apply blast
  apply (erule_tac x=xa in allE)
  (* found with sledgehammer *)
  by (metis divides_gt divides_trans less_Suc0 not_less_iff_gr_or_eq zero_not_divides)

Lean：

theorem prime_factor : ∀k, ¬(prime k) -> 1 < k -> ∃p, prime p ∧ divides p k := by
  intros k nprime kgt1
  induction k using Nat.strongRecOn with
  | ind k' ih =>
    simp at nprime
    obtain ⟨x,⟨xd,dvds⟩,xn1,xnk⟩ := nprime kgt1
    clear nprime
    by_cases h : prime x
    · exists x
      grind
    · have lt : x < k' := by
        apply Nat.lt_of_le_of_ne
        · apply divides_less <;> grind
        · assumption
      have gt : 1 < x := by
        cases x <;> grind
      obtain ⟨p,⟨prm,dvds⟩⟩ := ih x lt h gt
      exists p
      refine ⟨prm, ?_⟩
      apply divides_trans
      · assumption
      · grind

HOL4：

Theorem prime_factor:
  ∀k. ¬(prime k) ⇒ 1 < k ⇒ ∃p. prime p ∧ divides p k
Proof
  completeInduct_on ‘k’
  >> rpt strip_tac
  >> qpat_x_assum ‘¬_’
                  (fn h => assume_tac
                          (REWRITE_RULE [prime_def] h))
  >> gvs[]
  >> Cases_on ‘prime k'’
  >- (qexists ‘k'’ >> simp[])
  >- (first_x_assum $ qspecl_then [‘k'’] mp_tac
      >> strip_tac
      >> ‘0 < k'’ by metis_tac[divides_gt1_gt0]
      >> ‘1 < k'’ by decide_tac
      >> ‘k' <= k’ by gvs[divides_less]
      >> ‘k' < k’ by decide_tac
      >> first_x_assum drule
      >> strip_tac
      >> gvs[]
      >> qexists ‘p’
      >> metis_tac[divides_trans])
QED

HOL4 中 0 < k' ~> 1 < k' 和 k' <= k ~> k' < k 的步骤让我非常恼火，但我没能想出如何把它们精简掉。同样，这一行：

    obtain ⟨x,⟨xd,dvds⟩,xn1,xnk⟩ := nprime kgt1

Lean 证明中的这一行让我很痛苦。

我们现在快到了！还剩两步：证明在给定的数字集合（列表）之外总有一个素数，并用它来证明最终命题。首先，前者：

Isabelle/HOL：

lemma another_prime: "(∀x∈set xs. x > 1) ⟹ ∃p. prime p ∧ p ∉ set xs"
  apply (case_tac "prime (Suc (prod_list xs))")
  using prod_list_lt apply fastforce
  apply (frule prime_factor)
   apply clarsimp
  apply (case_tac "length xs = 0"; clarsimp)
   apply (rule prod_list_gt_zero; clarsimp)
  using prime_gt_one apply fastforce
  using divides_prod_list divides_diff prime_gt_one one_divides
  by (metis One_nat_def Suc_diff_Suc cancel_comm_monoid_add_class.diff_cancel lessI nat_less_le)

Lean：

theorem another_prime (xs : List Nat) (xsgt : ∀x, x ∈ xs -> 1 < x)
  : ∃p, prime p ∧ p ∉ xs := by
  by_cases h : prime (Nat.succ (prod_list xs))
  · exists (Nat.succ (prod_list xs))
    refine ⟨h, ?a⟩
    by_contra
    have lt : Nat.succ (prod_list xs) ≤ prod_list xs := by
      apply prod_list_lt <;> grind
    grind
  · have ⟨pf, isprm, dvds⟩ : ∃p, prime p ∧ divides p (Nat.succ (prod_list xs)) := by
      apply prime_factor
      · exact h
      · grind [prod_list_nz]
    by_cases g : pf ∈ xs
    · have pfdvds : divides pf (prod_list xs) := by
        apply divides_prod_list <;> grind
      have divone : divides pf ((Nat.succ (prod_list xs)) - prod_list xs) := by
        apply divides_sub <;> grind
      have also : divides pf 1 := by grind
      grind [divides_not_one]
    · grind

HOL4：

Theorem another_prime:
  ∀(xs : num list). (∀x. x ∈ set xs ⇒ 1 < x)
                    ⇒ ∃p. prime p ∧ p ∉ set xs
Proof
  rpt strip_tac
  >> Cases_on ‘prime (SUC (prod_list xs))’
  >- (qexists ‘SUC (prod_list xs)’
      >> metis_tac[LESS_REFL, OR_LESS, prod_list_lt, gt1_gt0_weaken])
  >- (drule prime_factor
      >> impl_tac
      >- metis_tac[ONE, LESS_MONO, prod_list_nz,gt1_gt0_weaken]
      >- (strip_tac
          >> Cases_on ‘MEM p xs’
          >- (‘divides p (prod_list xs)’
                by metis_tac[divides_prod_list]
              >> ‘divides p ((SUC (prod_list xs)) - prod_list xs)’
                by metis_tac [divides_sub]
              >> gvs[]
              >> metis_tac[prime_one, prime_zero, divides_not_one])
          >- (qexists ‘p’ >> metis_tac[])))
QED

Agda：

prime-not-in : ∀ xs → (∀ x → x ∈ xs → x > 0) → Σ _ λ k → k ∉ xs × Prime k
prime-not-in xs gt with 2 ≤? prod-list xs
... | no ¬a = 2 , lemma , two-prime
  where
    lemma : 2 ∈ xs → ⊥
    lemma pf with prod-list-lt xs gt 2 pf
    ... | also = ¬a also
... | yes a with prime-or-composite (suc (prod-list xs)) (s≤s (≤-trans (s≤s z≤n) a))
... | inj₁ x = suc (prod-list xs) , lemma , x
  where
    lemma : (suc (prod-list xs)) ∈ xs → ⊥
    lemma pf with prod-list-lt xs gt (suc (prod-list xs)) pf
    ... | also = 1+n≰n also
... | inj₂ (composite p Pp p<n p∣) with p ∈? xs
... | no ¬b = p , ¬b , Pp
... | yes b with prod-list-divides xs p b
... | divs with divides-sub p∣ divs
... | sothen = ⊥-elim (lemma {p} {prod-list xs} sothen λ{ refl → one-prime Pp })
  where
    suc-sub : ∀ i → suc i ∸ i ≡ 1
    suc-sub zero = refl
    suc-sub (suc i) = suc-sub i

    lemma : ∀ {i j} → i ∣ (suc j ∸ j) → i ≢ 1 → ⊥
    lemma {_} {j} div neq rewrite suc-sub j = divides-not-one div neq

Agda 的证明略有不同，以适应后面缺少范围（ranges）的情况。

Isabelle/HOL 的证明在长度上显然胜出，但它也让人完全不清楚发生了什么。其他人的证明则逐渐变得更加冗长，尤其是 HOL4 的证明在这里嵌套得有点难看。metis_tac[]（一个一阶求解器）承担了大量繁重的工作，grind 也是如此。如果你想知道为什么 Isabelle/HOL 和 HOL4 都有一个名为 metis/metis_tac 的东西，那是因为它是从 HOL4 移植到 Isabelle/HOL 的。

我们到达了最终命题！Agda 需要更多的调整，因为它不像另外两个那样内置了范围（ranges），但我们使用上面的引理来构造列表 [2..n]，然后证明在该列表之外有一个素数（因此它必然大于 n）。

Isabelle/HOL：

lemma infinite_primes: "∃p. prime p ∧ p > n"
  apply (insert another_prime[where xs="[2 ..< Suc n]"])
  apply (case_tac "n ≤ 1"; clarsimp)
   apply (rule_tac x=2 in exI)
   apply simp
  apply (rule_tac x=p in exI)
  apply simp
  using prime_gt_one by force

Lean：

theorem infinite_primes : ∀ n, ∃p, prime p ∧ p > n := by
  intros n
  by_cases h : ¬(1 < n)
  · exists 2
    grind [prime_two]
  · simp at h
    obtain ⟨p, prm, notin⟩ := another_prime (List.range' 2 n) (by grind)
    refine ⟨p, prm, ?notin⟩
    grind

HOL4：

Theorem infinite_primes:
    ∀n. ∃p. prime p ∧ p > n
Proof
  strip_tac
  >> Cases_on ‘n < 1’
  >- (qexists ‘2’ >> simp[prime_two])
  >- (qspec_then ‘listRangeINC 2 n’ assume_tac another_prime
      >> ‘∀x. MEM x [2 .. n] ⇒ 1 < x’
        by (rpt strip_tac >> gvs[MEM_listRangeINC])
      >> first_x_assum rev_drule
      >> rpt strip_tac
      >> qexists ‘p’
      >> gvs[MEM_listRangeINC, prime_gt_one]
      >> ‘p ≠ 0’ by metis_tac[prime_zero]
      >> ‘p ≠ 1’ by metis_tac[prime_one]
      >> decide_tac)
QED

我没能把它变得更小，这让我很恼火，但算了。

Agda：

infinite-primes : ∀ i → Σ _ λ p → p > i × Prime p
infinite-primes zero = 2 , s≤s z≤n , two-prime
infinite-primes (suc i) with prime-not-in (list-up-to (2+ i)) (list-up-to-nz (2+ i))
... | p , notin , Pp = p , DNE (2+ i ≤? p) lemma , Pp
  where
    notzero : p ≢ 0
    notzero = prime-not-zero p Pp

    implies : ∀ {a b} → (suc a ≤ b → ⊥) → (a ≡ b) ⊎ (a > b)
    implies {a} {b} x with compare a b
    ... | less .a k = ⊥-elim (x (s≤s (m≤m+n a k)))
    ... | equal .a = inj₁ refl
    ... | greater .b k = inj₂ (s≤s (m≤m+n b k))

    lemma : ((2+ i ≤ p) → ⊥) → ⊥
    lemma x with implies x
    ... | inj₁ refl = notin (there (here refl))
    ... | inj₂ (s≤s a) = notin (list-up-to-contains (2+ i) p (≤-trans a (≤-trans (n≤1+n i) (n≤1+n (suc i)))) (prime-not-zero p Pp))

我们做到了！欧几里得会感到骄傲的。（大概吧）

现在是时候发表更多意见了！

任意排名

我将根据五个标准进行排名：

  • 证明发现的容易程度（弄清楚我想做什么有多容易）
  • 证明操作的容易程度（做我想做的事有多容易）
  • 乐趣（我有多开心）
  • 烦人程度（我有多经常说“呃！”）
  • 困惑程度（我有多经常说“为什么你解决不了这个？？”）

证明发现的容易程度（越高越好）

  1. Isabelle/HOL
  2. HOL4
  3. Lean
  4. Agda

这里真的没什么好评论的。sledgehammer 是一个巨大的福音，Isabelle/HOL 和 HOL4 的定理发现工具都很棒。Lean 紧随其后，try? 经常能给出很好的相关引理作为求解结果，而 Agda 显然排在最后。在网上翻阅 .agda 文件来查找引理很烦人。

证明操作的容易程度（越高越好）

  1. Agda
  2. Lean
  3. HOL4
  4. Isabelle/HOL

爱它也好，恨它也好，Agda 完全使用原始证明项意味着事情本质上完全如你所告诉它们的那样。从来不会有那么一刻你会说“该死，为什么简化器只展开这个而不展开那个！”。Lean 在这方面相当不错，因为它对选择操作的内容相当保守，而且所有东西都有明确的命名。HOL4 的学习曲线相当合理，因为人们要学会使用像 qpat_assum 这样可以根据模式（例如 ¬_）进行定位的东西，但一旦你弄明白了，它就不错。Isabelle/HOL 在这里真的不怎么样；通常很难让它完全按照你的意愿去做。

乐趣（越高越好）

  1. HOL4
  2. Lean
  3. Isabelle/HOL
  4. Agda

我很享受学习 HOL4 和 Lean 的过程，但 HOL4 略胜一筹，因为它的交互模式非常独特，而且依然非常强大。Lean 很有趣，尽管有时令人恼火，而 Isabelle/HOL 不是特别有意思，但这部分是因为我对它已经很熟悉了。Agda 有时挺糟糕的；写一个完整的素性判定过程并摆弄类型上的琐事，过一阵子就变得相当烦人。

烦人程度（越低越好）

  1. Agda
  2. HOL4 / Lean（并列第二）
  3. Isabelle/HOL

Agda 因上述同样的原因“胜出”。不得不进行非常手动化的证明搜索并不断摆弄，这并不太令人愉快。HOL4 和 Lean 各有各的烦人之处，我认为把其中一个排在另一个之上是不公平的；在 HOL4 中，假设操作 / sim 的学习曲线相当陡峭，而 Lean 的自动化工具足够挑剔，有时相当糟糕。Isabelle/HOL 我只是用惯了，所以那里有一些偏差。

困惑程度（越低越好）

  1. HOL4
  2. Lean
  3. Isabelle/HOL
  4. Agda

原因同上；有很多次 HOL4 让我直呼“啊？？？”，因为某个定理-策略没有按我预期的方式工作，或者以不可预测的方式变换目标。Lean 也有类似情况，它会随机决定“呃其实我不打算用 grind 帮你解决这个非常简单的目标，请你自己来”，这让我感到困惑。说真的，有时 grind 比 sledgehammer 更聪明，有时它比 simp 更笨。奇怪。Isabelle/HOL 也有一些同样的问题，但总体还好，而 Agda 完全可预测。

总体同类最佳

HOL4！我学习它时非常愉快，它是一个非常有趣的系统。我并不是不喜欢 Lean，但其中发生了足够多的古怪事情，让我对它略有戒心，我想。Isabelle/HOL 仍然是我最擅长的（我写它多少能拿到报酬，所以这有帮助），而 Agda 就是 Agda。

你应该尝试什么？嗯，全都试试，但至少尝试一些新东西。如果你以前只用过依赖类型定理证明器，试试 Isabelle/HOL 或 HOL4，反之亦然。如果你只用过像 Lean 这样完全交互式工作的定理证明器，试试 HOL4 或 Agda！新的体验是生活的乐趣。

所有代码

享受吧。

展开一切。

Isabelle/HOL：

theory primes
  imports Main
begin

definition divides :: "nat ⇒ nat ⇒ bool" where
  "divides n k = (∃j. j * n = k)"

lemma zero_not_divides: "k ≠ 0 ⟹ ¬(divides 0 k)"
  by (simp add: divides_def)

lemma one_divides: "divides k 1 ⟹ k = 1"
  by (simp add: divides_def)

lemma divide_mult_l: "divides x k ⟹ divides x (n * k)"
  using divides_def by auto

lemma divides_diff: "divides x k ⟹ divides x n ⟹ divides x (k - n)"
  using divides_def by (metis diff_mult_distrib)

lemma divides_gt: "k ≠ 0 ⟹ n > k ⟹ ¬(divides n k)"
  by (clarsimp simp add: divides_def)

lemma divides_less: "k ≠ 0 ⟹ divides n k ⟹ n ≤ k"
  by (clarsimp simp add: divides_def)

lemma divides_trans: "divides n k ⟹ divides k j ⟹ divides n j"
  using divides_def by force

fun prod_list :: "nat list ⇒ nat" where
"prod_list [] = 1" | 
"prod_list (x # xs) = x * prod_list xs"

lemma prod_list_gt_zero: "(∀x∈set xs. x ≠ 0) ⟹ length xs > 0 ⟹ prod_list xs > 0"
  apply (induct xs)
   apply simp
  by (case_tac xs; clarsimp)

lemma prod_list_lt: "(∀x∈set xs. x > 0) ⟹ ∀x∈set xs. x ≤ prod_list xs"
  apply (induct xs)
   apply simp
  apply auto
  using prod_list_gt_zero apply fastforce
  apply (erule_tac x=x in ballE)
  using mult_eq_if apply auto[1]
  by blast

lemma divides_prod_list: "x ∈ set xs ⟹ divides x (prod_list xs)"
  apply (induct xs)
   apply simp
  apply auto
   apply (case_tac xs; simp add: divides_def)
  apply (case_tac xs; simp)
  apply (rule divide_mult_l)
  by assumption

definition prime :: "nat ⇒ bool" where
  "prime p = ((p > 1) ∧ (∀x. divides x p ⟶ x = p ∨ x = 1))"

lemma prime_zero[simp]: "¬(prime 0)"
  by (clarsimp simp add: prime_def)

lemma prime_one[simp]: "¬(prime 1)"
  by (clarsimp simp add: prime_def)

lemma prime_two[simp]: "prime 2"
  apply (clarsimp simp add: prime_def)
  apply (case_tac x; clarsimp simp add: divides_def)
  apply (case_tac nat; clarsimp simp add: divides_def)
  by (case_tac j; simp)

lemma prime_gt_one: "prime p ⟹ p > 1"
  using prime_def by simp

lemma notprime_split: "¬(prime k) ⟹ k > 1 ⟹ ∃n j. n < k ∧ j < k ∧ k = n * j"
  apply (clarsimp simp add: prime_def divides_def)
  apply (rule_tac x=x in exI)
  apply (rule conjI)
   apply (metis less_Suc0 linorder_neqE_nat mult_is_0 n_less_m_mult_n)
  apply (rule_tac x=j in exI)
  apply auto
  by (metis bot_nat_0.not_eq_extremum mult_zero_left not_less_zero)

lemma prime_not_divides_one: "prime p ⟹ ¬(divides p 1)"
  by (clarsimp simp add: prime_def divides_def)

lemma prime_factor: "¬(prime k) ⟹ k > 1 ⟹ ∃p. prime p ∧ divides p k"
  apply (induct k rule: measure_induct[of "id"]; simp)
  apply (rotate_tac 1)
  apply (subst (asm) prime_def)
  apply clarsimp
  apply (case_tac "prime xa")
   apply blast
  apply (erule_tac x=xa in allE)
  by (metis divides_gt divides_trans less_Suc0 not_less_iff_gr_or_eq zero_not_divides)


lemma another_prime: "(∀x∈set xs. x > 1) ⟹ ∃p. prime p ∧ p ∉ set xs"
  apply (case_tac "prime (Suc (prod_list xs))")
  using prod_list_lt apply fastforce
  apply (frule prime_factor)
   apply clarsimp
  apply (case_tac "length xs = 0"; clarsimp)
   apply (rule prod_list_gt_zero; clarsimp)
  using prime_gt_one apply fastforce
  using divides_prod_list divides_diff prime_gt_one one_divides
  by (metis One_nat_def Suc_diff_Suc cancel_comm_monoid_add_class.diff_cancel lessI nat_less_le)

lemma infinite_primes: "∃p. prime p ∧ p > n"
  apply (insert another_prime[where xs="[2 ..< Suc n]"])
  apply (case_tac "n ≤ 1"; clarsimp)
   apply (rule_tac x=2 in exI)
   apply simp
  apply (rule_tac x=p in exI)
  apply simp
  using prime_gt_one by force

end

Lean：

import Primes.Basic
import Mathlib.Tactic.ByContra

set_option linter.style.setOption false
set_option linter.flexible false
set_option linter.style.whitespace false

@[grind]
def divides (n k : Nat) : Prop :=
  ∃q, k = n * q

theorem divides_one (n : Nat) : divides n 1 -> n = 1 := by
  intro ⟨q, hq⟩
  cases n <;> cases q <;> grind

theorem divides_not_one (n : Nat) (d : divides n 1) (neq : n ≠ 1) : False := by
  grind [divides_one]

theorem divides_sub (n j k : Nat) (h1 : divides n k) (h2 : divides n j)
  : divides n (k - j) := by
  obtain ⟨q1, h1⟩ := h1
  obtain ⟨q2, h2⟩ := h2
  unfold divides
  exists (q1 - q2)
  grind [Nat.mul_sub]

theorem divides_less (n k : Nat) : k ≠ 0 -> divides n k -> n ≤ k := by
  intro knz div
  simp at *
  obtain ⟨q,hq⟩ := div
  cases q <;> grind

theorem divides_trans (n k j) : divides n k -> divides k j -> divides n j := by
  intro ⟨a,b⟩ ⟨c,d⟩
  simp [divides] at *
  exists (a * c)
  grind

@[simp, grind]
def prod_list (xs : List Nat) : Nat :=
  match xs with
  | [] => 1
  | x :: xs => x * prod_list xs

theorem divides_prod_list : ∀ xs x, x ∈ xs -> divides x (prod_list xs) := by
  intros xs x mem
  induction xs with
  | nil => grind
  | cons y ys ih =>
    by_cases h : (x = y)
    · rw [h]
      simp
      exists (prod_list ys)
    · cases mem with
      | head => grind
      | tail =>
        rename_i a
        have ⟨h, hq⟩ := ih a
        simp at *
        rw [hq]
        exists (y * h)
        grind

theorem prod_list_nz : ∀ xs, (∀ x ∈ xs, x > 0) -> prod_list xs > 0 := by
  intros xs f
  induction xs with
  | nil => grind
  | cons x xs ih =>
    obtain b : prod_list xs > 0 := ih (by grind)
    simp [*]

theorem prod_list_lt : ∀ xs, (∀ x ∈ xs, x > 0) -> ∀ y ∈ xs, y <= prod_list xs := by
  intro xs f y yin
  induction xs with
  | nil => grind
  | cons yp ys ih =>
    cases yin with
    | head =>
      obtain a : prod_list ys > 0 := by grind [prod_list_nz]
      exact Nat.le_mul_of_pos_right y a
    | tail _ a =>
      obtain a : y <= prod_list ys := ih (by grind) a
      obtain b : yp > 0 := f yp (by grind)
      apply Nat.le_trans
      · exact a
      · exact Nat.le_mul_of_pos_left (prod_list ys) b

@[simp, grind]
def prime (n : Nat) : Prop :=
  (n > 1) ∧ (∀k, divides k n -> k = 1 ∨ k = n)

theorem prime_two : prime 2 := by
  simp
  intros k x
  simp [divides] at x
  have ⟨q,hq⟩ := x
  (cases q <;> cases k <;> grind)


theorem prime_factor : ∀k, ¬(prime k) -> 1 < k -> ∃p, prime p ∧ divides p k := by
  intros k nprime kgt1
  induction k using Nat.strongRecOn with
  | ind k' ih =>
    simp at nprime
    obtain ⟨x,⟨xd,dvds⟩,xn1,xnk⟩ := nprime kgt1
    clear nprime
    by_cases h : prime x
    · exists x
      grind
    · have lt : x < k' := by
        apply Nat.lt_of_le_of_ne
        · apply divides_less <;> grind
        · assumption
      have gt : 1 < x := by
        cases x <;> grind
      obtain ⟨p,⟨prm,dvds⟩⟩ := ih x lt h gt
      exists p
      refine ⟨prm, ?_⟩
      apply divides_trans
      · assumption
      · grind


theorem another_prime (xs : List Nat) (xsgt : ∀x, x ∈ xs -> 1 < x)
  : ∃p, prime p ∧ p ∉ xs := by
  by_cases h : prime (Nat.succ (prod_list xs))
  · exists (Nat.succ (prod_list xs))
    refine ⟨h, ?a⟩
    by_contra
    have lt : Nat.succ (prod_list xs) ≤ prod_list xs := by
      apply prod_list_lt <;> grind
    grind
  · have ⟨pf, isprm, dvds⟩ : ∃p, prime p ∧ divides p (Nat.succ (prod_list xs)) := by
      apply prime_factor
      · exact h
      · grind [prod_list_nz]
    by_cases g : pf ∈ xs
    · have pfdvds : divides pf (prod_list xs) := by
        apply divides_prod_list <;> grind
      have divone : divides pf ((Nat.succ (prod_list xs)) - prod_list xs) := by
        apply divides_sub <;> grind
      have also : divides pf 1 := by grind
      grind [divides_not_one]
    · grind

theorem infinite_primes : ∀ n, ∃p, prime p ∧ p > n := by
  intros n
  by_cases h : ¬(1 < n)
  · exists 2
    grind [prime_two]
  · simp at h
    obtain ⟨p, prm, notin⟩ := another_prime (List.range' 2 n) (by grind)
    refine ⟨p, prm, ?notin⟩
    grind

HOL4：

open arithmeticTheory listTheory prim_recTheory listRangeTheory;
     
Definition divides_def:
  divides n k = ∃q. q * n = k
End

Theorem divides_not_one:
  ∀n. divides n 1 ⇒ n ≠ 1 ⇒ F
Proof
  simp[divides_def]
QED

Theorem divides_less:
  k ≠ 0 ⇒ divides n k ⇒ n ≤ k
Proof
  rpt strip_tac
  >> gvs[divides_def]
QED

Theorem divides_trans:
  divides a b ⇒ divides b c ⇒ divides a c
Proof
  rpt strip_tac
  >> gvs[divides_def]
  >> qexists ‘q * q'’
  >> gvs[MULT_ASSOC_COMM]
QED

Theorem divides_sub:
  divides n k ⇒ divides n j ⇒ divides n (k - j)
Proof
  rpt strip_tac
  >> metis_tac[RIGHT_SUB_DISTRIB, divides_def]
QED
            
Definition prod_list_def:
  (prod_list [] = 1) ∧
  (prod_list (x :: xs) = x * prod_list xs)
End

Theorem divides_prod_list:
  x ∈ set xs ⇒ divides x (prod_list xs)
Proof
  Induct_on ‘xs’
  >- fs[]
  >- (fs[]
      >> rpt strip_tac
      >- (fs[prod_list_def, divides_def]
          >> qexists_tac ‘prod_list xs’
          >> simp[])
      >- (fs[divides_def, prod_list_def]
          >> qexists_tac ‘h * q’
          >> rev_drule EQ_SYM
          >> strip_tac
          >> fs[]))
QED      

Theorem prod_list_nz:
  ∀xs. (∀x. x ∈ set xs ⇒ 0 < x) ⇒ 0 < prod_list xs
Proof
  rpt strip_tac
  >> Induct_on ‘xs’
  >> fs[prod_list_def]
QED
     
Theorem prod_list_lt:
  ∀xs. (∀x. x ∈ set xs ⇒ 0 < x) ⇒ ∀y. y ∈ set xs ⇒ y ≤ prod_list xs
Proof
  rpt strip_tac
  >> Induct_on ‘xs’
  >> gvs[]
  >> rpt strip_tac
  >> gvs[prod_list_def]
  >> metis_tac[prod_list_nz, LE_MULT_CANCEL_LBARE, LE_TRANS]
QED

Definition prime_def:
  prime n = ((1 < n) ∧ (∀k. divides k n ⇒ k = 1 ∨ k = n))
End

Theorem prime_zero:
  ¬(prime 0)
Proof
  fs[prime_def]
QED        


Theorem prime_one:
  ¬(prime 1)
Proof
  fs[prime_def]
QED

Theorem prime_gt_one[simp]:
  prime n ⇒ 1 < n
Proof
  fs[prime_def]
QED
              
Theorem prime_two:
  prime 2
Proof        
  fs[prime_def]
  >> rpt strip_tac
  >> fs[divides_def]
  >> (Cases_on ‘k’ >> Cases_on ‘q’ >> fs[MULT_SUC])
QED

Theorem divides_gt1_gt0:
  ∀n k. divides n k ⇒ 1 < k ⇒ 0 < n
Proof
  rpt strip_tac
  >> gvs[divides_def]
  >> (Cases_on ‘q’ >> gvs[MULT_SUC])
  >> (Cases_on ‘n’ >> gvs[])
QED

Theorem prime_factor:
  ∀k. ¬(prime k) ⇒ 1 < k ⇒ ∃p. prime p ∧ divides p k
Proof
  completeInduct_on ‘k’
  >> rpt strip_tac
  >> qpat_x_assum ‘¬_’
                  (fn h => assume_tac
                          (REWRITE_RULE [prime_def] h))
  >> gvs[]
  >> Cases_on ‘prime k'’
  >- (qexists ‘k'’ >> simp[])
  >- (first_x_assum $ qspecl_then [‘k'’] mp_tac
      >> strip_tac
      >> ‘0 < k'’ by metis_tac[divides_gt1_gt0]
      >> ‘1 < k'’ by decide_tac
      >> ‘k' <= k’ by gvs[divides_less]
      >> ‘k' < k’ by decide_tac
      >> first_x_assum drule
      >> strip_tac
      >> gvs[]
      >> qexists ‘p’
      >> metis_tac[divides_trans])
QED

Theorem gt1_gt0_weaken:
  ∀x. 1 < x ⇒ 0 < x
Proof
  strip_tac >> decide_tac
QED

Theorem another_prime:
  ∀(xs : num list). (∀x. x ∈ set xs ⇒ 1 < x)
                    ⇒ ∃p. prime p ∧ p ∉ set xs
Proof
  rpt strip_tac
  >> Cases_on ‘prime (SUC (prod_list xs))’
  >- (qexists ‘SUC (prod_list xs)’
      >> metis_tac[LESS_REFL, OR_LESS,
                   prod_list_lt, gt1_gt0_weaken])
  >- (drule prime_factor   
      >> impl_tac
      >- metis_tac[ONE, LESS_MONO, prod_list_nz,gt1_gt0_weaken]
      >- (strip_tac
          >> Cases_on ‘MEM p xs’
          >- (‘divides p (prod_list xs)’
                by metis_tac[divides_prod_list]
              >> ‘divides p ((SUC (prod_list xs)) - prod_list xs)’
                by metis_tac [divides_sub]
              >> gvs[]
              >> metis_tac[prime_one, prime_zero, divides_not_one])
          >- (qexists ‘p’ >> metis_tac[])))
QED

                    
Theorem infinite_primes:
    ∀n. ∃p. prime p ∧ p > n
Proof
  strip_tac
  >> Cases_on ‘n < 1’
  >- (qexists ‘2’ >> simp[prime_two])
  >- (qspec_then ‘listRangeINC 2 n’ assume_tac another_prime
      >> ‘∀x. MEM x [2 .. n] ⇒ 1 < x’
        by (rpt strip_tac >> gvs[MEM_listRangeINC])

      >> first_x_assum rev_drule
      >> rpt strip_tac
      >> qexists ‘p’
      >> gvs[MEM_listRangeINC, prime_gt_one]
      >> ‘p ≠ 0’ by metis_tac[prime_zero]
      >> ‘p ≠ 1’ by metis_tac[prime_one]
      >> decide_tac)
QED

Agda：

open import Data.Nat renaming (ℕ to Nat)
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Empty
open import Relation.Nullary.Negation
open import Data.List
open import Data.Sum
open import Relation.Nullary.Decidable
open import Relation.Binary
open import Relation.Nullary.Reflects
open import Data.Nat.Divisibility
open import Data.Bool using (Bool; true; false)
open import Data.Fin using (zero; suc; Fin; toℕ; fromℕ; fromℕ<)
open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-fromℕ<)
open import Induction.WellFounded
open import Data.Nat.Induction using (<-wellFounded; <-rec)

import Data.List.Membership.DecPropositional as DecPropMembership
open DecPropMembership Data.Nat._≟_
open import Data.List.Relation.Unary.Any using (here; there)

-- The prime decision procedure was with assistance from https://gist.github.com/copumpkin/1286093

div-goes-into : ∀ i k → k ≢ 0 → i ∣ k → i ≤ k
div-goes-into i k neq (divides zero eq) = ⊥-elim (neq eq)
div-goes-into zero k neq (divides (suc q) eq) = z≤n
div-goes-into (suc i) k neq (divides-refl (suc q)) = s≤s (m≤m+n i (q * suc i))

divides-zero : ∀ i → 0 ∣ i → i ≡ 0
divides-zero zero (divides q eq) = refl
divides-zero (suc i) (divides q eq) rewrite *-comm q 0 = eq

divides-trans : ∀ {i j k} → i ∣ j → j ∣ k → i ∣ k
divides-trans {i} (divides-refl q₁) (divides q₂ eq₂) = divides (q₂ * q₁) (trans eq₂ (sym (*-assoc q₂ q₁ i)))

divides-sub : ∀ {i j k} → i ∣ j → i ∣ k → i ∣ (j ∸ k)
divides-sub {i} (divides-refl q₁) (divides-refl q₂) = divides (q₁ ∸ q₂) (sym (*-distribʳ-∸ i q₁ q₂))

divides-one : ∀ i → i ∣ 1 → i ≡ 1
divides-one zero (divides (suc q) eq) rewrite *-comm q 0 = ⊥-elim (1+n≢0 eq)
divides-one (suc zero) (divides (suc q) eq) = refl

divides-not-one : ∀ {i} → i ∣ 1 → i ≢ 1 → ⊥
divides-not-one {zero} (divides q eq) neq rewrite *-comm q 0 = 1+n≢0 eq
divides-not-one {suc zero} (divides q eq) neq = neq refl
divides-not-one {2+ i} (divides zero eq) neq = 1+n≢0 eq
divides-not-one {2+ i} (divides (suc q) eq) neq = 1+n≢0 (sym (suc-injective eq))

lt-left-suc : ∀ i j → i ≤ j → i ≢ j → suc i ≤ j
lt-left-suc zero zero z≤n p = ⊥-elim (p refl)
lt-left-suc zero (suc j) z≤n p = s≤s z≤n
lt-left-suc (suc i) zero () p
lt-left-suc (suc i) (suc j) (s≤s x) p = s≤s (lt-left-suc i j x λ q → p (cong suc q))


not : {A : Set} → Dec A → Dec (¬ A)
not (yes p) = no (λ z → z p)
not (no ¬p) = yes ¬p

DNE : {A : Set} → Dec A → ¬ ¬ A → A
DNE (yes p) f = p
DNE (no ¬p) f = ⊥-elim (f ¬p)

Decide : {A : Set} (P : A → Set) → Set
Decide P = ∀ i → Dec (P i)

lt-lower : ∀ {i j} → suc i ≤ suc j → i ≢ j → suc i ≤ j
lt-lower {zero} {zero} (s≤s p) q = ⊥-elim (q refl)
lt-lower {zero} {suc j} (s≤s p) q = s≤s z≤n
lt-lower {suc i} {suc j} (s≤s p) q = s≤s (lt-lower p λ x → q (cong suc x))

lt-decide : ∀ i → (P : Nat → Set) (p? : ∀ n → n < i → Dec (P n)) → (∀ n → n < i → P n) ⊎ (Σ _ λ j → j < i × ¬ (P j))
lt-decide zero P p? = inj₁ λ _ ()
lt-decide (suc i) P p? with lt-decide i P h
  where
    h : (n : Nat) → n < i → Dec (P n)
    h n lt = p? n (s≤s (<⇒≤ lt))
... | inj₂ (a , b , c) = inj₂ (a , s≤s (≤-trans (n≤1+n a) b) , c)
... | inj₁ x with p? i ≤-refl
... | no ¬a = inj₂ (i , ≤-refl , ¬a)
... | yes a = inj₁ h
  where
    h : (n : Nat) → suc n ≤ suc i → P n
    h n lt with n ≟ i
    ... | yes refl = a
    ... | no ¬a = x n (lt-lower lt ¬a)

¬lt-decide : ∀ i → (P : Nat → Set) (p? : ∀ n → n < i → Dec (P n)) → (∀ n → n < i → ¬ P n) ⊎ (Σ _ λ j → j < i × (P j))
¬lt-decide i P p? with lt-decide i (λ x → ¬ (P x)) (λ n x → not (p? n x))
... | inj₁ x = inj₁ x
... | inj₂ (a , b , c) = inj₂ (a , b , DNE (p? a b) c)

record Prime (n : Nat) : Set where
  constructor isprime
  field
    gt1 : n > 1
    div : ∀ k → k ∣ n → k ≡ 1 ⊎ k ≡ n

open Prime

zero-prime : ¬ (Prime 0)
zero-prime ()

prime-not-zero : ∀ p → Prime p → p ≢ 0
prime-not-zero p x refl = zero-prime x

one-prime : ¬ (Prime 1)
one-prime (isprime (s≤s ()) div)

two-prime : Prime 2
two-prime .gt1 = s≤s (s≤s z≤n)
two-prime .div zero (divides (suc q) eq) rewrite *-comm q 0 = ⊥-elim (1+n≢0 eq)
two-prime .div (suc zero) (divides (suc q) eq) = inj₁ refl
two-prime .div (2+ zero) (divides (suc q) eq) = inj₂ refl

record Composite (n : Nat) : Set where
  constructor composite
  field
    p : Nat
    Pp : Prime p
    p<n : p < n
    p∣ : p ∣ n

not-prime-and-composite : ∀ p → Prime p → Composite p → ⊥
not-prime-and-composite _ (isprime gt2 div₁) (composite p (isprime gt3 div₂) p<n p∣) with div₁ p p∣
... | inj₁ refl = one-prime (isprime gt3 div₂)
... | inj₂ refl = 1+n≰n p<n

prime-or-composite : ∀ p → p > 1 → Prime p ⊎ Composite p
prime-or-composite (suc zero) (s≤s ())
prime-or-composite (2+ p) lt = <-rec _ h p
  where
    h : (x : Nat) →
         ({y : Nat} → suc y ≤ x → Prime (2+ y) ⊎ Composite (2+ y)) →
         Prime (2+ x) ⊎ Composite (2+ x)
    h x f with ¬lt-decide x (λ k → (2+ k) ∣ (2+ x)) (λ n nlt → 2+ n ∣? 2+ x)
    ... | inj₂ (ev₁ , ev₂ , ev₃) with f ev₂
    h x f | inj₂ (ev₁ , ev₂ , ev₃) | inj₁ prm = inj₂ (composite (2+ ev₁) prm (s≤s (s≤s ev₂)) ev₃)
    h x f | inj₂ (ev₁ , ev₂ , ev₃) | inj₂ (composite p Pp (s≤s p<n) p∣) =
        inj₂ (composite p Pp (s≤s (≤-trans p<n (≤-trans ev₂ (n≤1+n x)))) (divides-trans p∣ ev₃))
    h x f | inj₁ eq = inj₁ (isprime (s≤s (s≤s z≤n)) lemma)
      where
        lemma : (k : Nat) → k ∣ 2+ x → k ≡ 1 ⊎ k ≡ 2+ x
        lemma k dv with k ≟ 1 | k ≟ (2+ x)
        ... | no ¬a | yes refl = inj₂ refl
        ... | yes refl | no ¬b = inj₁ refl
        ... | yes refl | yes ()
        lemma zero dv | no ¬a | no ¬b rewrite divides-zero (2+ x) dv = inj₂ refl
        lemma (suc zero) dv | no ¬a | no ¬b = inj₁ refl
        lemma (2+ k) dv | no ¬a | no ¬b with suc k ≤? x
        ... | yes k≤x = ⊥-elim (eq k k≤x dv)
        ... | no ¬k≤x = ⊥-elim (¬k≤x sothen)
          where
            one : 2+ k ≤ 2+ x
            one = div-goes-into (2+ k) (2+ x) 1+n≢0 dv

            two : k ≤ x
            two with one
            ... | s≤s (s≤s a) = a

            also : k ≢ x
            also x = ¬b (cong suc (cong suc x))

            sothen : suc k ≤ x
            sothen = lt-left-suc k x two also

prod-list : List Nat → Nat
prod-list [] = 1
prod-list (x ∷ xs) = x * prod-list xs

prod-list-nz : ∀ xs → (∀ x → x ∈ xs → x > 0) → prod-list xs > 0
prod-list-nz [] f = s≤s z≤n
prod-list-nz (x ∷ []) f rewrite *-comm x 1 rewrite +-comm x 0 = f x (here refl)
prod-list-nz (x ∷ x₁ ∷ xs) f = h {x} (f x (here refl)) (prod-list-nz (x₁ ∷ xs) (λ x₂ z → f x₂ (there z)))
  where
    h : ∀ {i j} → 1 ≤ i → 1 ≤ j → 1 ≤ i * j
    h {suc i} {suc j} (s≤s a) (s≤s b) = s≤s z≤n

prod-list-NZ : ∀ xs → (∀ x → x ∈ xs → x > 0) → NonZero (prod-list xs)
prod-list-NZ xs f = >-nonZero (prod-list-nz xs f)

prod-list-lt : ∀ xs → (∀ x → x ∈ xs → x > 0) → ∀ y → y ∈ xs → y ≤ prod-list xs
prod-list-lt [] f y ()
prod-list-lt (x ∷ xs) f y (here refl) = m≤m*n x (prod-list xs) ⦃ prod-list-NZ xs λ x₂ z → f x₂ (there z) ⦄
prod-list-lt (x ∷ xs) f y (there py) = also (prod-list-lt xs (λ x₂ z → f x₂ (there z)) y py) (f x (here refl))
  where
    lt+ : ∀ {i j k} → i ≤ j → i ≤ j + k
    lt+ z≤n = z≤n
    lt+ (s≤s x) = s≤s (lt+ x)

    also : ∀ {i j k} → i ≤ k → 1 ≤ j → i ≤ j * k
    also a (s≤s z≤n) = lt+ a

prod-list-divides : ∀ xs x → x ∈ xs → x ∣ prod-list xs
prod-list-divides [] x ()
prod-list-divides (y ∷ xs) x (here refl) = divides (prod-list xs) (*-comm y (prod-list xs))
prod-list-divides (y ∷ xs) x (there p) with prod-list-divides xs x p
... | divides q eq rewrite eq = divides (y * q) (sym (*-assoc y q x))

prime-not-in : ∀ xs → (∀ x → x ∈ xs → x > 0) → Σ _ λ k → k ∉ xs × Prime k
prime-not-in xs gt with 2 ≤? prod-list xs
... | no ¬a = 2 , lemma , two-prime
  where
    lemma : 2 ∈ xs → ⊥
    lemma pf with prod-list-lt xs gt 2 pf
    ... | also = ¬a also
... | yes a with prime-or-composite (suc (prod-list xs)) (s≤s (≤-trans (s≤s z≤n) a))
... | inj₁ x = suc (prod-list xs) , lemma , x
  where
    lemma : (suc (prod-list xs)) ∈ xs → ⊥
    lemma pf with prod-list-lt xs gt (suc (prod-list xs)) pf
    ... | also = 1+n≰n also
... | inj₂ (composite p Pp p<n p∣) with p ∈? xs
... | no ¬b = p , ¬b , Pp
... | yes b with prod-list-divides xs p b
... | divs with divides-sub p∣ divs
... | sothen = ⊥-elim (lemma {p} {prod-list xs} sothen λ{ refl → one-prime Pp })
  where
    suc-sub : ∀ i → suc i ∸ i ≡ 1
    suc-sub zero = refl
    suc-sub (suc i) = suc-sub i

    lemma : ∀ {i j} → i ∣ (suc j ∸ j) → i ≢ 1 → ⊥
    lemma {_} {j} div neq rewrite suc-sub j = divides-not-one div neq


list-up-to : Nat → List Nat
list-up-to 0 = 1 ∷ []
list-up-to (suc n) = suc n ∷ list-up-to n

list-up-to-nz : ∀ k x → x ∈ list-up-to k → x > 0
list-up-to-nz zero x (here refl) = s≤s z≤n
list-up-to-nz (suc k) x (here refl) = s≤s z≤n
list-up-to-nz (suc k) x (there p) = list-up-to-nz k x p

list-up-to-contains : ∀ i j → j ≤ i → j ≢ 0 → j ∈ list-up-to i
list-up-to-contains zero zero z≤n b = ⊥-elim (b refl)
list-up-to-contains zero (suc j) () b
list-up-to-contains (suc i) zero z≤n b = ⊥-elim (b refl)
list-up-to-contains (suc i) (suc j) (s≤s a) b with suc i ≟ suc j
... | no ¬c = there (list-up-to-contains i (suc j) (lt-left-suc j i a λ x → ¬c (cong suc (sym x))) b)
... | yes refl = here refl


infinite-primes : ∀ i → Σ _ λ p → p > i × Prime p
infinite-primes zero = 2 , s≤s z≤n , two-prime
infinite-primes (suc i) with prime-not-in (list-up-to (2+ i)) (list-up-to-nz (2+ i))
... | p , notin , Pp = p , DNE (2+ i ≤? p) lemma , Pp
  where
    notzero : p ≢ 0
    notzero = prime-not-zero p Pp

    implies : ∀ {a b} → (suc a ≤ b → ⊥) → (a ≡ b) ⊎ (a > b)
    implies {a} {b} x with compare a b
    ... | less .a k = ⊥-elim (x (s≤s (m≤m+n a k)))
    ... | equal .a = inj₁ refl
    ... | greater .b k = inj₂ (s≤s (m≤m+n b k))

    lemma : ((2+ i ≤ p) → ⊥) → ⊥
    lemma x with implies x
    ... | inj₁ refl = notin (there (here refl))
    ... | inj₂ (s≤s a) = notin (list-up-to-contains (2+ i) p (≤-trans a (≤-trans (n≤1+n i) (n≤1+n (suc i)))) (prime-not-zero p Pp))

来源：Hacker News · blueberrywren.dev

推理能力教程实践#教程/实践#推理