Infinite primes : an exercise in basic Lean

Stream: new members

[Ioannis Konstantoulas]

Hello all; I recently completed my first big exercise for Lean 4 practice : a proof of the infinitude of primes completely from scratch, using only Nat lemmas from Core for the four operations, and using only the propext axiom. I wanted to practice writing terms directly, so I made minimal use of tactics.

The linked README contains a hastily written overview, but the source is somewhat tagliatelle code, so if you have any pointers on how to organize/structure it, please let me know. In particular, I'd like some directions on how to create good doc-strings.

Also, I am not sure what to do about licenses and the like; do I need to use a specific license, or none at all? This is an exercise written by an amateur, so people should not mimic it ( :laughing: ) but what is the general practice?

[Kevin Buzzard]

We generally license Lean code with the Apache license because this is the license which Lean uses.

[Ioannis Konstantoulas]

Kevin Buzzard said:

We generally license Lean code with the Apache license because this is the license which Lean uses.

Great, so I will use the same.

[Martin Dvořák]

Why don't you express the main result in terms of the "official" NatPrime definition?
It should be approximately zero extra work and much better presentability of your result!

[Martin Dvořák]

(deleted)

[Ioannis Konstantoulas]

Martin Dvořák said:

Why don't you express the main result in terms of the "official" NatPrime definition?
It should be approximately zero extra work and much better presentability of your result!

I do not know yet about what exists in the database, I wanted to implement everything myself. I used the Prime definition I did because it is the right generalization in other domains, it is harder to prove decidability for it (making it a worthier challenge), and I wanted to prove as many equivalences as I could for primality. I use all the equivalent definitions in an essential way.

[Martin Dvořák]

I mean, you can keep everything you have but add

theorem main_result :
    ∀ n, ∃ p, NatPrime p ∧ p > n

for sake of the average reader.

[Mario Carneiro]

It's actually spelled docs#Nat.Prime

[Martin Dvořák]

The project doesn't import Mathlib.

[Martin Dvořák]

Speaking of docs#Nat.Prime vs decidable definitions, I wrote an extremely amateurish characterization of primes:
https://github.com/madvorak/lean4-exercises/blob/main/PrimeTesting.lean

[Martin Dvořák]

Ioannis Konstantoulas said:

I used the Prime definition I did because it is the right generalization in other domains

You can have a look at how Mathlib does it. In particular docs#Nat.Prime is defined in Mathlib as follows:

structure Units (α : Type u) [Monoid α] where
  /-- The underlying value in the base `Monoid`. -/
  val : α
  /-- The inverse value of `val` in the base `Monoid`. -/
  inv : α
  /-- `inv` is the right inverse of `val` in the base `Monoid`. -/
  val_inv : val * inv = 1
  /-- `inv` is the left inverse of `val` in the base `Monoid`. -/
  inv_val : inv * val = 1

structure Irreducible [Monoid α] (p : α) : Prop where
  /-- `p` is not a unit -/
  not_unit : ¬IsUnit p
  /-- if `p` factors then one factor is a unit -/
  isUnit_or_isUnit' : ∀ a b, p = a * b → IsUnit a ∨ IsUnit b

def Prime (p : ℕ) :=
  Irreducible p

[Ioannis Konstantoulas]

Thank you for the suggestions!