Euclid's proof from LftCM 2023 tutorial

Stream: new members

[Moti Ben-Ari]

In the first tutorial the following proof of Euclid's theorem that there is an infinite number of primes is given:

theorem Euclid_Thm (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
  let p := minFac (Nat.factorial n + 1)
  have f1 : factorial n + 1 ≠ 1 := Nat.ne_of_gt <| Nat.succ_lt_succ <| factorial_pos _
  have pp : Nat.Prime p := minFac_prime f1
  have np : n ≤ p :=
    le_of_not_ge fun h =>
      have h₁ : p ∣ factorial n := dvd_factorial (minFac_pos _) h
      have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (minFac_dvd _)
      pp.not_dvd_one h₂
  exact ⟨p, np, pp⟩

I don't understand the line le_of_not_ge fun h =>. It seems to be decomposing ¬ n≥p into n≥p → False. How does fun h => do that? I don't think I've seen this syntax in MiL.

[Eric Wieser]

Moti Ben-Ari said:

It seems to be decomposing ¬ n≥p into n≥p → False.

That's because this is the definition of ¬ (docs#Not)!

[Moti Ben-Ari]

Sorry for not being clear. I know the definition of negation, but the previous occurrences of n≥p → False that I have seen have used intro to make n≥p into a hypothesis and False into a goal. How does fun h => do work in this situation? Would it be possible to use intro instead?

[Eric Wieser]

A rough analogy is that in term-mode, fun x => by foo is the same as by intro x; foo

[Eric Wieser]

Or alternatively, in tactic-mode exact fun x => y is the same as intro x; exact y

[Damiano Testa]

In this case, this is essentially equivalent to what you see:

theorem Euclid_Thm (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
  let p := minFac (Nat.factorial n + 1)
  have f1 : factorial n + 1 ≠ 1 := Nat.ne_of_gt <| Nat.succ_lt_succ <| factorial_pos _
  have pp : Nat.Prime p := minFac_prime f1
  have np : n ≤ p := by
    apply le_of_not_ge
    intro h
    have h₁ : p ∣ factorial n := dvd_factorial (minFac_pos _) h
    have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (minFac_dvd _)
    exact pp.not_dvd_one h₂
  exact ⟨p, np, pp⟩

[Eric Wieser]

What's relevant here is that everything after the have np : n ≤ p := is in term-mode not tactic mode, but I think MiL tries very hard to pretend that term-mode proofs don't exist (as they're harder to learn to write, and often less readable)

[Moti Ben-Ari]

Thanks! I am looking into Lean for teaching math and tactics really are easier than terms.

[Damiano Testa]

All the have ... := ...s in the proof above can be converted to have ... := by exact ... (I think, I did not test it).

[Moti Ben-Ari]

For the benefit of other newbees, I am trying to modify this program to use a minimal number of Lean constructs: tactics only, no anonymous, explicit applications of tactics and rewrites. This is as far as I can get:

import Mathlib.Data.Nat.Prime
open Nat

theorem Euclid_Thm (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
  let p := minFac (factorial n + 1)
  have f1 : factorial n + 1 ≠ 1 := by
    apply Nat.ne_of_gt <| succ_lt_succ <| factorial_pos _
  have pp : Nat.Prime p := by
    apply minFac_prime f1
  have np : n ≤ p := by
    apply le_of_not_ge
    intro h
    have h₁ : p ∣ factorial n := by
      apply dvd_factorial (minFac_pos _) h
    have h₂ : p ∣ 1 := by
      apply (Nat.dvd_add_iff_right h₁).mpr (minFac_dvd _)
    apply pp.not_dvd_one
    exact h₂
  exact ⟨p, np, pp⟩

1. Is pp.not_dvd_one an anonymous projection? If so I should be able to do something like apply not_dvd_one pp but I get unknown identifier. How can I get rid of the projection or whatever it is?
2. I also want to get rid of the anonymous constructor in the last line. use p works, but I want to do this step-by-step. I tried constructor to prove the two subformulas of the conjunction in the main goal separately using np,pp but couldn't get it to work. Help would be appreciated.

[Kevin Buzzard]

1. pp has type Nat.Prime p so pp.not_dvd_one means Nat.Prime.not_dvd_one pp.
2. Replace exact ⟨p, np, pp⟩ with show_term exact ⟨p, np, pp⟩ to see what the actual constructor used was. It's Exists.intro.

[Moti Ben-Ari]

Thanks, Kevin. I searched the entire collection of Lean documentation and couldn't find any mention of the syntax{ left = ... , right = ... }. But I found another way of doing it that should be easier to understand for newbees:

apply Exists.intro p
    constructor
    · exact np
    · exact pp

[Kevin Buzzard]

{ left = ... , right = ... } is just the default constructor for And(it's a structure and those are the names of the fields). You could use And.intro.