3 proofs from Mathematics in Lean

Stream: new members

[Michael Bucko]

Used ▸, λ , and a bunch of docs. I am now working on Mathematics in Lean examples (recommendation from @Daniel Weber - thank you, the book is great!).

How would you improve those proofs?

3 proofs

import Mathlib

theorem my_lemma3 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intros x y ε epos ele1 xlt ylt
  have h1 : |x * y| = |x| * |y| := abs_mul x y
  have hprod_lt : |x| * |y| < ε * ε := by
    apply mul_lt_mul'' xlt ylt (abs_nonneg x) (abs_nonneg y)
  have hε_sq_le_ε : ε * ε ≤ ε := by
    calc
      ε * ε ≤ ε * 1 := mul_le_mul_of_nonneg_left ele1 (le_of_lt epos)
      _ = ε := mul_one ε
  have h : |x| * |y| < ε := hprod_lt.trans_le hε_sq_le_ε
  exact h1 ▸ h

example {α : Type} {r s t : Set α} : r ⊆ s → s ⊆ t → r ⊆ t :=
  λ (hr : r ⊆ s) (hs : s ⊆ t) (x : α) (hx : x ∈ r) => hs (hr hx)

example (injg : Function.Injective g) (injf : Function.Injective f) : Function.Injective (g ∘ f) := by
  intros x y h
  apply injf
  apply injg h

[Kevin Buzzard]

"improve" by what metric? Readability? Length-minimisation? adherence to code standards?

[Michael Bucko]

Any improvements and suggestions are welcome. I'd love my proofs to:

1. be more concise, but readable at the same time
2. adhere to code standards, and be highly reusable

Any best practices advise is welcome too. (I finished The Mechanics.., and hope to soon finish Mathematics in Lean, but I want to do it the slow way, and learn as much as possible).

[Kevin Buzzard]

In my experience, conciceness and readability pull in two different directions. And what does reusability mean in the context of proofs? All proofs of a proposition are equal and are "erased at runtime" (so I've heard, I have no idea what I'm talking about here).

[Kevin Buzzard]

import Mathlib
set_option autoImplicit true

-- far more readable
example {α : Type} {r s t : Set α} : r ⊆ s → s ⊆ t → r ⊆ t := by
  -- Assume r ⊆ s and s ⊆ t
  intro (hr : r ⊆ s) (hs : s ⊆ t)
  -- We need to prove r ⊆ t, i.e., for all x, if x ∈ r then x ∈ t.
  -- So assume x ∈ r is arbitrary
  intro (x : α) (hx : x ∈ r)
  -- Because r ⊆ s we know x ∈ s
  apply hr at hx
  -- Because s ⊆ t we deduce x ∈ t
  apply hs at hx
  -- and this was what we wanted to prove
  assumption

-- far more concise
example (injg : Function.Injective g) (injf : Function.Injective f) : Function.Injective (g ∘ f) :=
  fun _ _ h ↦ injf <| injg h

Your last two examples: I can rewrite the first to be readable like the second, or the second to be concise like the first.

[Kevin Buzzard]

I could be even more concise by using $\lambda$ instead of fun but code standards prefer fun so this would be even less readable.

[Michael Bucko]

Kevin Buzzard schrieb:

import Mathlib
set_option autoImplicit true

-- far more readable
example {α : Type} {r s t : Set α} : r ⊆ s → s ⊆ t → r ⊆ t := by
  -- Assume r ⊆ s and s ⊆ t
  intro (hr : r ⊆ s) (hs : s ⊆ t)
  -- We need to prove r ⊆ t, i.e., for all x, if x ∈ r then x ∈ t.
  -- So assume x ∈ r is arbitrary
  intro (x : α) (hx : x ∈ r)
  -- Because r ⊆ s we know x ∈ s
  apply hr at hx
  -- Because s ⊆ t we deduce x ∈ t
  apply hs at hx
  -- and this was what we wanted to prove
  assumption

-- far more concise
example (injg : Function.Injective g) (injf : Function.Injective f) : Function.Injective (g ∘ f) :=
  fun _ _ h ↦ injf <| injg h

Your last two examples: I can rewrite the first to be readable like the second, or the second to be concise like the first.

Beautiful! Also, I am always forgetting about pipelines - <| :man_facepalming:

[metakuntyyy]

Where can I find this document?

[Michael Bucko]

Reusability - I want to start developing tactics, and also make sure that others will be able to re-use them in the most efficient way (find them quickly, understand them quickly, apply them quickly).

Currently, I only know about the simp tag, and autocompletion. I'll read Metaprogramming in Lean 4 soon, and then will be able to say more.

[Michael Bucko]

metakuntyyy schrieb:

Where can I find this document?

Here's the book (it's magical in many ways): https://leanprover-community.github.io/mathematics_in_lean/

[Michael Bucko]

@Kevin Buzzard As for the comments in the proof - I prefer fewer comments (and only comment the critical parts). My assumption is that, if someone really cares to understand, they'll learn how to read code.

The pipeline line in the second proof is awesome (I feel like it'd be awesome to even skip injf and injg (not sure if possible), and get a smart tactic to understand it).

[metakuntyyy]

Ah you are the author of that, great. Loved reading it.

[Michael Bucko]

metakuntyyy schrieb:

Ah you are the author of that, great. Loved reading it.

I'm not an author of that book. I am just reading that book. It's been recommended to me too.