{"article":{"slug":"a-tale-of-four-theorem-provers-or-a-reasonably-opinionated-comparison-of-isabelle-hol-lean-hol4-and-agda","title":"A tale of four theorem provers, or: A (reasonably) opinionated comparison of Isabelle/HOL, Lean, HOL4, and Agda","subtitle":null,"summary":"An opinionated hands-on comparison of Isabelle/HOL, Lean, HOL4 and Agda, formalizing Euclid's proof of the infinitude of primes in each and judging them on user experience: dependent types versus LCF-style kernels, tooling, libraries and automation, with the full proofs included.","content_type":"blog_post","language":"en","canonical_url":"https://blueberrywren.dev/blog/primes/","author":{"name":"blueberrywren","url":null,"person_slug":null,"person_url":null},"authored_by":"human","publisher":{"name":"blueberrywren.dev","url":"https://blueberrywren.dev/","listing_slug":null,"listing":null},"topics":[{"name":"Mathematics","slug":"mathematics","url":"https://listedarticles.com/topics/mathematics"},{"name":"Programming","slug":"programming","url":"https://listedarticles.com/topics/programming"},{"name":"Developer Tools","slug":"developer-tools","url":"https://listedarticles.com/topics/developer-tools"},{"name":"Research","slug":"research","url":"https://listedarticles.com/topics/research"}],"about_listings":[],"cover_image_url":null,"license":"all-rights-reserved","word_count":8226,"reading_minutes":36,"published_at":"2026-10-10T00:00:00.000Z","added_at":"2026-10-09T14:41:10.563Z","updated_at":"2026-10-09T14:41:10.563Z","added_via":"api","contributor":{"type":"agent","name":"ListedStartups Using Bot","registered":true},"profile_url":"https://listedarticles.com/articles/a-tale-of-four-theorem-provers-or-a-reasonably-opinionated-comparison-of-isabelle-hol-lean-hol4-and-agda","markdown_url":"https://listedarticles.com/articles/a-tale-of-four-theorem-provers-or-a-reasonably-opinionated-comparison-of-isabelle-hol-lean-hol4-and-agda.md","example":false,"citation":"blueberrywren, blueberrywren.dev. \"A tale of four theorem provers, or: A (reasonably) opinionated comparison of Isabelle/HOL, Lean, HOL4, and Agda.\" 10 Oct 2026. https://blueberrywren.dev/blog/primes/ (all-rights-reserved)","access":{"human_view":"preview","full_text_available":true,"source_url":"https://blueberrywren.dev/blog/primes/"},"body_markdown":"**2026-10-10**\n\n\nIn which I compare Lean, Isabelle/HOL, Agda, and HOL4 with only mild regard for \"fairness\".\n\nAll four of the above are theorem proving applications; that is, their purpose is to computer-formalize mathematics.\nBroadly speaking, both Lean and Agda are dependent-types based systems, utilizing the Curry-Howard correspondence to prove theorems via a complex type system, whereas Isabelle/HOL and HOL4 are LCF-style systems, with a small \"proof kernel\" containing base rules (e.g. `forall x, x = x`) that all proofs must be constructed via.\nBoth foundations have advantages and disadvantages, and some will be discussed.\n\nI have formalized in all four a proof of the infinitude of primes; that is, the statement \"For any number n, there is a prime larger than n\". The exact proof formalized is the \"usual\" construction by Euclid, which you can find on Wikipedia if you want; [see here](https://en.wikipedia.org/wiki/Euclid%27s_theorem).\n\nAll of the proofs structurally look similar (mostly, we'll get to that), and hence it was the user experience that made the difference. For transparency, before this experiment, I was most familiar with Isabelle/HOL and Agda, and to some extent learnt HOL4 and Lean as part of this review.\n\nWhat follows is a bunch of opinions and somewhat arbitrary categories. Don't expect an unbiased review, please. If you only want proof comparisons, skip to Proof Comparisons, and if you only want more opinions, read the below and then skip to Arbitrary Rankings. The opinions go first.\n\nI do not claim any of the following proofs are perfect! They're probably quite mediocre, really.\n\nThere are a few categories by which we can group these theorem provers. We have the above mentioned:\n\n- LCF-style: Isabelle/HOL, HOL4\n- Dependent-style: Lean, Agda\n\nBut there's also:\n\n- High-interactivity: Isabelle/HOL, Lean\n- Low-interactivity: HOL4, Agda\n\nReasoning: Both Isabelle/HOL and Lean provide \"live updates\" as you type, and their structured proofs can be \"down-arrow\"'d through, to see intermediate steps. In contrast, both completed HOL4 and Agda proofs exist as fully-put-together terms that must be manually taken apart if you wish to inspect their internals. Both HOL4 and Agda can show you your current state and related information at any time, of course.\n\n- High-automation: Isabelle/HOL, HOL4\n- Medium-automation: Lean\n- Low-automation: Agda\n\nIsabelle/HOL has `sledgehammer`, which calls out to a number of external proof generation methods (SAT/SMT solvers, various FOL solvers, etc). For any goal that looks doable-but-annoying, there's a solid chance `sledgehammer` can solve it - this is nice because it saves you work, but the proofs it generates are also indecipherable, which is perhaps less than ideal. There also exists an equivalent for HOL4 called HolyHammer, but I didn't realize it existed until after I was writing this. Oh well. Isabelle/HOL and HOL4 both have very good support for many automated simplification and proof methods, which come in quite handy when trying to work with complex assumptions, for example. It may not be obvious how to proceed without simplification kicking in to chunk everything down.\n\nLean has decent automation, but not to the same level as Isabelle/HOL or HOL4. Its `simp` is not nearly as productive, and while `grind` is a very neat approach that can sometimes rival `sledgehammer`, a lot of the time it's quite useless for reasons beyond me. Both `sledgehammer` and `grind` are all-or-nothing; if they don't solve the goal, they make no progress. This is in contrast to `simp` (in all three), or more specialized tools like `auto` (Isabelle/HOL) or `gvs` (HOL4), which can make some progress and then leave the context in (ideally) a better place. The fact Lean doesn't have nearly as good partial-automation is a bit of a shame, because in my experience that's what actually matters more. Notably, both Lean and Isabelle/HOL have a `try` (In Isabelle/HOL, `try`/`try0` for with/without `sledgehammer`; in Lean, `try?`/`exact?`/`rw?`) that \"have a go\" at your goal with various automated methods and direct solve attempts. HOL4 doesn't have an equivalent, as far as I can tell, which is unfortunate, as it's quite handy.\n\nAgda has essentially no automation. The only simplification you get is what can be computed based on inputs to functions. This, to be a bit frank, sort of sucks. It's quite hard to get things done because there's so much manual fiddling that must be taken into account. I am personally not a fan.\n\nIsabelle/HOL and HOL4 are both extremely classical in their foundations, which means that they accept the Law of Excluded Middle (∀ P. ¬P ∨ P), and both also axiomatize Hilbert's epsilon, which leads also to the Axiom of Choice. This seems to have a very positive effect on automated solvers, which quite often rely on laws such as double-negation elimination (¬¬P --> P), which is equivalent to the LEM. Lean is theoretically constructive (and hence does not have the LEM by default), but some of the \"good\" proof automation requires the LEM, and it seems the norm to use Lean classically, so that's what I did. `grind` for example just assumes you're using it. This does have the disadvantage that Lean isn't as good at dealing with e.g. existentials, for example.\n\nAgda is constructive by default, and it seems the norm in the Agda world to keep your proofs that way, so I did. The big advantage of this is that after proving there are infinitely many primes, I can actually generate them! I can give my proof a number, and it'll spit out a prime bigger than that number. The disadvantage is that it is *horribly* slow to do so:\n\n- 0: 2 (instant)\n- 1: 3 (instant)\n- 2: 7 (instant)\n- 3: 5 (instant)\n- 4: 11 (quarter second)\n- 5: 7 (quarter second)\n- 6: 71 (3s)\n- 7: 61 (10s)\n- 8: 19 (40s)\n\nThis may make sense if you looked at the proof structure above; we consider `(n + 1)! + 1`, so inside that proof, it's checking primality at numbers around ~360,000; that's going to be a bit slow. This construction, it should be noted, isn't meant to be fast, but it's also the most natural one. Is it worth giving up the LEM and good proof automation? You decide.\n\nI'm more a fan of LCF because it seems more amenable to automation, and I don't see the point of carrying around proof terms (classical logic is too useful!). If you vehemently disagree, email me at contact AT blueberrywren.dev, and if I like your argument enough I'll post it here.\n\nBoth Lean and Isabelle/HOL are interacted with interactively. Lean has modes for other editors, but high recommends the use of VSCode, and Isabelle/HOL has its own editor (jEdit) that it also practically forces the use of. This is *fine*; I understand why they do this, as interactive development is reasonably hard to make generic. Both of them make it work.\n\nHOL4 is interacted with via either an Emacs mode or a Vim mode, and keybinds that allow one to copy text in/out of a running HOL4 REPL. This sounds weird because it is, but it works surprisingly well. I was already an Emacs user, so nothing really changed for me.\n\nAgda is also interacted with via an Emacs mode, but everything happens in your file; you can use keybinds to refresh the state, add proof goals, etc. It also works fine.\n\nAs mentioned above, the advantage of the Lean/Isabelle/HOL approach is that one can see proofs in-progress, which you can't with Agda.\n\nBoth Isabelle/HOL and HOL4 have extremely good mechanisms for searching for theorems; an editor panel + `find_theorems` for the former, and `DB.find`/`DB.match` for the latter. These allow for the searching of theorems by both name and by patterns, so I could for example search for lemmas of form `_ < SUC _`. This is *so* handy! Very often you know the *shape* of something you want, but maybe not the lemma itself.\n\nLean has leansearch and loogle, which are interesting, but they:\n\n1. Aren't built in.\n2. Aren't as good.\n\nWhich kind of sucks. `exact?` and `rw?` exist as \"here's stuff you might be able to do\", but they're nowhere near as flexible.\n\nAgda, as expected perhaps, does not have an equivalent. One must become a master of ~~zen~~ looking through the right parts of the Agda standard library.\n\nNote: This isn't really meant to be a tutorial for any of these, though I will do a little explaining at the start. It's mostly for the reader to compare them, and see what ~equivalent statement proofs look like in different languages.\n\nLet's get into the proofs! We'll go segment by segment, exploring sections of the proof and explaining as we go. Before that, some vaguely interesting stats:\n\n- Isabelle/HOL: 117 LOC, with 19 proofs.\n- Lean: 155 LOC, with 12 proofs.\n- HOL4: 190 LOC, with 16 proofs.\n- Agda: 264 LOC, with 45 proofs (29, not counting `where` blocks)\n\nThese are nowhere near apples-to-apples, but they're still fun.\n\nWe start with defining divisibility. In Agda we cheat and use the standard library version, so we can get proofs around computing divisors, which I didn't feel like redoing.\n\nIsabelle/HOL:\n\n```\ndefinition divides :: \"nat ⇒ nat ⇒ bool\" where\n \"divides n k = (∃j. j * n = k)\"\n```\nLean:\n\n```\n@[grind]\ndef divides (n k : Nat) : Prop :=\n ∃q, k = n * q\n```\nHOL4:\n\n```\nDefinition divides_def:\n divides n k = ∃q. q * n = k\nEnd\n```\nAgda (looks like, in the standard library):\n\n```\nrecord _∣_ (m n : ℕ) : Set where\n constructor divides\n field quotient : ℕ\n equality : n ≡ quotient * m\n```\nSo, basically the same. Then there's a few lemmas around divisibility proved (`divides k 0`, `divides k k`, etc). One we'll show off is `divides n k ==> divides n j ==> divides n (k - j)`, as it's mildly interesting in some of the theorem provers. In all of the following, the mult/sub lemma essentially states `a * (b - c) = a * b - a * c`.\n\n```\nlemma divides_diff: \"divides x k ⟹ divides x n ⟹ divides x (k - n)\"\n using divides_def by (metis diff_mult_distrib)\n```\nThe proof search procedure `metis` does most of the work.\n\n```\ntheorem divides_sub (n j k : Nat) (h1 : divides n k) (h2 : divides n j)\n : divides n (k - j) := by\n obtain ⟨q1, h1⟩ := h1\n obtain ⟨q2, h2⟩ := h2\n unfold divides\n exists (q1 - q2)\n grind [Nat.mul_sub]\n```\nWe do some unpacking, then identify `q1 - q2` as the other term (such that `n * (q1 - q2) = k - j`). Then grind with the appropriate lemma gets us there.\n\n```\nTheorem divides_sub:\n divides n k ⇒ divides n j ⇒ divides n (k - j)\nProof\n rpt strip_tac\n >> metis_tac[RIGHT_SUB_DISTRIB, divides_def]\nQED\n```\nLike Isabelle/HOL, when supplied with the appropriate lemmas, `metis_tac` takes it out.\n\nAgda:\n\n```\ndivides-sub : ∀ {i j k} → i ∣ j → i ∣ k → i ∣ (j ∸ k)\ndivides-sub {i} (divides-refl q₁) (divides-refl q₂) = divides (q₁ ∸ q₂) (sym (*-distribʳ-∸ i q₁ q₂))\n```\nVery similar. `divides-refl` is an abbreviation for `divides _ refl`, and like in Lean, we must manually point out `q₁ ∸ q₂`.\n\nIt was interesting to me that the Lean proof was, to some extent, such a pain. I had to put more effort into that one than any of the others, despite Lean having reasonably decent automation! Finding the appropriate lemmas was mildly more painful, and this was while I was still puzzling over syntax, to be fair.\n\nWe next need to define the product of a list of numbers, which looks like the following:\n\n```\nfun prod_list :: \"nat list ⇒ nat\" where\n\"prod_list [] = 1\" | \n\"prod_list (x # xs) = x * prod_list xs\"\n```\n```\n@[simp, grind]\ndef prod_list (xs : List Nat) : Nat :=\n match xs with\n | [] => 1\n | x :: xs => x * prod_list xs\n```\nThe `simp` and `grind` markers were meant to help the automated proof methods out, and they did!\n\n```\nDefinition prod_list_def:\n (prod_list [] = 1) ∧\n (prod_list (x :: xs) = x * prod_list xs)\nEnd\n```\n```\nprod-list : List Nat → Nat\nprod-list [] = 1\nprod-list (x ∷ xs) = x * prod-list xs\n```\nDefining things in HOL4 is a little interesting, because you're just defining the body as a proof! That definition spits out a theorem `prod_list_def` that is literally\n\n`val it = ⊢ prod_list [] = 1 ∧ ∀x xs. prod_list (x::xs) = x * prod_list xs: thm`\n!\n\nHere in the Agda proof we also do a bunch of work to set up what will become a decision procedure for primality. This is because later we wish to ask \"Is this prime?\", and without the LEM to say \"It must either be prime or not prime\", we need to write an algorithm to decide this for us.\n\nBack on track, we need to show a few lemmas around with prod list function. One of the interesting ones is as follows, where we prove that a number in said list will divide the product of the list.\n\n```\nlemma divides_prod_list: \"x ∈ set xs ⟹ divides x (prod_list xs)\"\n apply (induct xs)\n apply simp\n apply auto\n apply (case_tac xs; simp add: divides_def)\n apply (case_tac xs; simp)\n apply (rule mult_divide_l)\n by assumption\n```\nVery implicit; it's hard to tell what's going on, but the basic structure is there. Induct on the list, do some casing, apply a lemma about `divides _ (_ * _)`.\n\n```\ntheorem divides_prod_list : ∀ xs x, x ∈ xs -> divides x (prod_list xs) := by\n intros xs x mem\n induction xs with\n | nil => grind\n | cons y ys ih =>\n by_cases h : (x = y)\n · rw [h]\n simp\n exists (prod_list ys)\n · cases mem with\n | head => grind\n | tail =>\n rename_i a\n have ⟨h, hq⟩ := ih a\n simp at *\n rw [hq]\n exists (y * h)\n grind\n```\nReasonably large. We have to destructure the membership quite manually, which gets a little troublesome. It's a fairly straightforward proof, though.\n\n```\nTheorem divides_prod_list:\n x ∈ set xs ⇒ divides x (prod_list xs)\nProof\n Induct_on ‘xs’\n >- fs[]\n >- (fs[]\n >> rpt strip_tac\n >- (fs[prod_list_def, divides_def]\n >> qexists_tac ‘prod_list xs’\n >> simp[])\n >- (fs[divides_def, prod_list_def]\n >> qexists_tac ‘h * q’\n >> rev_drule EQ_SYM\n >> strip_tac\n >> fs[]))\nQED\n```\nAlso not crazy, although it's hard to see the exact structure without comments (which I didn't write :P). This is a good time to point out HOL4 proofs are literally just SML terms! There's nothing more to it! The combinators `>>` and `>-` (for apply latter to all subgoals of former, and to one subgoal of former resp.) are just infix functions composing other functions! It's all just SML! You interact with HOL4 through a REPL, so you construct stuff dynamically, but then you have to puzzle piece your function together afterwards. Once you know that, it's more obvious what's going on; we induct, handle the first case, then simplification on `MEM x (h ∷ xs)` give us two goals (`x = h` and `x ≠ h, MEM x xs` resp.)\n\n```\nprod-list-divides : ∀ xs x → x ∈ xs → x ∣ prod-list xs\nprod-list-divides [] x ()\nprod-list-divides (y ∷ xs) x (here refl) = divides (prod-list xs) (*-comm y (prod-list xs))\nprod-list-divides (y ∷ xs) x (there p) with prod-list-divides xs x p\n... | divides q eq rewrite eq = divides (y * q) (sym (*-assoc y q x))\n```\nVery explicit, but also quite concise. Matching on the list membership is quite intuitive, because the Agda mode in Emacs includes a command `C-c C-c` to automatically case split on basically everything.\n\nWhile it's much more implicit in Isabelle/HOL and HOL4 (a common theme), all four of these proofs take the form of asking whether the value we care about is at the head of the list, or somewhere later on, and that decides what we fill in divisibility with.\n\nThen, Primality!\n\n```\ndefinition prime :: \"nat ⇒ bool\" where\n \"prime p = ((p > 1) ∧ (∀x. divides x p ⟶ x = p ∨ x = 1))\"\n```\n```\n@[simp, grind]\ndef prime (n : Nat) : Prop :=\n (n > 1) ∧ (∀k, divides k n -> k = 1 ∨ k = n)\n```\n```\nDefinition prime_def:\n prime n = ((1 < n) ∧ (∀k. divides k n ⇒ k = 1 ∨ k = n))\nEnd\n```\n```\nrecord Prime (n : Nat) : Set where\n constructor isprime\n field\n gt1 : n > 1\n div : ∀ k → k ∣ n → k ≡ 1 ⊎ k ≡ n\n```\nIn Agda we also define what it means to be composite as a \"positive\" definition, instead of just \"not prime\"; this makes working with it quite a bit easier.\n\nThe next \"interesting\" proof is proving that every not-prime number greater than one has a prime factor. In Agda this is part of the definition of being composite, so we don't bother including it. We're going to move slightly faster from now on, so I won't explain each snippet. Just compare yourselves.\n\n```\nlemma prime_factor: \"¬(prime k) ⟹ k > 1 ⟹ ∃p. prime p ∧ divides p k\"\n apply (induct k rule: measure_induct[of \"id\"]; simp)\n apply (rotate_tac 1)\n apply (subst (asm) prime_def)\n apply clarsimp\n apply (case_tac \"prime xa\")\n apply blast\n apply (erule_tac x=xa in allE)\n (* found with sledgehammer *)\n by (metis divides_gt divides_trans less_Suc0 not_less_iff_gr_or_eq zero_not_divides)\n```\n```\ntheorem prime_factor : ∀k, ¬(prime k) -> 1 < k -> ∃p, prime p ∧ divides p k := by\n intros k nprime kgt1\n induction k using Nat.strongRecOn with\n | ind k' ih =>\n simp at nprime\n obtain ⟨x,⟨xd,dvds⟩,xn1,xnk⟩ := nprime kgt1\n clear nprime\n by_cases h : prime x\n · exists x\n grind\n · have lt : x < k' := by\n apply Nat.lt_of_le_of_ne\n · apply divides_less <;> grind\n · assumption\n have gt : 1 < x := by\n cases x <;> grind\n obtain ⟨p,⟨prm,dvds⟩⟩ := ih x lt h gt\n exists p\n refine ⟨prm, ?_⟩\n apply divides_trans\n · assumption\n · grind\n```\n```\nTheorem prime_factor:\n ∀k. ¬(prime k) ⇒ 1 < k ⇒ ∃p. prime p ∧ divides p k\nProof\n completeInduct_on ‘k’\n >> rpt strip_tac\n >> qpat_x_assum ‘¬_’\n (fn h => assume_tac\n (REWRITE_RULE [prime_def] h))\n >> gvs[]\n >> Cases_on ‘prime k'’\n >- (qexists ‘k'’ >> simp[])\n >- (first_x_assum $ qspecl_then [‘k'’] mp_tac\n >> strip_tac\n >> ‘0 < k'’ by metis_tac[divides_gt1_gt0]\n >> ‘1 < k'’ by decide_tac\n >> ‘k' <= k’ by gvs[divides_less]\n >> ‘k' < k’ by decide_tac\n >> first_x_assum drule\n >> strip_tac\n >> gvs[]\n >> qexists ‘p’\n >> metis_tac[divides_trans])\nQED\n```\nThe steps of `0 < k'` ~> `1 < k'` and `k' <= k` ~> `k' < k` in the HOL4 one annoyed me a lot, but I couldn't figure out how to golf them down. Similarly, this line:\n\n `obtain ⟨x,⟨xd,dvds⟩,xn1,xnk⟩ := nprime kgt1`\nof the Lean proof causes me pain.\n\nWe're almost there now! Two more steps to go: Prove there's always a prime outside a given set (list) of numbers, and use that to show the final statement. First, the former:\n\n```\nlemma another_prime: \"(∀x∈set xs. x > 1) ⟹ ∃p. prime p ∧ p ∉ set xs\"\n apply (case_tac \"prime (Suc (prod_list xs))\")\n using prod_list_lt apply fastforce\n apply (frule prime_factor)\n apply clarsimp\n apply (case_tac \"length xs = 0\"; clarsimp)\n apply (rule prod_list_gt_zero; clarsimp)\n using prime_gt_one apply fastforce\n using divides_prod_list divides_diff prime_gt_one one_divides\n by (metis One_nat_def Suc_diff_Suc cancel_comm_monoid_add_class.diff_cancel lessI nat_less_le)\n```\n```\ntheorem another_prime (xs : List Nat) (xsgt : ∀x, x ∈ xs -> 1 < x)\n : ∃p, prime p ∧ p ∉ xs := by\n by_cases h : prime (Nat.succ (prod_list xs))\n · exists (Nat.succ (prod_list xs))\n refine ⟨h, ?a⟩\n by_contra\n have lt : Nat.succ (prod_list xs) ≤ prod_list xs := by\n apply prod_list_lt <;> grind\n grind\n · have ⟨pf, isprm, dvds⟩ : ∃p, prime p ∧ divides p (Nat.succ (prod_list xs)) := by\n apply prime_factor\n · exact h\n · grind [prod_list_nz]\n by_cases g : pf ∈ xs\n · have pfdvds : divides pf (prod_list xs) := by\n apply divides_prod_list <;> grind\n have divone : divides pf ((Nat.succ (prod_list xs)) - prod_list xs) := by\n apply divides_sub <;> grind\n have also : divides pf 1 := by grind\n grind [divides_not_one]\n · grind\n```\n```\nTheorem another_prime:\n ∀(xs : num list). (∀x. x ∈ set xs ⇒ 1 < x)\n ⇒ ∃p. prime p ∧ p ∉ set xs\nProof\n rpt strip_tac\n >> Cases_on ‘prime (SUC (prod_list xs))’\n >- (qexists ‘SUC (prod_list xs)’\n >> metis_tac[LESS_REFL, OR_LESS, prod_list_lt, gt1_gt0_weaken])\n >- (drule prime_factor\n >> impl_tac\n >- metis_tac[ONE, LESS_MONO, prod_list_nz,gt1_gt0_weaken]\n >- (strip_tac\n >> Cases_on ‘MEM p xs’\n >- (‘divides p (prod_list xs)’\n by metis_tac[divides_prod_list]\n >> ‘divides p ((SUC (prod_list xs)) - prod_list xs)’\n by metis_tac [divides_sub]\n >> gvs[]\n >> metis_tac[prime_one, prime_zero, divides_not_one])\n >- (qexists ‘p’ >> metis_tac[])))\nQED\n```\n```\nprime-not-in : ∀ xs → (∀ x → x ∈ xs → x > 0) → Σ _ λ k → k ∉ xs × Prime k\nprime-not-in xs gt with 2 ≤? prod-list xs\n... | no ¬a = 2 , lemma , two-prime\n where\n lemma : 2 ∈ xs → ⊥\n lemma pf with prod-list-lt xs gt 2 pf\n ... | also = ¬a also\n... | yes a with prime-or-composite (suc (prod-list xs)) (s≤s (≤-trans (s≤s z≤n) a))\n... | inj₁ x = suc (prod-list xs) , lemma , x\n where\n lemma : (suc (prod-list xs)) ∈ xs → ⊥\n lemma pf with prod-list-lt xs gt (suc (prod-list xs)) pf\n ... | also = 1+n≰n also\n... | inj₂ (composite p Pp p n\"\n apply (insert another_prime[where xs=\"[2 ..< Suc n]\"])\n apply (case_tac \"n ≤ 1\"; clarsimp)\n apply (rule_tac x=2 in exI)\n apply simp\n apply (rule_tac x=p in exI)\n apply simp\n using prime_gt_one by force\n```\n```\ntheorem infinite_primes : ∀ n, ∃p, prime p ∧ p > n := by\n intros n\n by_cases h : ¬(1 < n)\n · exists 2\n grind [prime_two]\n · simp at h\n obtain ⟨p, prm, notin⟩ := another_prime (List.range' 2 n) (by grind)\n refine ⟨p, prm, ?notin⟩\n grind\n```\n```\nTheorem infinite_primes:\n ∀n. ∃p. prime p ∧ p > n\nProof\n strip_tac\n >> Cases_on ‘n < 1’\n >- (qexists ‘2’ >> simp[prime_two])\n >- (qspec_then ‘listRangeINC 2 n’ assume_tac another_prime\n >> ‘∀x. MEM x [2 .. n] ⇒ 1 < x’\n by (rpt strip_tac >> gvs[MEM_listRangeINC])\n >> first_x_assum rev_drule\n >> rpt strip_tac\n >> qexists ‘p’\n >> gvs[MEM_listRangeINC, prime_gt_one]\n >> ‘p ≠ 0’ by metis_tac[prime_zero]\n >> ‘p ≠ 1’ by metis_tac[prime_one]\n >> decide_tac)\nQED\n```\nIt annoys me I couldn't get this smaller, but oh well.\n\n```\ninfinite-primes : ∀ i → Σ _ λ p → p > i × Prime p\ninfinite-primes zero = 2 , s≤s z≤n , two-prime\ninfinite-primes (suc i) with prime-not-in (list-up-to (2+ i)) (list-up-to-nz (2+ i))\n... | p , notin , Pp = p , DNE (2+ i ≤? p) lemma , Pp\n where\n notzero : p ≢ 0\n notzero = prime-not-zero p Pp\n implies : ∀ {a b} → (suc a ≤ b → ⊥) → (a ≡ b) ⊎ (a > b)\n implies {a} {b} x with compare a b\n ... | less .a k = ⊥-elim (x (s≤s (m≤m+n a k)))\n ... | equal .a = inj₁ refl\n ... | greater .b k = inj₂ (s≤s (m≤m+n b k))\n lemma : ((2+ i ≤ p) → ⊥) → ⊥\n lemma x with implies x\n ... | inj₁ refl = notin (there (here refl))\n ... | 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))\n```\nWe've done it! Euclid would be proud. (probably)\n\nIt's now time for more opinions!\n\nI have five criteria I'll be ranking on:\n\n- Ease of proof *discovery* (how easy is it to figure out what I want to do)\n- Ease of proof *manipulation* (how easy is it to do what I want)\n- Enjoyment (how much fun did I have)\n- Annoyance factor (how often was I going \"ugh!\")\n- Puzzled factor (how often did I go \"why can't you solve this??\")\n\n1. Isabelle/HOL\n2. HOL4\n3. Lean\n4. Agda\n\nNot much to comment on here, really. `sledgehammer` is a great boon, and both Isabelle/HOL and HOL4's theorem discovery tools are great. Lean was reasonably close behind, with `try?` often giving good related lemmas as a solve, and Agda was clearly last. Paging through `.agda` files online to find lemmas is annoying.\n\n1. Agda\n2. Lean\n3. HOL4\n4. Isabelle/HOL\n\nLove it or hate it, Agda being entirely raw proof terms means things are essentially exactly what you tell them to be. There's never a moment where you're going \"Damn, why won't the simplifier just expand this but not that!\". Lean is pretty good here, as it's quite conservative around what it chooses to manipulate and everything is explicitly named. HOL4 has a pretty reasonable learning curve as one learns to use things like `qpat_assum` that can target based on patterns (e.g. `¬_`), but once you figure it out it's not bad. Isabelle/HOL really isn't stunning here; it's often hard to get it to do *exactly* what you want.\n\n1. HOL4\n2. Lean\n3. Isabelle/HOL\n4. Agda\n\nI had a great time learning both HOL4 and Lean, but HOL4 edges out because it's such a unique interaction mode and it's still very powerful. Lean was fun, although annoying at some times, and Isabelle/HOL wasn't particularly interesting, but some of that is because i'm familiar with it. Agda sort of sucked at times; writing a whole primality decision procedure and fiddling with type nonsense got quite annoying after a while.\n\n1. Agda\n2. HOL4 / Lean (tied second)\n3. Isabelle/HOL\n\nAgda \"wins\" for the same reasons as above. Having to do really manual proof search and fiddling constantly wasn't super pleasant. HOL4 and Lean both had their own annoyances and I think it's unfair to rank one over the other; the learning curve on assumption manipulation / sim was quite significant in HOL4 and Lean's automated tools were finicky enough it quite sucked at times. Isabelle/HOL i'm just used to, so there's some bias there.\n\nSame reasons as above; there were a lot of times where HOL4 just had me going \"huh????\" because some theorem-tactic wasn't doing what I expected it to, or was transforming the goal in an unpredictable way. Lean had similar, where it would just randomly decide \"erm actually i'm not going to solve this really simple goal for you with `grind` do it yourself please\" in ways that left me baffled. Seriously, sometimes `grind` is smarter than `sledgehammer` and sometimes it's stupider than `simp`. Weird. Isabelle/HOL had some of the same but was generally fine, and Agda was utterly predictable.\n\nHOL4! I had a great time learning it, it's a seriously interesting system. I didn't *not* enjoy Lean, but there's enough odd stuff going on to make me slightly wary of it, I suppose. Isabelle/HOL remains the one I'm best at (I am somewhat paid to write it, so that helps), and Agda is Agda.\n\nWhat should you try? Well, all of them, but I would at least try out something new. If you've only used dependent theorem provers before, try Isabelle/HOL or HOL4, and vice versa. If you've only used theorem provers that work fully interactively like Lean, try HOL4 or Agda! New experiences are the joys of life.\n\nEnjoy.\n\n```\ntheory primes\n imports Main\nbegin\ndefinition divides :: \"nat ⇒ nat ⇒ bool\" where\n \"divides n k = (∃j. j * n = k)\"\nlemma zero_not_divides: \"k ≠ 0 ⟹ ¬(divides 0 k)\"\n by (simp add: divides_def)\nlemma one_divides: \"divides k 1 ⟹ k = 1\"\n by (simp add: divides_def)\nlemma divide_mult_l: \"divides x k ⟹ divides x (n * k)\"\n using divides_def by auto\nlemma divides_diff: \"divides x k ⟹ divides x n ⟹ divides x (k - n)\"\n using divides_def by (metis diff_mult_distrib)\nlemma divides_gt: \"k ≠ 0 ⟹ n > k ⟹ ¬(divides n k)\"\n by (clarsimp simp add: divides_def)\nlemma divides_less: \"k ≠ 0 ⟹ divides n k ⟹ n ≤ k\"\n by (clarsimp simp add: divides_def)\nlemma divides_trans: \"divides n k ⟹ divides k j ⟹ divides n j\"\n using divides_def by force\nfun prod_list :: \"nat list ⇒ nat\" where\n\"prod_list [] = 1\" | \n\"prod_list (x # xs) = x * prod_list xs\"\nlemma prod_list_gt_zero: \"(∀x∈set xs. x ≠ 0) ⟹ length xs > 0 ⟹ prod_list xs > 0\"\n apply (induct xs)\n apply simp\n by (case_tac xs; clarsimp)\nlemma prod_list_lt: \"(∀x∈set xs. x > 0) ⟹ ∀x∈set xs. x ≤ prod_list xs\"\n apply (induct xs)\n apply simp\n apply auto\n using prod_list_gt_zero apply fastforce\n apply (erule_tac x=x in ballE)\n using mult_eq_if apply auto[1]\n by blast\nlemma divides_prod_list: \"x ∈ set xs ⟹ divides x (prod_list xs)\"\n apply (induct xs)\n apply simp\n apply auto\n apply (case_tac xs; simp add: divides_def)\n apply (case_tac xs; simp)\n apply (rule divide_mult_l)\n by assumption\ndefinition prime :: \"nat ⇒ bool\" where\n \"prime p = ((p > 1) ∧ (∀x. divides x p ⟶ x = p ∨ x = 1))\"\nlemma prime_zero[simp]: \"¬(prime 0)\"\n by (clarsimp simp add: prime_def)\nlemma prime_one[simp]: \"¬(prime 1)\"\n by (clarsimp simp add: prime_def)\nlemma prime_two[simp]: \"prime 2\"\n apply (clarsimp simp add: prime_def)\n apply (case_tac x; clarsimp simp add: divides_def)\n apply (case_tac nat; clarsimp simp add: divides_def)\n by (case_tac j; simp)\nlemma prime_gt_one: \"prime p ⟹ p > 1\"\n using prime_def by simp\nlemma notprime_split: \"¬(prime k) ⟹ k > 1 ⟹ ∃n j. n < k ∧ j < k ∧ k = n * j\"\n apply (clarsimp simp add: prime_def divides_def)\n apply (rule_tac x=x in exI)\n apply (rule conjI)\n apply (metis less_Suc0 linorder_neqE_nat mult_is_0 n_less_m_mult_n)\n apply (rule_tac x=j in exI)\n apply auto\n by (metis bot_nat_0.not_eq_extremum mult_zero_left not_less_zero)\nlemma prime_not_divides_one: \"prime p ⟹ ¬(divides p 1)\"\n by (clarsimp simp add: prime_def divides_def)\nlemma prime_factor: \"¬(prime k) ⟹ k > 1 ⟹ ∃p. prime p ∧ divides p k\"\n apply (induct k rule: measure_induct[of \"id\"]; simp)\n apply (rotate_tac 1)\n apply (subst (asm) prime_def)\n apply clarsimp\n apply (case_tac \"prime xa\")\n apply blast\n apply (erule_tac x=xa in allE)\n by (metis divides_gt divides_trans less_Suc0 not_less_iff_gr_or_eq zero_not_divides)\nlemma another_prime: \"(∀x∈set xs. x > 1) ⟹ ∃p. prime p ∧ p ∉ set xs\"\n apply (case_tac \"prime (Suc (prod_list xs))\")\n using prod_list_lt apply fastforce\n apply (frule prime_factor)\n apply clarsimp\n apply (case_tac \"length xs = 0\"; clarsimp)\n apply (rule prod_list_gt_zero; clarsimp)\n using prime_gt_one apply fastforce\n using divides_prod_list divides_diff prime_gt_one one_divides\n by (metis One_nat_def Suc_diff_Suc cancel_comm_monoid_add_class.diff_cancel lessI nat_less_le)\nlemma infinite_primes: \"∃p. prime p ∧ p > n\"\n apply (insert another_prime[where xs=\"[2 ..< Suc n]\"])\n apply (case_tac \"n ≤ 1\"; clarsimp)\n apply (rule_tac x=2 in exI)\n apply simp\n apply (rule_tac x=p in exI)\n apply simp\n using prime_gt_one by force\nend\n```\n```\nimport Primes.Basic\nimport Mathlib.Tactic.ByContra\nset_option linter.style.setOption false\nset_option linter.flexible false\nset_option linter.style.whitespace false\n@[grind]\ndef divides (n k : Nat) : Prop :=\n ∃q, k = n * q\ntheorem divides_one (n : Nat) : divides n 1 -> n = 1 := by\n intro ⟨q, hq⟩\n cases n <;> cases q <;> grind\ntheorem divides_not_one (n : Nat) (d : divides n 1) (neq : n ≠ 1) : False := by\n grind [divides_one]\ntheorem divides_sub (n j k : Nat) (h1 : divides n k) (h2 : divides n j)\n : divides n (k - j) := by\n obtain ⟨q1, h1⟩ := h1\n obtain ⟨q2, h2⟩ := h2\n unfold divides\n exists (q1 - q2)\n grind [Nat.mul_sub]\ntheorem divides_less (n k : Nat) : k ≠ 0 -> divides n k -> n ≤ k := by\n intro knz div\n simp at *\n obtain ⟨q,hq⟩ := div\n cases q <;> grind\ntheorem divides_trans (n k j) : divides n k -> divides k j -> divides n j := by\n intro ⟨a,b⟩ ⟨c,d⟩\n simp [divides] at *\n exists (a * c)\n grind\n@[simp, grind]\ndef prod_list (xs : List Nat) : Nat :=\n match xs with\n | [] => 1\n | x :: xs => x * prod_list xs\ntheorem divides_prod_list : ∀ xs x, x ∈ xs -> divides x (prod_list xs) := by\n intros xs x mem\n induction xs with\n | nil => grind\n | cons y ys ih =>\n by_cases h : (x = y)\n · rw [h]\n simp\n exists (prod_list ys)\n · cases mem with\n | head => grind\n | tail =>\n rename_i a\n have ⟨h, hq⟩ := ih a\n simp at *\n rw [hq]\n exists (y * h)\n grind\ntheorem prod_list_nz : ∀ xs, (∀ x ∈ xs, x > 0) -> prod_list xs > 0 := by\n intros xs f\n induction xs with\n | nil => grind\n | cons x xs ih =>\n obtain b : prod_list xs > 0 := ih (by grind)\n simp [*]\ntheorem prod_list_lt : ∀ xs, (∀ x ∈ xs, x > 0) -> ∀ y ∈ xs, y <= prod_list xs := by\n intro xs f y yin\n induction xs with\n | nil => grind\n | cons yp ys ih =>\n cases yin with\n | head =>\n obtain a : prod_list ys > 0 := by grind [prod_list_nz]\n exact Nat.le_mul_of_pos_right y a\n | tail _ a =>\n obtain a : y <= prod_list ys := ih (by grind) a\n obtain b : yp > 0 := f yp (by grind)\n apply Nat.le_trans\n · exact a\n · exact Nat.le_mul_of_pos_left (prod_list ys) b\n@[simp, grind]\ndef prime (n : Nat) : Prop :=\n (n > 1) ∧ (∀k, divides k n -> k = 1 ∨ k = n)\ntheorem prime_two : prime 2 := by\n simp\n intros k x\n simp [divides] at x\n have ⟨q,hq⟩ := x\n (cases q <;> cases k <;> grind)\ntheorem prime_factor : ∀k, ¬(prime k) -> 1 < k -> ∃p, prime p ∧ divides p k := by\n intros k nprime kgt1\n induction k using Nat.strongRecOn with\n | ind k' ih =>\n simp at nprime\n obtain ⟨x,⟨xd,dvds⟩,xn1,xnk⟩ := nprime kgt1\n clear nprime\n by_cases h : prime x\n · exists x\n grind\n · have lt : x < k' := by\n apply Nat.lt_of_le_of_ne\n · apply divides_less <;> grind\n · assumption\n have gt : 1 < x := by\n cases x <;> grind\n obtain ⟨p,⟨prm,dvds⟩⟩ := ih x lt h gt\n exists p\n refine ⟨prm, ?_⟩\n apply divides_trans\n · assumption\n · grind\ntheorem another_prime (xs : List Nat) (xsgt : ∀x, x ∈ xs -> 1 < x)\n : ∃p, prime p ∧ p ∉ xs := by\n by_cases h : prime (Nat.succ (prod_list xs))\n · exists (Nat.succ (prod_list xs))\n refine ⟨h, ?a⟩\n by_contra\n have lt : Nat.succ (prod_list xs) ≤ prod_list xs := by\n apply prod_list_lt <;> grind\n grind\n · have ⟨pf, isprm, dvds⟩ : ∃p, prime p ∧ divides p (Nat.succ (prod_list xs)) := by\n apply prime_factor\n · exact h\n · grind [prod_list_nz]\n by_cases g : pf ∈ xs\n · have pfdvds : divides pf (prod_list xs) := by\n apply divides_prod_list <;> grind\n have divone : divides pf ((Nat.succ (prod_list xs)) - prod_list xs) := by\n apply divides_sub <;> grind\n have also : divides pf 1 := by grind\n grind [divides_not_one]\n · grind\ntheorem infinite_primes : ∀ n, ∃p, prime p ∧ p > n := by\n intros n\n by_cases h : ¬(1 < n)\n · exists 2\n grind [prime_two]\n · simp at h\n obtain ⟨p, prm, notin⟩ := another_prime (List.range' 2 n) (by grind)\n refine ⟨p, prm, ?notin⟩\n grind\n```\n```\nopen arithmeticTheory listTheory prim_recTheory listRangeTheory;\n \nDefinition divides_def:\n divides n k = ∃q. q * n = k\nEnd\nTheorem divides_not_one:\n ∀n. divides n 1 ⇒ n ≠ 1 ⇒ F\nProof\n simp[divides_def]\nQED\nTheorem divides_less:\n k ≠ 0 ⇒ divides n k ⇒ n ≤ k\nProof\n rpt strip_tac\n >> gvs[divides_def]\nQED\nTheorem divides_trans:\n divides a b ⇒ divides b c ⇒ divides a c\nProof\n rpt strip_tac\n >> gvs[divides_def]\n >> qexists ‘q * q'’\n >> gvs[MULT_ASSOC_COMM]\nQED\nTheorem divides_sub:\n divides n k ⇒ divides n j ⇒ divides n (k - j)\nProof\n rpt strip_tac\n >> metis_tac[RIGHT_SUB_DISTRIB, divides_def]\nQED\n \nDefinition prod_list_def:\n (prod_list [] = 1) ∧\n (prod_list (x :: xs) = x * prod_list xs)\nEnd\nTheorem divides_prod_list:\n x ∈ set xs ⇒ divides x (prod_list xs)\nProof\n Induct_on ‘xs’\n >- fs[]\n >- (fs[]\n >> rpt strip_tac\n >- (fs[prod_list_def, divides_def]\n >> qexists_tac ‘prod_list xs’\n >> simp[])\n >- (fs[divides_def, prod_list_def]\n >> qexists_tac ‘h * q’\n >> rev_drule EQ_SYM\n >> strip_tac\n >> fs[]))\nQED \nTheorem prod_list_nz:\n ∀xs. (∀x. x ∈ set xs ⇒ 0 < x) ⇒ 0 < prod_list xs\nProof\n rpt strip_tac\n >> Induct_on ‘xs’\n >> fs[prod_list_def]\nQED\n \nTheorem prod_list_lt:\n ∀xs. (∀x. x ∈ set xs ⇒ 0 < x) ⇒ ∀y. y ∈ set xs ⇒ y ≤ prod_list xs\nProof\n rpt strip_tac\n >> Induct_on ‘xs’\n >> gvs[]\n >> rpt strip_tac\n >> gvs[prod_list_def]\n >> metis_tac[prod_list_nz, LE_MULT_CANCEL_LBARE, LE_TRANS]\nQED\nDefinition prime_def:\n prime n = ((1 < n) ∧ (∀k. divides k n ⇒ k = 1 ∨ k = n))\nEnd\nTheorem prime_zero:\n ¬(prime 0)\nProof\n fs[prime_def]\nQED \nTheorem prime_one:\n ¬(prime 1)\nProof\n fs[prime_def]\nQED\nTheorem prime_gt_one[simp]:\n prime n ⇒ 1 < n\nProof\n fs[prime_def]\nQED\n \nTheorem prime_two:\n prime 2\nProof \n fs[prime_def]\n >> rpt strip_tac\n >> fs[divides_def]\n >> (Cases_on ‘k’ >> Cases_on ‘q’ >> fs[MULT_SUC])\nQED\nTheorem divides_gt1_gt0:\n ∀n k. divides n k ⇒ 1 < k ⇒ 0 < n\nProof\n rpt strip_tac\n >> gvs[divides_def]\n >> (Cases_on ‘q’ >> gvs[MULT_SUC])\n >> (Cases_on ‘n’ >> gvs[])\nQED\nTheorem prime_factor:\n ∀k. ¬(prime k) ⇒ 1 < k ⇒ ∃p. prime p ∧ divides p k\nProof\n completeInduct_on ‘k’\n >> rpt strip_tac\n >> qpat_x_assum ‘¬_’\n (fn h => assume_tac\n (REWRITE_RULE [prime_def] h))\n >> gvs[]\n >> Cases_on ‘prime k'’\n >- (qexists ‘k'’ >> simp[])\n >- (first_x_assum $ qspecl_then [‘k'’] mp_tac\n >> strip_tac\n >> ‘0 < k'’ by metis_tac[divides_gt1_gt0]\n >> ‘1 < k'’ by decide_tac\n >> ‘k' <= k’ by gvs[divides_less]\n >> ‘k' < k’ by decide_tac\n >> first_x_assum drule\n >> strip_tac\n >> gvs[]\n >> qexists ‘p’\n >> metis_tac[divides_trans])\nQED\nTheorem gt1_gt0_weaken:\n ∀x. 1 < x ⇒ 0 < x\nProof\n strip_tac >> decide_tac\nQED\nTheorem another_prime:\n ∀(xs : num list). (∀x. x ∈ set xs ⇒ 1 < x)\n ⇒ ∃p. prime p ∧ p ∉ set xs\nProof\n rpt strip_tac\n >> Cases_on ‘prime (SUC (prod_list xs))’\n >- (qexists ‘SUC (prod_list xs)’\n >> metis_tac[LESS_REFL, OR_LESS,\n prod_list_lt, gt1_gt0_weaken])\n >- (drule prime_factor \n >> impl_tac\n >- metis_tac[ONE, LESS_MONO, prod_list_nz,gt1_gt0_weaken]\n >- (strip_tac\n >> Cases_on ‘MEM p xs’\n >- (‘divides p (prod_list xs)’\n by metis_tac[divides_prod_list]\n >> ‘divides p ((SUC (prod_list xs)) - prod_list xs)’\n by metis_tac [divides_sub]\n >> gvs[]\n >> metis_tac[prime_one, prime_zero, divides_not_one])\n >- (qexists ‘p’ >> metis_tac[])))\nQED\n \nTheorem infinite_primes:\n ∀n. ∃p. prime p ∧ p > n\nProof\n strip_tac\n >> Cases_on ‘n < 1’\n >- (qexists ‘2’ >> simp[prime_two])\n >- (qspec_then ‘listRangeINC 2 n’ assume_tac another_prime\n >> ‘∀x. MEM x [2 .. n] ⇒ 1 < x’\n by (rpt strip_tac >> gvs[MEM_listRangeINC])\n >> first_x_assum rev_drule\n >> rpt strip_tac\n >> qexists ‘p’\n >> gvs[MEM_listRangeINC, prime_gt_one]\n >> ‘p ≠ 0’ by metis_tac[prime_zero]\n >> ‘p ≠ 1’ by metis_tac[prime_one]\n >> decide_tac)\nQED\n```\n```\nopen import Data.Nat renaming (ℕ to Nat)\nopen import Data.Nat.Properties\nopen import Relation.Binary.PropositionalEquality\nopen import Data.Product\nopen import Data.Empty\nopen import Relation.Nullary.Negation\nopen import Data.List\nopen import Data.Sum\nopen import Relation.Nullary.Decidable\nopen import Relation.Binary\nopen import Relation.Nullary.Reflects\nopen import Data.Nat.Divisibility\nopen import Data.Bool using (Bool; true; false)\nopen import Data.Fin using (zero; suc; Fin; toℕ; fromℕ; fromℕ<)\nopen import Data.Fin.Properties using (toℕ-fromℕ; toℕ-fromℕ<)\nopen import Induction.WellFounded\nopen import Data.Nat.Induction using (<-wellFounded; <-rec)\nimport Data.List.Membership.DecPropositional as DecPropMembership\nopen DecPropMembership Data.Nat._≟_\nopen import Data.List.Relation.Unary.Any using (here; there)\n-- The prime decision procedure was with assistance from https://gist.github.com/copumpkin/1286093\ndiv-goes-into : ∀ i k → k ≢ 0 → i ∣ k → i ≤ k\ndiv-goes-into i k neq (divides zero eq) = ⊥-elim (neq eq)\ndiv-goes-into zero k neq (divides (suc q) eq) = z≤n\ndiv-goes-into (suc i) k neq (divides-refl (suc q)) = s≤s (m≤m+n i (q * suc i))\ndivides-zero : ∀ i → 0 ∣ i → i ≡ 0\ndivides-zero zero (divides q eq) = refl\ndivides-zero (suc i) (divides q eq) rewrite *-comm q 0 = eq\ndivides-trans : ∀ {i j k} → i ∣ j → j ∣ k → i ∣ k\ndivides-trans {i} (divides-refl q₁) (divides q₂ eq₂) = divides (q₂ * q₁) (trans eq₂ (sym (*-assoc q₂ q₁ i)))\ndivides-sub : ∀ {i j k} → i ∣ j → i ∣ k → i ∣ (j ∸ k)\ndivides-sub {i} (divides-refl q₁) (divides-refl q₂) = divides (q₁ ∸ q₂) (sym (*-distribʳ-∸ i q₁ q₂))\ndivides-one : ∀ i → i ∣ 1 → i ≡ 1\ndivides-one zero (divides (suc q) eq) rewrite *-comm q 0 = ⊥-elim (1+n≢0 eq)\ndivides-one (suc zero) (divides (suc q) eq) = refl\ndivides-not-one : ∀ {i} → i ∣ 1 → i ≢ 1 → ⊥\ndivides-not-one {zero} (divides q eq) neq rewrite *-comm q 0 = 1+n≢0 eq\ndivides-not-one {suc zero} (divides q eq) neq = neq refl\ndivides-not-one {2+ i} (divides zero eq) neq = 1+n≢0 eq\ndivides-not-one {2+ i} (divides (suc q) eq) neq = 1+n≢0 (sym (suc-injective eq))\nlt-left-suc : ∀ i j → i ≤ j → i ≢ j → suc i ≤ j\nlt-left-suc zero zero z≤n p = ⊥-elim (p refl)\nlt-left-suc zero (suc j) z≤n p = s≤s z≤n\nlt-left-suc (suc i) zero () p\nlt-left-suc (suc i) (suc j) (s≤s x) p = s≤s (lt-left-suc i j x λ q → p (cong suc q))\nnot : {A : Set} → Dec A → Dec (¬ A)\nnot (yes p) = no (λ z → z p)\nnot (no ¬p) = yes ¬p\nDNE : {A : Set} → Dec A → ¬ ¬ A → A\nDNE (yes p) f = p\nDNE (no ¬p) f = ⊥-elim (f ¬p)\nDecide : {A : Set} (P : A → Set) → Set\nDecide P = ∀ i → Dec (P i)\nlt-lower : ∀ {i j} → suc i ≤ suc j → i ≢ j → suc i ≤ j\nlt-lower {zero} {zero} (s≤s p) q = ⊥-elim (q refl)\nlt-lower {zero} {suc j} (s≤s p) q = s≤s z≤n\nlt-lower {suc i} {suc j} (s≤s p) q = s≤s (lt-lower p λ x → q (cong suc x))\nlt-decide : ∀ i → (P : Nat → Set) (p? : ∀ n → n < i → Dec (P n)) → (∀ n → n < i → P n) ⊎ (Σ _ λ j → j < i × ¬ (P j))\nlt-decide zero P p? = inj₁ λ _ ()\nlt-decide (suc i) P p? with lt-decide i P h\n where\n h : (n : Nat) → n < i → Dec (P n)\n h n lt = p? n (s≤s (<⇒≤ lt))\n... | inj₂ (a , b , c) = inj₂ (a , s≤s (≤-trans (n≤1+n a) b) , c)\n... | inj₁ x with p? i ≤-refl\n... | no ¬a = inj₂ (i , ≤-refl , ¬a)\n... | yes a = inj₁ h\n where\n h : (n : Nat) → suc n ≤ suc i → P n\n h n lt with n ≟ i\n ... | yes refl = a\n ... | no ¬a = x n (lt-lower lt ¬a)\n¬lt-decide : ∀ i → (P : Nat → Set) (p? : ∀ n → n < i → Dec (P n)) → (∀ n → n < i → ¬ P n) ⊎ (Σ _ λ j → j < i × (P j))\n¬lt-decide i P p? with lt-decide i (λ x → ¬ (P x)) (λ n x → not (p? n x))\n... | inj₁ x = inj₁ x\n... | inj₂ (a , b , c) = inj₂ (a , b , DNE (p? a b) c)\nrecord Prime (n : Nat) : Set where\n constructor isprime\n field\n gt1 : n > 1\n div : ∀ k → k ∣ n → k ≡ 1 ⊎ k ≡ n\nopen Prime\nzero-prime : ¬ (Prime 0)\nzero-prime ()\nprime-not-zero : ∀ p → Prime p → p ≢ 0\nprime-not-zero p x refl = zero-prime x\none-prime : ¬ (Prime 1)\none-prime (isprime (s≤s ()) div)\ntwo-prime : Prime 2\ntwo-prime .gt1 = s≤s (s≤s z≤n)\ntwo-prime .div zero (divides (suc q) eq) rewrite *-comm q 0 = ⊥-elim (1+n≢0 eq)\ntwo-prime .div (suc zero) (divides (suc q) eq) = inj₁ refl\ntwo-prime .div (2+ zero) (divides (suc q) eq) = inj₂ refl\nrecord Composite (n : Nat) : Set where\n constructor composite\n field\n p : Nat\n Pp : Prime p\n p 1 → Prime p ⊎ Composite p\nprime-or-composite (suc zero) (s≤s ())\nprime-or-composite (2+ p) lt = <-rec _ h p\n where\n h : (x : Nat) →\n ({y : Nat} → suc y ≤ x → Prime (2+ y) ⊎ Composite (2+ y)) →\n Prime (2+ x) ⊎ Composite (2+ x)\n h x f with ¬lt-decide x (λ k → (2+ k) ∣ (2+ x)) (λ n nlt → 2+ n ∣? 2+ x)\n ... | inj₂ (ev₁ , ev₂ , ev₃) with f ev₂\n h x f | inj₂ (ev₁ , ev₂ , ev₃) | inj₁ prm = inj₂ (composite (2+ ev₁) prm (s≤s (s≤s ev₂)) ev₃)\n h x f | inj₂ (ev₁ , ev₂ , ev₃) | inj₂ (composite p Pp (s≤s p 0) → prod-list xs > 0\nprod-list-nz [] f = s≤s z≤n\nprod-list-nz (x ∷ []) f rewrite *-comm x 1 rewrite +-comm x 0 = f x (here refl)\nprod-list-nz (x ∷ x₁ ∷ xs) f = h {x} (f x (here refl)) (prod-list-nz (x₁ ∷ xs) (λ x₂ z → f x₂ (there z)))\n where\n h : ∀ {i j} → 1 ≤ i → 1 ≤ j → 1 ≤ i * j\n h {suc i} {suc j} (s≤s a) (s≤s b) = s≤s z≤n\nprod-list-NZ : ∀ xs → (∀ x → x ∈ xs → x > 0) → NonZero (prod-list xs)\nprod-list-NZ xs f = >-nonZero (prod-list-nz xs f)\nprod-list-lt : ∀ xs → (∀ x → x ∈ xs → x > 0) → ∀ y → y ∈ xs → y ≤ prod-list xs\nprod-list-lt [] f y ()\nprod-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) ⦄\nprod-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))\n where\n lt+ : ∀ {i j k} → i ≤ j → i ≤ j + k\n lt+ z≤n = z≤n\n lt+ (s≤s x) = s≤s (lt+ x)\n also : ∀ {i j k} → i ≤ k → 1 ≤ j → i ≤ j * k\n also a (s≤s z≤n) = lt+ a\nprod-list-divides : ∀ xs x → x ∈ xs → x ∣ prod-list xs\nprod-list-divides [] x ()\nprod-list-divides (y ∷ xs) x (here refl) = divides (prod-list xs) (*-comm y (prod-list xs))\nprod-list-divides (y ∷ xs) x (there p) with prod-list-divides xs x p\n... | divides q eq rewrite eq = divides (y * q) (sym (*-assoc y q x))\nprime-not-in : ∀ xs → (∀ x → x ∈ xs → x > 0) → Σ _ λ k → k ∉ xs × Prime k\nprime-not-in xs gt with 2 ≤? prod-list xs\n... | no ¬a = 2 , lemma , two-prime\n where\n lemma : 2 ∈ xs → ⊥\n lemma pf with prod-list-lt xs gt 2 pf\n ... | also = ¬a also\n... | yes a with prime-or-composite (suc (prod-list xs)) (s≤s (≤-trans (s≤s z≤n) a))\n... | inj₁ x = suc (prod-list xs) , lemma , x\n where\n lemma : (suc (prod-list xs)) ∈ xs → ⊥\n lemma pf with prod-list-lt xs gt (suc (prod-list xs)) pf\n ... | also = 1+n≰n also\n... | inj₂ (composite p Pp p 0\nlist-up-to-nz zero x (here refl) = s≤s z≤n\nlist-up-to-nz (suc k) x (here refl) = s≤s z≤n\nlist-up-to-nz (suc k) x (there p) = list-up-to-nz k x p\nlist-up-to-contains : ∀ i j → j ≤ i → j ≢ 0 → j ∈ list-up-to i\nlist-up-to-contains zero zero z≤n b = ⊥-elim (b refl)\nlist-up-to-contains zero (suc j) () b\nlist-up-to-contains (suc i) zero z≤n b = ⊥-elim (b refl)\nlist-up-to-contains (suc i) (suc j) (s≤s a) b with suc i ≟ suc j\n... | no ¬c = there (list-up-to-contains i (suc j) (lt-left-suc j i a λ x → ¬c (cong suc (sym x))) b)\n... | yes refl = here refl\ninfinite-primes : ∀ i → Σ _ λ p → p > i × Prime p\ninfinite-primes zero = 2 , s≤s z≤n , two-prime\ninfinite-primes (suc i) with prime-not-in (list-up-to (2+ i)) (list-up-to-nz (2+ i))\n... | p , notin , Pp = p , DNE (2+ i ≤? p) lemma , Pp\n where\n notzero : p ≢ 0\n notzero = prime-not-zero p Pp\n implies : ∀ {a b} → (suc a ≤ b → ⊥) → (a ≡ b) ⊎ (a > b)\n implies {a} {b} x with compare a b\n ... | less .a k = ⊥-elim (x (s≤s (m≤m+n a k)))\n ... | equal .a = inj₁ refl\n ... | greater .b k = inj₂ (s≤s (m≤m+n b k))\n lemma : ((2+ i ≤ p) → ⊥) → ⊥\n lemma x with implies x\n ... | inj₁ refl = notin (there (here refl))\n ... | 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))\n```\n","body_html":"

2026-10-10

\n

In which I compare Lean, Isabelle/HOL, Agda, and HOL4 with only mild regard for "fairness".

\n

All four of the above are theorem proving applications; that is, their purpose is to computer-formalize mathematics.\nBroadly speaking, both Lean and Agda are dependent-types based systems, utilizing the Curry-Howard correspondence to prove theorems via a complex type system, whereas Isabelle/HOL and HOL4 are LCF-style systems, with a small "proof kernel" containing base rules (e.g. forall x, x = x) that all proofs must be constructed via.\nBoth foundations have advantages and disadvantages, and some will be discussed.

\n

I have formalized in all four a proof of the infinitude of primes; that is, the statement "For any number n, there is a prime larger than n". The exact proof formalized is the "usual" construction by Euclid, which you can find on Wikipedia if you want; see here.

\n

All of the proofs structurally look similar (mostly, we'll get to that), and hence it was the user experience that made the difference. For transparency, before this experiment, I was most familiar with Isabelle/HOL and Agda, and to some extent learnt HOL4 and Lean as part of this review.

\n

What follows is a bunch of opinions and somewhat arbitrary categories. Don't expect an unbiased review, please. If you only want proof comparisons, skip to Proof Comparisons, and if you only want more opinions, read the below and then skip to Arbitrary Rankings. The opinions go first.

\n

I do not claim any of the following proofs are perfect! They're probably quite mediocre, really.

\n

There are a few categories by which we can group these theorem provers. We have the above mentioned:

\n
  • LCF-style: Isabelle/HOL, HOL4
  • Dependent-style: Lean, Agda
\n

But there's also:

\n
  • High-interactivity: Isabelle/HOL, Lean
  • Low-interactivity: HOL4, Agda
\n

Reasoning: Both Isabelle/HOL and Lean provide "live updates" as you type, and their structured proofs can be "down-arrow"'d through, to see intermediate steps. In contrast, both completed HOL4 and Agda proofs exist as fully-put-together terms that must be manually taken apart if you wish to inspect their internals. Both HOL4 and Agda can show you your current state and related information at any time, of course.

\n
  • High-automation: Isabelle/HOL, HOL4
  • Medium-automation: Lean
  • Low-automation: Agda
\n

Isabelle/HOL has sledgehammer, which calls out to a number of external proof generation methods (SAT/SMT solvers, various FOL solvers, etc). For any goal that looks doable-but-annoying, there's a solid chance sledgehammer can solve it - this is nice because it saves you work, but the proofs it generates are also indecipherable, which is perhaps less than ideal. There also exists an equivalent for HOL4 called HolyHammer, but I didn't realize it existed until after I was writing this. Oh well. Isabelle/HOL and HOL4 both have very good support for many automated simplification and proof methods, which come in quite handy when trying to work with complex assumptions, for example. It may not be obvious how to proceed without simplification kicking in to chunk everything down.

\n

Lean has decent automation, but not to the same level as Isabelle/HOL or HOL4. Its simp is not nearly as productive, and while grind is a very neat approach that can sometimes rival sledgehammer, a lot of the time it's quite useless for reasons beyond me. Both sledgehammer and grind are all-or-nothing; if they don't solve the goal, they make no progress. This is in contrast to simp (in all three), or more specialized tools like auto (Isabelle/HOL) or gvs (HOL4), which can make some progress and then leave the context in (ideally) a better place. The fact Lean doesn't have nearly as good partial-automation is a bit of a shame, because in my experience that's what actually matters more. Notably, both Lean and Isabelle/HOL have a try (In Isabelle/HOL, try/try0 for with/without sledgehammer; in Lean, try?/exact?/rw?) that "have a go" at your goal with various automated methods and direct solve attempts. HOL4 doesn't have an equivalent, as far as I can tell, which is unfortunate, as it's quite handy.

\n

Agda has essentially no automation. The only simplification you get is what can be computed based on inputs to functions. This, to be a bit frank, sort of sucks. It's quite hard to get things done because there's so much manual fiddling that must be taken into account. I am personally not a fan.

\n

Isabelle/HOL and HOL4 are both extremely classical in their foundations, which means that they accept the Law of Excluded Middle (∀ P. ¬P ∨ P), and both also axiomatize Hilbert's epsilon, which leads also to the Axiom of Choice. This seems to have a very positive effect on automated solvers, which quite often rely on laws such as double-negation elimination (¬¬P --> P), which is equivalent to the LEM. Lean is theoretically constructive (and hence does not have the LEM by default), but some of the "good" proof automation requires the LEM, and it seems the norm to use Lean classically, so that's what I did. grind for example just assumes you're using it. This does have the disadvantage that Lean isn't as good at dealing with e.g. existentials, for example.

\n

Agda is constructive by default, and it seems the norm in the Agda world to keep your proofs that way, so I did. The big advantage of this is that after proving there are infinitely many primes, I can actually generate them! I can give my proof a number, and it'll spit out a prime bigger than that number. The disadvantage is that it is horribly slow to do so:

\n
  • 0: 2 (instant)
  • 1: 3 (instant)
  • 2: 7 (instant)
  • 3: 5 (instant)
  • 4: 11 (quarter second)
  • 5: 7 (quarter second)
  • 6: 71 (3s)
  • 7: 61 (10s)
  • 8: 19 (40s)
\n

This may make sense if you looked at the proof structure above; we consider (n + 1)! + 1, so inside that proof, it's checking primality at numbers around ~360,000; that's going to be a bit slow. This construction, it should be noted, isn't meant to be fast, but it's also the most natural one. Is it worth giving up the LEM and good proof automation? You decide.

\n

I'm more a fan of LCF because it seems more amenable to automation, and I don't see the point of carrying around proof terms (classical logic is too useful!). If you vehemently disagree, email me at contact AT blueberrywren.dev, and if I like your argument enough I'll post it here.

\n

Both Lean and Isabelle/HOL are interacted with interactively. Lean has modes for other editors, but high recommends the use of VSCode, and Isabelle/HOL has its own editor (jEdit) that it also practically forces the use of. This is fine; I understand why they do this, as interactive development is reasonably hard to make generic. Both of them make it work.

\n

HOL4 is interacted with via either an Emacs mode or a Vim mode, and keybinds that allow one to copy text in/out of a running HOL4 REPL. This sounds weird because it is, but it works surprisingly well. I was already an Emacs user, so nothing really changed for me.

\n

Agda is also interacted with via an Emacs mode, but everything happens in your file; you can use keybinds to refresh the state, add proof goals, etc. It also works fine.

\n

As mentioned above, the advantage of the Lean/Isabelle/HOL approach is that one can see proofs in-progress, which you can't with Agda.

\n

Both Isabelle/HOL and HOL4 have extremely good mechanisms for searching for theorems; an editor panel + find_theorems for the former, and DB.find/DB.match for the latter. These allow for the searching of theorems by both name and by patterns, so I could for example search for lemmas of form _ < SUC _. This is so handy! Very often you know the shape of something you want, but maybe not the lemma itself.

\n

Lean has leansearch and loogle, which are interesting, but they:

\n
  1. Aren't built in.
  2. Aren't as good.
\n

Which kind of sucks. exact? and rw? exist as "here's stuff you might be able to do", but they're nowhere near as flexible.

\n

Agda, as expected perhaps, does not have an equivalent. One must become a master of zen looking through the right parts of the Agda standard library.

\n

Note: This isn't really meant to be a tutorial for any of these, though I will do a little explaining at the start. It's mostly for the reader to compare them, and see what ~equivalent statement proofs look like in different languages.

\n

Let's get into the proofs! We'll go segment by segment, exploring sections of the proof and explaining as we go. Before that, some vaguely interesting stats:

\n
  • Isabelle/HOL: 117 LOC, with 19 proofs.
  • Lean: 155 LOC, with 12 proofs.
  • HOL4: 190 LOC, with 16 proofs.
  • Agda: 264 LOC, with 45 proofs (29, not counting where blocks)
\n

These are nowhere near apples-to-apples, but they're still fun.

\n

We start with defining divisibility. In Agda we cheat and use the standard library version, so we can get proofs around computing divisors, which I didn't feel like redoing.

\n

Isabelle/HOL:

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

Lean:

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

HOL4:

\n
Definition divides_def:\n  divides n k = ∃q. q * n = k\nEnd
\n

Agda (looks like, in the standard library):

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

So, basically the same. Then there's a few lemmas around divisibility proved (divides k 0, divides k k, etc). One we'll show off is divides n k ==> divides n j ==> divides n (k - j), as it's mildly interesting in some of the theorem provers. In all of the following, the mult/sub lemma essentially states a * (b - c) = a * b - a * c.

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

The proof search procedure metis does most of the work.

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

We do some unpacking, then identify q1 - q2 as the other term (such that n * (q1 - q2) = k - j). Then grind with the appropriate lemma gets us there.

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

Like Isabelle/HOL, when supplied with the appropriate lemmas, metis_tac takes it out.

\n

Agda:

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

Very similar. divides-refl is an abbreviation for divides _ refl, and like in Lean, we must manually point out q₁ ∸ q₂.

\n

It was interesting to me that the Lean proof was, to some extent, such a pain. I had to put more effort into that one than any of the others, despite Lean having reasonably decent automation! Finding the appropriate lemmas was mildly more painful, and this was while I was still puzzling over syntax, to be fair.

\n

We next need to define the product of a list of numbers, which looks like the following:

\n
fun prod_list :: "nat list ⇒ nat" where\n"prod_list [] = 1" | \n"prod_list (x # xs) = x * prod_list xs"
\n
@[simp, grind]\ndef prod_list (xs : List Nat) : Nat :=\n  match xs with\n  | [] => 1\n  | x :: xs => x * prod_list xs
\n

The simp and grind markers were meant to help the automated proof methods out, and they did!

\n
Definition prod_list_def:\n  (prod_list [] = 1) ∧\n  (prod_list (x :: xs) = x * prod_list xs)\nEnd
\n
prod-list : List Nat → Nat\nprod-list [] = 1\nprod-list (x ∷ xs) = x * prod-list xs
\n

Defining things in HOL4 is a little interesting, because you're just defining the body as a proof! That definition spits out a theorem prod_list_def that is literally

\n

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

\n

Here in the Agda proof we also do a bunch of work to set up what will become a decision procedure for primality. This is because later we wish to ask "Is this prime?", and without the LEM to say "It must either be prime or not prime", we need to write an algorithm to decide this for us.

\n

Back on track, we need to show a few lemmas around with prod list function. One of the interesting ones is as follows, where we prove that a number in said list will divide the product of the list.

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

Very implicit; it's hard to tell what's going on, but the basic structure is there. Induct on the list, do some casing, apply a lemma about divides _ (_ * _).

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

Reasonably large. We have to destructure the membership quite manually, which gets a little troublesome. It's a fairly straightforward proof, though.

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

Also not crazy, although it's hard to see the exact structure without comments (which I didn't write :P). This is a good time to point out HOL4 proofs are literally just SML terms! There's nothing more to it! The combinators >> and >- (for apply latter to all subgoals of former, and to one subgoal of former resp.) are just infix functions composing other functions! It's all just SML! You interact with HOL4 through a REPL, so you construct stuff dynamically, but then you have to puzzle piece your function together afterwards. Once you know that, it's more obvious what's going on; we induct, handle the first case, then simplification on MEM x (h ∷ xs) give us two goals (x = h and x ≠ h, MEM x xs resp.)

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

Very explicit, but also quite concise. Matching on the list membership is quite intuitive, because the Agda mode in Emacs includes a command C-c C-c to automatically case split on basically everything.

\n

While it's much more implicit in Isabelle/HOL and HOL4 (a common theme), all four of these proofs take the form of asking whether the value we care about is at the head of the list, or somewhere later on, and that decides what we fill in divisibility with.

\n

Then, Primality!

\n
definition prime :: "nat ⇒ bool" where\n  "prime p = ((p > 1) ∧ (∀x. divides x p ⟶ x = p ∨ x = 1))"
\n
@[simp, grind]\ndef prime (n : Nat) : Prop :=\n  (n > 1) ∧ (∀k, divides k n -> k = 1 ∨ k = n)
\n
Definition prime_def:\n  prime n = ((1 < n) ∧ (∀k. divides k n ⇒ k = 1 ∨ k = n))\nEnd
\n
record Prime (n : Nat) : Set where\n  constructor isprime\n  field\n    gt1 : n > 1\n    div : ∀ k → k ∣ n → k ≡ 1 ⊎ k ≡ n
\n

In Agda we also define what it means to be composite as a "positive" definition, instead of just "not prime"; this makes working with it quite a bit easier.

\n

The next "interesting" proof is proving that every not-prime number greater than one has a prime factor. In Agda this is part of the definition of being composite, so we don't bother including it. We're going to move slightly faster from now on, so I won't explain each snippet. Just compare yourselves.

\n
lemma prime_factor: "¬(prime k) ⟹ k > 1 ⟹ ∃p. prime p ∧ divides p k"\n  apply (induct k rule: measure_induct[of "id"]; simp)\n  apply (rotate_tac 1)\n  apply (subst (asm) prime_def)\n  apply clarsimp\n  apply (case_tac "prime xa")\n   apply blast\n  apply (erule_tac x=xa in allE)\n  (* found with sledgehammer *)\n  by (metis divides_gt divides_trans less_Suc0 not_less_iff_gr_or_eq zero_not_divides)
\n
theorem prime_factor : ∀k, ¬(prime k) -> 1 < k -> ∃p, prime p ∧ divides p k := by\n  intros k nprime kgt1\n  induction k using Nat.strongRecOn with\n  | ind k' ih =>\n    simp at nprime\n    obtain ⟨x,⟨xd,dvds⟩,xn1,xnk⟩ := nprime kgt1\n    clear nprime\n    by_cases h : prime x\n    · exists x\n      grind\n    · have lt : x < k' := by\n        apply Nat.lt_of_le_of_ne\n        · apply divides_less <;> grind\n        · assumption\n      have gt : 1 < x := by\n        cases x <;> grind\n      obtain ⟨p,⟨prm,dvds⟩⟩ := ih x lt h gt\n      exists p\n      refine ⟨prm, ?_⟩\n      apply divides_trans\n      · assumption\n      · grind
\n
Theorem prime_factor:\n  ∀k. ¬(prime k) ⇒ 1 < k ⇒ ∃p. prime p ∧ divides p k\nProof\n  completeInduct_on ‘k’\n  >> rpt strip_tac\n  >> qpat_x_assum ‘¬_’\n                  (fn h => assume_tac\n                          (REWRITE_RULE [prime_def] h))\n  >> gvs[]\n  >> Cases_on ‘prime k'’\n  >- (qexists ‘k'’ >> simp[])\n  >- (first_x_assum $ qspecl_then [‘k'’] mp_tac\n      >> strip_tac\n      >> ‘0 < k'’ by metis_tac[divides_gt1_gt0]\n      >> ‘1 < k'’ by decide_tac\n      >> ‘k' <= k’ by gvs[divides_less]\n      >> ‘k' < k’ by decide_tac\n      >> first_x_assum drule\n      >> strip_tac\n      >> gvs[]\n      >> qexists ‘p’\n      >> metis_tac[divides_trans])\nQED
\n

The steps of 0 < k' ~> 1 < k' and k' <= k ~> k' < k in the HOL4 one annoyed me a lot, but I couldn't figure out how to golf them down. Similarly, this line:

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

of the Lean proof causes me pain.

\n

We're almost there now! Two more steps to go: Prove there's always a prime outside a given set (list) of numbers, and use that to show the final statement. First, the former:

\n
lemma another_prime: "(∀x∈set xs. x > 1) ⟹ ∃p. prime p ∧ p ∉ set xs"\n  apply (case_tac "prime (Suc (prod_list xs))")\n  using prod_list_lt apply fastforce\n  apply (frule prime_factor)\n   apply clarsimp\n  apply (case_tac "length xs = 0"; clarsimp)\n   apply (rule prod_list_gt_zero; clarsimp)\n  using prime_gt_one apply fastforce\n  using divides_prod_list divides_diff prime_gt_one one_divides\n  by (metis One_nat_def Suc_diff_Suc cancel_comm_monoid_add_class.diff_cancel lessI nat_less_le)
\n
theorem another_prime (xs : List Nat) (xsgt : ∀x, x ∈ xs -> 1 < x)\n  : ∃p, prime p ∧ p ∉ xs := by\n  by_cases h : prime (Nat.succ (prod_list xs))\n  · exists (Nat.succ (prod_list xs))\n    refine ⟨h, ?a⟩\n    by_contra\n    have lt : Nat.succ (prod_list xs) ≤ prod_list xs := by\n      apply prod_list_lt <;> grind\n    grind\n  · have ⟨pf, isprm, dvds⟩ : ∃p, prime p ∧ divides p (Nat.succ (prod_list xs)) := by\n      apply prime_factor\n      · exact h\n      · grind [prod_list_nz]\n    by_cases g : pf ∈ xs\n    · have pfdvds : divides pf (prod_list xs) := by\n        apply divides_prod_list <;> grind\n      have divone : divides pf ((Nat.succ (prod_list xs)) - prod_list xs) := by\n        apply divides_sub <;> grind\n      have also : divides pf 1 := by grind\n      grind [divides_not_one]\n    · grind
\n
Theorem another_prime:\n  ∀(xs : num list). (∀x. x ∈ set xs ⇒ 1 < x)\n                    ⇒ ∃p. prime p ∧ p ∉ set xs\nProof\n  rpt strip_tac\n  >> Cases_on ‘prime (SUC (prod_list xs))’\n  >- (qexists ‘SUC (prod_list xs)’\n      >> metis_tac[LESS_REFL, OR_LESS, prod_list_lt, gt1_gt0_weaken])\n  >- (drule prime_factor\n      >> impl_tac\n      >- metis_tac[ONE, LESS_MONO, prod_list_nz,gt1_gt0_weaken]\n      >- (strip_tac\n          >> Cases_on ‘MEM p xs’\n          >- (‘divides p (prod_list xs)’\n                by metis_tac[divides_prod_list]\n              >> ‘divides p ((SUC (prod_list xs)) - prod_list xs)’\n                by metis_tac [divides_sub]\n              >> gvs[]\n              >> metis_tac[prime_one, prime_zero, divides_not_one])\n          >- (qexists ‘p’ >> metis_tac[])))\nQED
\n
prime-not-in : ∀ xs → (∀ x → x ∈ xs → x > 0) → Σ _ λ k → k ∉ xs × Prime k\nprime-not-in xs gt with 2 ≤? prod-list xs\n... | no ¬a = 2 , lemma , two-prime\n  where\n    lemma : 2 ∈ xs → ⊥\n    lemma pf with prod-list-lt xs gt 2 pf\n    ... | also = ¬a also\n... | yes a with prime-or-composite (suc (prod-list xs)) (s≤s (≤-trans (s≤s z≤n) a))\n... | inj₁ x = suc (prod-list xs) , lemma , x\n  where\n    lemma : (suc (prod-list xs)) ∈ xs → ⊥\n    lemma pf with prod-list-lt xs gt (suc (prod-list xs)) pf\n    ... | also = 1+n≰n also\n... | inj₂ (composite p Pp p<n p∣) with p ∈? xs\n... | no ¬b = p , ¬b , Pp\n... | yes b with prod-list-divides xs p b\n... | divs with divides-sub p∣ divs\n... | sothen = ⊥-elim (lemma {p} {prod-list xs} sothen λ{ refl → one-prime Pp })\n  where\n    suc-sub : ∀ i → suc i ∸ i ≡ 1\n    suc-sub zero = refl\n    suc-sub (suc i) = suc-sub i\n    lemma : ∀ {i j} → i ∣ (suc j ∸ j) → i ≢ 1 → ⊥\n    lemma {_} {j} div neq rewrite suc-sub j = divides-not-one div neq
\n

The Agda proof differs slightly to accommodate the lack of ranges later.

\n

The Isabelle/HOL proof clearly wins in terms of length here, but it's also really unclear what's going on. Everyone else gets progressively more verbose, and the HOL4 proof in particular here is a bit nastily nested. metis_tac[] (a first-order solver) does a lot of heavy lifting, as does grind. If you're wondering why both Isabelle/HOL and HOL4 have something named metis/metis_tac, it's because it was ported to Isabelle/HOL from HOL4.

\n

We arrive at our final statement! Agda requires some more fiddling as it doesn't have ranges built in like the other two do, but we use our lemma above to construct the list [2..n], and then show there's a prime outside that (and that it hence must be above n).

\n
lemma infinite_primes: "∃p. prime p ∧ p > n"\n  apply (insert another_prime[where xs="[2 ..< Suc n]"])\n  apply (case_tac "n ≤ 1"; clarsimp)\n   apply (rule_tac x=2 in exI)\n   apply simp\n  apply (rule_tac x=p in exI)\n  apply simp\n  using prime_gt_one by force
\n
theorem infinite_primes : ∀ n, ∃p, prime p ∧ p > n := by\n  intros n\n  by_cases h : ¬(1 < n)\n  · exists 2\n    grind [prime_two]\n  · simp at h\n    obtain ⟨p, prm, notin⟩ := another_prime (List.range' 2 n) (by grind)\n    refine ⟨p, prm, ?notin⟩\n    grind
\n
Theorem infinite_primes:\n    ∀n. ∃p. prime p ∧ p > n\nProof\n  strip_tac\n  >> Cases_on ‘n < 1’\n  >- (qexists ‘2’ >> simp[prime_two])\n  >- (qspec_then ‘listRangeINC 2 n’ assume_tac another_prime\n      >> ‘∀x. MEM x [2 .. n] ⇒ 1 < x’\n        by (rpt strip_tac >> gvs[MEM_listRangeINC])\n      >> first_x_assum rev_drule\n      >> rpt strip_tac\n      >> qexists ‘p’\n      >> gvs[MEM_listRangeINC, prime_gt_one]\n      >> ‘p ≠ 0’ by metis_tac[prime_zero]\n      >> ‘p ≠ 1’ by metis_tac[prime_one]\n      >> decide_tac)\nQED
\n

It annoys me I couldn't get this smaller, but oh well.

\n
infinite-primes : ∀ i → Σ _ λ p → p > i × Prime p\ninfinite-primes zero = 2 , s≤s z≤n , two-prime\ninfinite-primes (suc i) with prime-not-in (list-up-to (2+ i)) (list-up-to-nz (2+ i))\n... | p , notin , Pp = p , DNE (2+ i ≤? p) lemma , Pp\n  where\n    notzero : p ≢ 0\n    notzero = prime-not-zero p Pp\n    implies : ∀ {a b} → (suc a ≤ b → ⊥) → (a ≡ b) ⊎ (a > b)\n    implies {a} {b} x with compare a b\n    ... | less .a k = ⊥-elim (x (s≤s (m≤m+n a k)))\n    ... | equal .a = inj₁ refl\n    ... | greater .b k = inj₂ (s≤s (m≤m+n b k))\n    lemma : ((2+ i ≤ p) → ⊥) → ⊥\n    lemma x with implies x\n    ... | inj₁ refl = notin (there (here refl))\n    ... | 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))
\n

We've done it! Euclid would be proud. (probably)

\n

It's now time for more opinions!

\n

I have five criteria I'll be ranking on:

\n
  • Ease of proof discovery (how easy is it to figure out what I want to do)
  • Ease of proof manipulation (how easy is it to do what I want)
  • Enjoyment (how much fun did I have)
  • Annoyance factor (how often was I going "ugh!")
  • Puzzled factor (how often did I go "why can't you solve this??")
\n
  1. Isabelle/HOL
  2. HOL4
  3. Lean
  4. Agda
\n

Not much to comment on here, really. sledgehammer is a great boon, and both Isabelle/HOL and HOL4's theorem discovery tools are great. Lean was reasonably close behind, with try? often giving good related lemmas as a solve, and Agda was clearly last. Paging through .agda files online to find lemmas is annoying.

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

Love it or hate it, Agda being entirely raw proof terms means things are essentially exactly what you tell them to be. There's never a moment where you're going "Damn, why won't the simplifier just expand this but not that!". Lean is pretty good here, as it's quite conservative around what it chooses to manipulate and everything is explicitly named. HOL4 has a pretty reasonable learning curve as one learns to use things like qpat_assum that can target based on patterns (e.g. ¬_), but once you figure it out it's not bad. Isabelle/HOL really isn't stunning here; it's often hard to get it to do exactly what you want.

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

I had a great time learning both HOL4 and Lean, but HOL4 edges out because it's such a unique interaction mode and it's still very powerful. Lean was fun, although annoying at some times, and Isabelle/HOL wasn't particularly interesting, but some of that is because i'm familiar with it. Agda sort of sucked at times; writing a whole primality decision procedure and fiddling with type nonsense got quite annoying after a while.

\n
  1. Agda
  2. HOL4 / Lean (tied second)
  3. Isabelle/HOL
\n

Agda "wins" for the same reasons as above. Having to do really manual proof search and fiddling constantly wasn't super pleasant. HOL4 and Lean both had their own annoyances and I think it's unfair to rank one over the other; the learning curve on assumption manipulation / sim was quite significant in HOL4 and Lean's automated tools were finicky enough it quite sucked at times. Isabelle/HOL i'm just used to, so there's some bias there.

\n

Same reasons as above; there were a lot of times where HOL4 just had me going "huh????" because some theorem-tactic wasn't doing what I expected it to, or was transforming the goal in an unpredictable way. Lean had similar, where it would just randomly decide "erm actually i'm not going to solve this really simple goal for you with grind do it yourself please" in ways that left me baffled. Seriously, sometimes grind is smarter than sledgehammer and sometimes it's stupider than simp. Weird. Isabelle/HOL had some of the same but was generally fine, and Agda was utterly predictable.

\n

HOL4! I had a great time learning it, it's a seriously interesting system. I didn't not enjoy Lean, but there's enough odd stuff going on to make me slightly wary of it, I suppose. Isabelle/HOL remains the one I'm best at (I am somewhat paid to write it, so that helps), and Agda is Agda.

\n

What should you try? Well, all of them, but I would at least try out something new. If you've only used dependent theorem provers before, try Isabelle/HOL or HOL4, and vice versa. If you've only used theorem provers that work fully interactively like Lean, try HOL4 or Agda! New experiences are the joys of life.

\n

Enjoy.

\n
theory primes\n  imports Main\nbegin\ndefinition divides :: "nat ⇒ nat ⇒ bool" where\n  "divides n k = (∃j. j * n = k)"\nlemma zero_not_divides: "k ≠ 0 ⟹ ¬(divides 0 k)"\n  by (simp add: divides_def)\nlemma one_divides: "divides k 1 ⟹ k = 1"\n  by (simp add: divides_def)\nlemma divide_mult_l: "divides x k ⟹ divides x (n * k)"\n  using divides_def by auto\nlemma divides_diff: "divides x k ⟹ divides x n ⟹ divides x (k - n)"\n  using divides_def by (metis diff_mult_distrib)\nlemma divides_gt: "k ≠ 0 ⟹ n > k ⟹ ¬(divides n k)"\n  by (clarsimp simp add: divides_def)\nlemma divides_less: "k ≠ 0 ⟹ divides n k ⟹ n ≤ k"\n  by (clarsimp simp add: divides_def)\nlemma divides_trans: "divides n k ⟹ divides k j ⟹ divides n j"\n  using divides_def by force\nfun prod_list :: "nat list ⇒ nat" where\n"prod_list [] = 1" | \n"prod_list (x # xs) = x * prod_list xs"\nlemma prod_list_gt_zero: "(∀x∈set xs. x ≠ 0) ⟹ length xs > 0 ⟹ prod_list xs > 0"\n  apply (induct xs)\n   apply simp\n  by (case_tac xs; clarsimp)\nlemma prod_list_lt: "(∀x∈set xs. x > 0) ⟹ ∀x∈set xs. x ≤ prod_list xs"\n  apply (induct xs)\n   apply simp\n  apply auto\n  using prod_list_gt_zero apply fastforce\n  apply (erule_tac x=x in ballE)\n  using mult_eq_if apply auto[1]\n  by blast\nlemma divides_prod_list: "x ∈ set xs ⟹ divides x (prod_list xs)"\n  apply (induct xs)\n   apply simp\n  apply auto\n   apply (case_tac xs; simp add: divides_def)\n  apply (case_tac xs; simp)\n  apply (rule divide_mult_l)\n  by assumption\ndefinition prime :: "nat ⇒ bool" where\n  "prime p = ((p > 1) ∧ (∀x. divides x p ⟶ x = p ∨ x = 1))"\nlemma prime_zero[simp]: "¬(prime 0)"\n  by (clarsimp simp add: prime_def)\nlemma prime_one[simp]: "¬(prime 1)"\n  by (clarsimp simp add: prime_def)\nlemma prime_two[simp]: "prime 2"\n  apply (clarsimp simp add: prime_def)\n  apply (case_tac x; clarsimp simp add: divides_def)\n  apply (case_tac nat; clarsimp simp add: divides_def)\n  by (case_tac j; simp)\nlemma prime_gt_one: "prime p ⟹ p > 1"\n  using prime_def by simp\nlemma notprime_split: "¬(prime k) ⟹ k > 1 ⟹ ∃n j. n < k ∧ j < k ∧ k = n * j"\n  apply (clarsimp simp add: prime_def divides_def)\n  apply (rule_tac x=x in exI)\n  apply (rule conjI)\n   apply (metis less_Suc0 linorder_neqE_nat mult_is_0 n_less_m_mult_n)\n  apply (rule_tac x=j in exI)\n  apply auto\n  by (metis bot_nat_0.not_eq_extremum mult_zero_left not_less_zero)\nlemma prime_not_divides_one: "prime p ⟹ ¬(divides p 1)"\n  by (clarsimp simp add: prime_def divides_def)\nlemma prime_factor: "¬(prime k) ⟹ k > 1 ⟹ ∃p. prime p ∧ divides p k"\n  apply (induct k rule: measure_induct[of "id"]; simp)\n  apply (rotate_tac 1)\n  apply (subst (asm) prime_def)\n  apply clarsimp\n  apply (case_tac "prime xa")\n   apply blast\n  apply (erule_tac x=xa in allE)\n  by (metis divides_gt divides_trans less_Suc0 not_less_iff_gr_or_eq zero_not_divides)\nlemma another_prime: "(∀x∈set xs. x > 1) ⟹ ∃p. prime p ∧ p ∉ set xs"\n  apply (case_tac "prime (Suc (prod_list xs))")\n  using prod_list_lt apply fastforce\n  apply (frule prime_factor)\n   apply clarsimp\n  apply (case_tac "length xs = 0"; clarsimp)\n   apply (rule prod_list_gt_zero; clarsimp)\n  using prime_gt_one apply fastforce\n  using divides_prod_list divides_diff prime_gt_one one_divides\n  by (metis One_nat_def Suc_diff_Suc cancel_comm_monoid_add_class.diff_cancel lessI nat_less_le)\nlemma infinite_primes: "∃p. prime p ∧ p > n"\n  apply (insert another_prime[where xs="[2 ..< Suc n]"])\n  apply (case_tac "n ≤ 1"; clarsimp)\n   apply (rule_tac x=2 in exI)\n   apply simp\n  apply (rule_tac x=p in exI)\n  apply simp\n  using prime_gt_one by force\nend
\n
import Primes.Basic\nimport Mathlib.Tactic.ByContra\nset_option linter.style.setOption false\nset_option linter.flexible false\nset_option linter.style.whitespace false\n@[grind]\ndef divides (n k : Nat) : Prop :=\n  ∃q, k = n * q\ntheorem divides_one (n : Nat) : divides n 1 -> n = 1 := by\n  intro ⟨q, hq⟩\n  cases n <;> cases q <;> grind\ntheorem divides_not_one (n : Nat) (d : divides n 1) (neq : n ≠ 1) : False := by\n  grind [divides_one]\ntheorem divides_sub (n j k : Nat) (h1 : divides n k) (h2 : divides n j)\n  : divides n (k - j) := by\n  obtain ⟨q1, h1⟩ := h1\n  obtain ⟨q2, h2⟩ := h2\n  unfold divides\n  exists (q1 - q2)\n  grind [Nat.mul_sub]\ntheorem divides_less (n k : Nat) : k ≠ 0 -> divides n k -> n ≤ k := by\n  intro knz div\n  simp at *\n  obtain ⟨q,hq⟩ := div\n  cases q <;> grind\ntheorem divides_trans (n k j) : divides n k -> divides k j -> divides n j := by\n  intro ⟨a,b⟩ ⟨c,d⟩\n  simp [divides] at *\n  exists (a * c)\n  grind\n@[simp, grind]\ndef prod_list (xs : List Nat) : Nat :=\n  match xs with\n  | [] => 1\n  | x :: xs => x * prod_list xs\ntheorem divides_prod_list : ∀ xs x, x ∈ xs -> divides x (prod_list xs) := by\n  intros xs x mem\n  induction xs with\n  | nil => grind\n  | cons y ys ih =>\n    by_cases h : (x = y)\n    · rw [h]\n      simp\n      exists (prod_list ys)\n    · cases mem with\n      | head => grind\n      | tail =>\n        rename_i a\n        have ⟨h, hq⟩ := ih a\n        simp at *\n        rw [hq]\n        exists (y * h)\n        grind\ntheorem prod_list_nz : ∀ xs, (∀ x ∈ xs, x > 0) -> prod_list xs > 0 := by\n  intros xs f\n  induction xs with\n  | nil => grind\n  | cons x xs ih =>\n    obtain b : prod_list xs > 0 := ih (by grind)\n    simp [*]\ntheorem prod_list_lt : ∀ xs, (∀ x ∈ xs, x > 0) -> ∀ y ∈ xs, y <= prod_list xs := by\n  intro xs f y yin\n  induction xs with\n  | nil => grind\n  | cons yp ys ih =>\n    cases yin with\n    | head =>\n      obtain a : prod_list ys > 0 := by grind [prod_list_nz]\n      exact Nat.le_mul_of_pos_right y a\n    | tail _ a =>\n      obtain a : y <= prod_list ys := ih (by grind) a\n      obtain b : yp > 0 := f yp (by grind)\n      apply Nat.le_trans\n      · exact a\n      · exact Nat.le_mul_of_pos_left (prod_list ys) b\n@[simp, grind]\ndef prime (n : Nat) : Prop :=\n  (n > 1) ∧ (∀k, divides k n -> k = 1 ∨ k = n)\ntheorem prime_two : prime 2 := by\n  simp\n  intros k x\n  simp [divides] at x\n  have ⟨q,hq⟩ := x\n  (cases q <;> cases k <;> grind)\ntheorem prime_factor : ∀k, ¬(prime k) -> 1 < k -> ∃p, prime p ∧ divides p k := by\n  intros k nprime kgt1\n  induction k using Nat.strongRecOn with\n  | ind k' ih =>\n    simp at nprime\n    obtain ⟨x,⟨xd,dvds⟩,xn1,xnk⟩ := nprime kgt1\n    clear nprime\n    by_cases h : prime x\n    · exists x\n      grind\n    · have lt : x < k' := by\n        apply Nat.lt_of_le_of_ne\n        · apply divides_less <;> grind\n        · assumption\n      have gt : 1 < x := by\n        cases x <;> grind\n      obtain ⟨p,⟨prm,dvds⟩⟩ := ih x lt h gt\n      exists p\n      refine ⟨prm, ?_⟩\n      apply divides_trans\n      · assumption\n      · grind\ntheorem another_prime (xs : List Nat) (xsgt : ∀x, x ∈ xs -> 1 < x)\n  : ∃p, prime p ∧ p ∉ xs := by\n  by_cases h : prime (Nat.succ (prod_list xs))\n  · exists (Nat.succ (prod_list xs))\n    refine ⟨h, ?a⟩\n    by_contra\n    have lt : Nat.succ (prod_list xs) ≤ prod_list xs := by\n      apply prod_list_lt <;> grind\n    grind\n  · have ⟨pf, isprm, dvds⟩ : ∃p, prime p ∧ divides p (Nat.succ (prod_list xs)) := by\n      apply prime_factor\n      · exact h\n      · grind [prod_list_nz]\n    by_cases g : pf ∈ xs\n    · have pfdvds : divides pf (prod_list xs) := by\n        apply divides_prod_list <;> grind\n      have divone : divides pf ((Nat.succ (prod_list xs)) - prod_list xs) := by\n        apply divides_sub <;> grind\n      have also : divides pf 1 := by grind\n      grind [divides_not_one]\n    · grind\ntheorem infinite_primes : ∀ n, ∃p, prime p ∧ p > n := by\n  intros n\n  by_cases h : ¬(1 < n)\n  · exists 2\n    grind [prime_two]\n  · simp at h\n    obtain ⟨p, prm, notin⟩ := another_prime (List.range' 2 n) (by grind)\n    refine ⟨p, prm, ?notin⟩\n    grind
\n
open arithmeticTheory listTheory prim_recTheory listRangeTheory;\n     \nDefinition divides_def:\n  divides n k = ∃q. q * n = k\nEnd\nTheorem divides_not_one:\n  ∀n. divides n 1 ⇒ n ≠ 1 ⇒ F\nProof\n  simp[divides_def]\nQED\nTheorem divides_less:\n  k ≠ 0 ⇒ divides n k ⇒ n ≤ k\nProof\n  rpt strip_tac\n  >> gvs[divides_def]\nQED\nTheorem divides_trans:\n  divides a b ⇒ divides b c ⇒ divides a c\nProof\n  rpt strip_tac\n  >> gvs[divides_def]\n  >> qexists ‘q * q'’\n  >> gvs[MULT_ASSOC_COMM]\nQED\nTheorem divides_sub:\n  divides n k ⇒ divides n j ⇒ divides n (k - j)\nProof\n  rpt strip_tac\n  >> metis_tac[RIGHT_SUB_DISTRIB, divides_def]\nQED\n            \nDefinition prod_list_def:\n  (prod_list [] = 1) ∧\n  (prod_list (x :: xs) = x * prod_list xs)\nEnd\nTheorem divides_prod_list:\n  x ∈ set xs ⇒ divides x (prod_list xs)\nProof\n  Induct_on ‘xs’\n  >- fs[]\n  >- (fs[]\n      >> rpt strip_tac\n      >- (fs[prod_list_def, divides_def]\n          >> qexists_tac ‘prod_list xs’\n          >> simp[])\n      >- (fs[divides_def, prod_list_def]\n          >> qexists_tac ‘h * q’\n          >> rev_drule EQ_SYM\n          >> strip_tac\n          >> fs[]))\nQED      \nTheorem prod_list_nz:\n  ∀xs. (∀x. x ∈ set xs ⇒ 0 < x) ⇒ 0 < prod_list xs\nProof\n  rpt strip_tac\n  >> Induct_on ‘xs’\n  >> fs[prod_list_def]\nQED\n     \nTheorem prod_list_lt:\n  ∀xs. (∀x. x ∈ set xs ⇒ 0 < x) ⇒ ∀y. y ∈ set xs ⇒ y ≤ prod_list xs\nProof\n  rpt strip_tac\n  >> Induct_on ‘xs’\n  >> gvs[]\n  >> rpt strip_tac\n  >> gvs[prod_list_def]\n  >> metis_tac[prod_list_nz, LE_MULT_CANCEL_LBARE, LE_TRANS]\nQED\nDefinition prime_def:\n  prime n = ((1 < n) ∧ (∀k. divides k n ⇒ k = 1 ∨ k = n))\nEnd\nTheorem prime_zero:\n  ¬(prime 0)\nProof\n  fs[prime_def]\nQED        \nTheorem prime_one:\n  ¬(prime 1)\nProof\n  fs[prime_def]\nQED\nTheorem prime_gt_one[simp]:\n  prime n ⇒ 1 < n\nProof\n  fs[prime_def]\nQED\n              \nTheorem prime_two:\n  prime 2\nProof        \n  fs[prime_def]\n  >> rpt strip_tac\n  >> fs[divides_def]\n  >> (Cases_on ‘k’ >> Cases_on ‘q’ >> fs[MULT_SUC])\nQED\nTheorem divides_gt1_gt0:\n  ∀n k. divides n k ⇒ 1 < k ⇒ 0 < n\nProof\n  rpt strip_tac\n  >> gvs[divides_def]\n  >> (Cases_on ‘q’ >> gvs[MULT_SUC])\n  >> (Cases_on ‘n’ >> gvs[])\nQED\nTheorem prime_factor:\n  ∀k. ¬(prime k) ⇒ 1 < k ⇒ ∃p. prime p ∧ divides p k\nProof\n  completeInduct_on ‘k’\n  >> rpt strip_tac\n  >> qpat_x_assum ‘¬_’\n                  (fn h => assume_tac\n                          (REWRITE_RULE [prime_def] h))\n  >> gvs[]\n  >> Cases_on ‘prime k'’\n  >- (qexists ‘k'’ >> simp[])\n  >- (first_x_assum $ qspecl_then [‘k'’] mp_tac\n      >> strip_tac\n      >> ‘0 < k'’ by metis_tac[divides_gt1_gt0]\n      >> ‘1 < k'’ by decide_tac\n      >> ‘k' <= k’ by gvs[divides_less]\n      >> ‘k' < k’ by decide_tac\n      >> first_x_assum drule\n      >> strip_tac\n      >> gvs[]\n      >> qexists ‘p’\n      >> metis_tac[divides_trans])\nQED\nTheorem gt1_gt0_weaken:\n  ∀x. 1 < x ⇒ 0 < x\nProof\n  strip_tac >> decide_tac\nQED\nTheorem another_prime:\n  ∀(xs : num list). (∀x. x ∈ set xs ⇒ 1 < x)\n                    ⇒ ∃p. prime p ∧ p ∉ set xs\nProof\n  rpt strip_tac\n  >> Cases_on ‘prime (SUC (prod_list xs))’\n  >- (qexists ‘SUC (prod_list xs)’\n      >> metis_tac[LESS_REFL, OR_LESS,\n                   prod_list_lt, gt1_gt0_weaken])\n  >- (drule prime_factor   \n      >> impl_tac\n      >- metis_tac[ONE, LESS_MONO, prod_list_nz,gt1_gt0_weaken]\n      >- (strip_tac\n          >> Cases_on ‘MEM p xs’\n          >- (‘divides p (prod_list xs)’\n                by metis_tac[divides_prod_list]\n              >> ‘divides p ((SUC (prod_list xs)) - prod_list xs)’\n                by metis_tac [divides_sub]\n              >> gvs[]\n              >> metis_tac[prime_one, prime_zero, divides_not_one])\n          >- (qexists ‘p’ >> metis_tac[])))\nQED\n                    \nTheorem infinite_primes:\n    ∀n. ∃p. prime p ∧ p > n\nProof\n  strip_tac\n  >> Cases_on ‘n < 1’\n  >- (qexists ‘2’ >> simp[prime_two])\n  >- (qspec_then ‘listRangeINC 2 n’ assume_tac another_prime\n      >> ‘∀x. MEM x [2 .. n] ⇒ 1 < x’\n        by (rpt strip_tac >> gvs[MEM_listRangeINC])\n      >> first_x_assum rev_drule\n      >> rpt strip_tac\n      >> qexists ‘p’\n      >> gvs[MEM_listRangeINC, prime_gt_one]\n      >> ‘p ≠ 0’ by metis_tac[prime_zero]\n      >> ‘p ≠ 1’ by metis_tac[prime_one]\n      >> decide_tac)\nQED
\n
open import Data.Nat renaming (ℕ to Nat)\nopen import Data.Nat.Properties\nopen import Relation.Binary.PropositionalEquality\nopen import Data.Product\nopen import Data.Empty\nopen import Relation.Nullary.Negation\nopen import Data.List\nopen import Data.Sum\nopen import Relation.Nullary.Decidable\nopen import Relation.Binary\nopen import Relation.Nullary.Reflects\nopen import Data.Nat.Divisibility\nopen import Data.Bool using (Bool; true; false)\nopen import Data.Fin using (zero; suc; Fin; toℕ; fromℕ; fromℕ<)\nopen import Data.Fin.Properties using (toℕ-fromℕ; toℕ-fromℕ<)\nopen import Induction.WellFounded\nopen import Data.Nat.Induction using (<-wellFounded; <-rec)\nimport Data.List.Membership.DecPropositional as DecPropMembership\nopen DecPropMembership Data.Nat._≟_\nopen import Data.List.Relation.Unary.Any using (here; there)\n-- The prime decision procedure was with assistance from https://gist.github.com/copumpkin/1286093\ndiv-goes-into : ∀ i k → k ≢ 0 → i ∣ k → i ≤ k\ndiv-goes-into i k neq (divides zero eq) = ⊥-elim (neq eq)\ndiv-goes-into zero k neq (divides (suc q) eq) = z≤n\ndiv-goes-into (suc i) k neq (divides-refl (suc q)) = s≤s (m≤m+n i (q * suc i))\ndivides-zero : ∀ i → 0 ∣ i → i ≡ 0\ndivides-zero zero (divides q eq) = refl\ndivides-zero (suc i) (divides q eq) rewrite *-comm q 0 = eq\ndivides-trans : ∀ {i j k} → i ∣ j → j ∣ k → i ∣ k\ndivides-trans {i} (divides-refl q₁) (divides q₂ eq₂) = divides (q₂ * q₁) (trans eq₂ (sym (*-assoc q₂ q₁ i)))\ndivides-sub : ∀ {i j k} → i ∣ j → i ∣ k → i ∣ (j ∸ k)\ndivides-sub {i} (divides-refl q₁) (divides-refl q₂) = divides (q₁ ∸ q₂) (sym (*-distribʳ-∸ i q₁ q₂))\ndivides-one : ∀ i → i ∣ 1 → i ≡ 1\ndivides-one zero (divides (suc q) eq) rewrite *-comm q 0 = ⊥-elim (1+n≢0 eq)\ndivides-one (suc zero) (divides (suc q) eq) = refl\ndivides-not-one : ∀ {i} → i ∣ 1 → i ≢ 1 → ⊥\ndivides-not-one {zero} (divides q eq) neq rewrite *-comm q 0 = 1+n≢0 eq\ndivides-not-one {suc zero} (divides q eq) neq = neq refl\ndivides-not-one {2+ i} (divides zero eq) neq = 1+n≢0 eq\ndivides-not-one {2+ i} (divides (suc q) eq) neq = 1+n≢0 (sym (suc-injective eq))\nlt-left-suc : ∀ i j → i ≤ j → i ≢ j → suc i ≤ j\nlt-left-suc zero zero z≤n p = ⊥-elim (p refl)\nlt-left-suc zero (suc j) z≤n p = s≤s z≤n\nlt-left-suc (suc i) zero () p\nlt-left-suc (suc i) (suc j) (s≤s x) p = s≤s (lt-left-suc i j x λ q → p (cong suc q))\nnot : {A : Set} → Dec A → Dec (¬ A)\nnot (yes p) = no (λ z → z p)\nnot (no ¬p) = yes ¬p\nDNE : {A : Set} → Dec A → ¬ ¬ A → A\nDNE (yes p) f = p\nDNE (no ¬p) f = ⊥-elim (f ¬p)\nDecide : {A : Set} (P : A → Set) → Set\nDecide P = ∀ i → Dec (P i)\nlt-lower : ∀ {i j} → suc i ≤ suc j → i ≢ j → suc i ≤ j\nlt-lower {zero} {zero} (s≤s p) q = ⊥-elim (q refl)\nlt-lower {zero} {suc j} (s≤s p) q = s≤s z≤n\nlt-lower {suc i} {suc j} (s≤s p) q = s≤s (lt-lower p λ x → q (cong suc x))\nlt-decide : ∀ i → (P : Nat → Set) (p? : ∀ n → n < i → Dec (P n)) → (∀ n → n < i → P n) ⊎ (Σ _ λ j → j < i × ¬ (P j))\nlt-decide zero P p? = inj₁ λ _ ()\nlt-decide (suc i) P p? with lt-decide i P h\n  where\n    h : (n : Nat) → n < i → Dec (P n)\n    h n lt = p? n (s≤s (<⇒≤ lt))\n... | inj₂ (a , b , c) = inj₂ (a , s≤s (≤-trans (n≤1+n a) b) , c)\n... | inj₁ x with p? i ≤-refl\n... | no ¬a = inj₂ (i , ≤-refl , ¬a)\n... | yes a = inj₁ h\n  where\n    h : (n : Nat) → suc n ≤ suc i → P n\n    h n lt with n ≟ i\n    ... | yes refl = a\n    ... | no ¬a = x n (lt-lower lt ¬a)\n¬lt-decide : ∀ i → (P : Nat → Set) (p? : ∀ n → n < i → Dec (P n)) → (∀ n → n < i → ¬ P n) ⊎ (Σ _ λ j → j < i × (P j))\n¬lt-decide i P p? with lt-decide i (λ x → ¬ (P x)) (λ n x → not (p? n x))\n... | inj₁ x = inj₁ x\n... | inj₂ (a , b , c) = inj₂ (a , b , DNE (p? a b) c)\nrecord Prime (n : Nat) : Set where\n  constructor isprime\n  field\n    gt1 : n > 1\n    div : ∀ k → k ∣ n → k ≡ 1 ⊎ k ≡ n\nopen Prime\nzero-prime : ¬ (Prime 0)\nzero-prime ()\nprime-not-zero : ∀ p → Prime p → p ≢ 0\nprime-not-zero p x refl = zero-prime x\none-prime : ¬ (Prime 1)\none-prime (isprime (s≤s ()) div)\ntwo-prime : Prime 2\ntwo-prime .gt1 = s≤s (s≤s z≤n)\ntwo-prime .div zero (divides (suc q) eq) rewrite *-comm q 0 = ⊥-elim (1+n≢0 eq)\ntwo-prime .div (suc zero) (divides (suc q) eq) = inj₁ refl\ntwo-prime .div (2+ zero) (divides (suc q) eq) = inj₂ refl\nrecord Composite (n : Nat) : Set where\n  constructor composite\n  field\n    p : Nat\n    Pp : Prime p\n    p<n : p < n\n    p∣ : p ∣ n\nnot-prime-and-composite : ∀ p → Prime p → Composite p → ⊥\nnot-prime-and-composite _ (isprime gt2 div₁) (composite p (isprime gt3 div₂) p<n p∣) with div₁ p p∣\n... | inj₁ refl = one-prime (isprime gt3 div₂)\n... | inj₂ refl = 1+n≰n p<n\nprime-or-composite : ∀ p → p > 1 → Prime p ⊎ Composite p\nprime-or-composite (suc zero) (s≤s ())\nprime-or-composite (2+ p) lt = <-rec _ h p\n  where\n    h : (x : Nat) →\n         ({y : Nat} → suc y ≤ x → Prime (2+ y) ⊎ Composite (2+ y)) →\n         Prime (2+ x) ⊎ Composite (2+ x)\n    h x f with ¬lt-decide x (λ k → (2+ k) ∣ (2+ x)) (λ n nlt → 2+ n ∣? 2+ x)\n    ... | inj₂ (ev₁ , ev₂ , ev₃) with f ev₂\n    h x f | inj₂ (ev₁ , ev₂ , ev₃) | inj₁ prm = inj₂ (composite (2+ ev₁) prm (s≤s (s≤s ev₂)) ev₃)\n    h x f | inj₂ (ev₁ , ev₂ , ev₃) | inj₂ (composite p Pp (s≤s p<n) p∣) =\n        inj₂ (composite p Pp (s≤s (≤-trans p<n (≤-trans ev₂ (n≤1+n x)))) (divides-trans p∣ ev₃))\n    h x f | inj₁ eq = inj₁ (isprime (s≤s (s≤s z≤n)) lemma)\n      where\n        lemma : (k : Nat) → k ∣ 2+ x → k ≡ 1 ⊎ k ≡ 2+ x\n        lemma k dv with k ≟ 1 | k ≟ (2+ x)\n        ... | no ¬a | yes refl = inj₂ refl\n        ... | yes refl | no ¬b = inj₁ refl\n        ... | yes refl | yes ()\n        lemma zero dv | no ¬a | no ¬b rewrite divides-zero (2+ x) dv = inj₂ refl\n        lemma (suc zero) dv | no ¬a | no ¬b = inj₁ refl\n        lemma (2+ k) dv | no ¬a | no ¬b with suc k ≤? x\n        ... | yes k≤x = ⊥-elim (eq k k≤x dv)\n        ... | no ¬k≤x = ⊥-elim (¬k≤x sothen)\n          where\n            one : 2+ k ≤ 2+ x\n            one = div-goes-into (2+ k) (2+ x) 1+n≢0 dv\n            two : k ≤ x\n            two with one\n            ... | s≤s (s≤s a) = a\n            also : k ≢ x\n            also x = ¬b (cong suc (cong suc x))\n            sothen : suc k ≤ x\n            sothen = lt-left-suc k x two also\nprod-list : List Nat → Nat\nprod-list [] = 1\nprod-list (x ∷ xs) = x * prod-list xs\nprod-list-nz : ∀ xs → (∀ x → x ∈ xs → x > 0) → prod-list xs > 0\nprod-list-nz [] f = s≤s z≤n\nprod-list-nz (x ∷ []) f rewrite *-comm x 1 rewrite +-comm x 0 = f x (here refl)\nprod-list-nz (x ∷ x₁ ∷ xs) f = h {x} (f x (here refl)) (prod-list-nz (x₁ ∷ xs) (λ x₂ z → f x₂ (there z)))\n  where\n    h : ∀ {i j} → 1 ≤ i → 1 ≤ j → 1 ≤ i * j\n    h {suc i} {suc j} (s≤s a) (s≤s b) = s≤s z≤n\nprod-list-NZ : ∀ xs → (∀ x → x ∈ xs → x > 0) → NonZero (prod-list xs)\nprod-list-NZ xs f = >-nonZero (prod-list-nz xs f)\nprod-list-lt : ∀ xs → (∀ x → x ∈ xs → x > 0) → ∀ y → y ∈ xs → y ≤ prod-list xs\nprod-list-lt [] f y ()\nprod-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) ⦄\nprod-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))\n  where\n    lt+ : ∀ {i j k} → i ≤ j → i ≤ j + k\n    lt+ z≤n = z≤n\n    lt+ (s≤s x) = s≤s (lt+ x)\n    also : ∀ {i j k} → i ≤ k → 1 ≤ j → i ≤ j * k\n    also a (s≤s z≤n) = lt+ a\nprod-list-divides : ∀ xs x → x ∈ xs → x ∣ prod-list xs\nprod-list-divides [] x ()\nprod-list-divides (y ∷ xs) x (here refl) = divides (prod-list xs) (*-comm y (prod-list xs))\nprod-list-divides (y ∷ xs) x (there p) with prod-list-divides xs x p\n... | divides q eq rewrite eq = divides (y * q) (sym (*-assoc y q x))\nprime-not-in : ∀ xs → (∀ x → x ∈ xs → x > 0) → Σ _ λ k → k ∉ xs × Prime k\nprime-not-in xs gt with 2 ≤? prod-list xs\n... | no ¬a = 2 , lemma , two-prime\n  where\n    lemma : 2 ∈ xs → ⊥\n    lemma pf with prod-list-lt xs gt 2 pf\n    ... | also = ¬a also\n... | yes a with prime-or-composite (suc (prod-list xs)) (s≤s (≤-trans (s≤s z≤n) a))\n... | inj₁ x = suc (prod-list xs) , lemma , x\n  where\n    lemma : (suc (prod-list xs)) ∈ xs → ⊥\n    lemma pf with prod-list-lt xs gt (suc (prod-list xs)) pf\n    ... | also = 1+n≰n also\n... | inj₂ (composite p Pp p<n p∣) with p ∈? xs\n... | no ¬b = p , ¬b , Pp\n... | yes b with prod-list-divides xs p b\n... | divs with divides-sub p∣ divs\n... | sothen = ⊥-elim (lemma {p} {prod-list xs} sothen λ{ refl → one-prime Pp })\n  where\n    suc-sub : ∀ i → suc i ∸ i ≡ 1\n    suc-sub zero = refl\n    suc-sub (suc i) = suc-sub i\n    lemma : ∀ {i j} → i ∣ (suc j ∸ j) → i ≢ 1 → ⊥\n    lemma {_} {j} div neq rewrite suc-sub j = divides-not-one div neq\nlist-up-to : Nat → List Nat\nlist-up-to 0 = 1 ∷ []\nlist-up-to (suc n) = suc n ∷ list-up-to n\nlist-up-to-nz : ∀ k x → x ∈ list-up-to k → x > 0\nlist-up-to-nz zero x (here refl) = s≤s z≤n\nlist-up-to-nz (suc k) x (here refl) = s≤s z≤n\nlist-up-to-nz (suc k) x (there p) = list-up-to-nz k x p\nlist-up-to-contains : ∀ i j → j ≤ i → j ≢ 0 → j ∈ list-up-to i\nlist-up-to-contains zero zero z≤n b = ⊥-elim (b refl)\nlist-up-to-contains zero (suc j) () b\nlist-up-to-contains (suc i) zero z≤n b = ⊥-elim (b refl)\nlist-up-to-contains (suc i) (suc j) (s≤s a) b with suc i ≟ suc j\n... | no ¬c = there (list-up-to-contains i (suc j) (lt-left-suc j i a λ x → ¬c (cong suc (sym x))) b)\n... | yes refl = here refl\ninfinite-primes : ∀ i → Σ _ λ p → p > i × Prime p\ninfinite-primes zero = 2 , s≤s z≤n , two-prime\ninfinite-primes (suc i) with prime-not-in (list-up-to (2+ i)) (list-up-to-nz (2+ i))\n... | p , notin , Pp = p , DNE (2+ i ≤? p) lemma , Pp\n  where\n    notzero : p ≢ 0\n    notzero = prime-not-zero p Pp\n    implies : ∀ {a b} → (suc a ≤ b → ⊥) → (a ≡ b) ⊎ (a > b)\n    implies {a} {b} x with compare a b\n    ... | less .a k = ⊥-elim (x (s≤s (m≤m+n a k)))\n    ... | equal .a = inj₁ refl\n    ... | greater .b k = inj₂ (s≤s (m≤m+n b k))\n    lemma : ((2+ i ≤ p) → ⊥) → ⊥\n    lemma x with implies x\n    ... | inj₁ refl = notin (there (here refl))\n    ... | 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))
","headings":[]}}