Answers to exercises in Theorem Proving in lean 4

Stream: new members

[Jonne]

Hi all,

I'm trying to learn Lean 4 (have not used older versions) by reading the following and making the exercises:
https://leanprover.github.io/theorem_proving_in_lean4

I'm wondering if the answers to these are posted somewhere so I can compare mine and also learn from the ones I'm unable to do.

Thanks!

[Kevin Buzzard]

Feel free to ask questions here. I'm not sure the book has any official solutions

[Jonne]

Ok, thanks, here I go :)

• Does the example proof for evenProp 10 look good? It seems to "work", but may not be a good way to do this.
• Is it always the case that when using typ Prop you get noncomputable definitions (which you need to prove yourself) and changing that to Bool is needed to get computable definitions (so you could use #eval for instance)?

def evenProp (n : Nat) : Prop :=
  ∃ m, n = 2 * m

example : evenProp 10 := by
    have evenProp10 : 2 * 5 = 10 := by norm_num
    exact Exists.intro 5 evenProp10

def even (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ m => not (even m)

#check even
#print even
#eval even 22
#eval even 3

I used the following definition for primes.

• Is that a good enough definition, and should I be able to complete the two examples below?
• I'm still working on the proofs, of course, :blush:

def prime (n : ℕ) : Prop :=
    n > 1 ∧ ¬∃d : ℕ, d ∣ n ∧ d ≠ 1 ∧ d ≠ n

example : prime 7 := by
    sorry

example : ¬(prime 9) := by
    have h₃ : 3 * 3 = 9 := by norm_num
    refine Not.intro ?h
    sorry

def infinitely_many_primes : Prop :=
    ∀ p₁, prime p₁ → ∃ p₂, prime p₂ ∧ p₂ > p₁

Thanks!

[Kevin Buzzard]

Here's some golfs of evenProp 10:

import Mathlib

def evenProp (n : Nat) : Prop :=
  ∃ m, n = 2 * m

example : evenProp 10 := by
    exact Exists.intro 5 (by norm_num)

example : evenProp 10 := ⟨5, by norm_num⟩

For #eval, you can't eval an arbitrary Prop because maths is hard. But you might want to read about docs#Decidable .

[Daniel Weber]

You can also use rfl instead of by norm_num

[Kevin Buzzard]

Your definition of prime looks fine, although you're going to have to write some API for it to be usable. For example you will need to show that being prime is equivalent to there being no number d < n such that ..., (i.e. n >= 1 and d | n implies d <= n, which will be in mathlib somewhere) before you have an algorithm for proving that 7 is prime which you can then turn into a proof. Every definition comes with a cost. If you don't want to pay the cost you could change the definition to make it less costly but in mathlib in practice every definition comes with many many basic theorems about it, this is what formalization looks like.

For infinitely_many_primes I would drop prime p_1 -> because it's not necessary.

[Kevin Buzzard]

Daniel Weber said:

You can also use rfl instead of by norm_num

That's true but I would argue that it is bad practice; norm_num is designed to prove equalities between numerals, the fact that rfl works is exposing internal design decisions, which could in theory change later on.

[Daniel Weber]

I don't agree, at least for Nat and Int, but I guess that's up to what you consider internal

[Kevin Buzzard]

I worry that people see that 10=2*5 can be proved by rfl and deduce that some much more complex numerical expression should also be proved by rfl. Sure rfl works for small numbers, but for large numbers the correct tool is norm_num so using rfl is giving out the wrong signals.

[Daniel Weber]

I believe even for more complex expressions the correct tool is rfl — the kernel has special casing to efficiently handle operations on Nat/Int