Is there a concept of 'efficiency' in Lean?

Stream: new members

[debord]

Often times in programming, more efficient and less wasteful algorithms/code is preferable over big memory-eating clunky code. Does something like this apply when proving theorems in Lean? For example, I wrote this big ugly proof for an exercise in Theorem Proving in Lean 4:

example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
  Iff.intro
    (λ h : ∃ x, p x ∨ q x =>
      Exists.elim h
        (λ w =>
          λ hw : p w ∨ q w =>
            byCases
              (λ hp : p w =>
                Or.intro_left (∃ x, q x) (Exists.intro w hp))
              (λ hnp : ¬p w =>
                have hq : q w := Or.elim hw
                  (λ hpw : p w =>
                    absurd hpw hnp)
                  (λ hqr : q w =>
                    hqr)
                Or.intro_right (∃ x, p x) (Exists.intro w hq))))
    (λ h : (∃ x, p x) ∨ (∃ x, q x) =>
      Or.elim h
        (λ hp : ∃ x, p x =>
          Exists.elim hp
            (λ w =>
              λ hw : p w =>
                Exists.intro w (Or.intro_left (q w) hw)))
        (λ hq : ∃ x, q x =>
          Exists.elim hq
            (λ w =>
              λ hw : q w =>
                Exists.intro w (Or.intro_right (p w) hw))))

And the book provides this much smaller, more elegant solution:

example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
  Iff.intro
    (fun ⟨a, (h1 : p a ∨ q a)⟩ =>
      Or.elim h1
        (fun hpa : p a => Or.inl ⟨a, hpa⟩)
        (fun hqa : q a => Or.inr ⟨a, hqa⟩))
    (fun h : (∃ x, p x) ∨ (∃ x, q x) =>
      Or.elim h
        (fun ⟨a, hpa⟩ => ⟨a, (Or.inl hpa)⟩)
        (fun ⟨a, hqa⟩ => ⟨a, (Or.inr hqa)⟩))

Is there any technical reason that the latter should be preferred to the former? Does it 'run' better? Is it just down to human readability, line count, and perhaps mathematical elegance?

[Bulhwi Cha]

I don't think your proof is big and ugly. Mine was also longer than the one presented in the book:

theorem exists_or {α : Type} (p q : α → Prop) :
        (∃ x : α, p x ∨ q x) ↔ (∃ x : α, p x) ∨ (∃ x : α, q x) :=
  Iff.intro
    (fun h : ∃ x : α, p x ∨ q x =>
      Exists.elim h
        (fun w : α =>
          fun hw : p w ∨ q w =>
            Or.elim hw
              (fun hp : p w => Or.inl (Exists.intro w hp))
              (fun hq : q w => Or.inr (Exists.intro w hq))))
    (fun h : (∃ x : α, p x) ∨ (∃ x : α, q x) =>
      Or.elim h
        (fun hp : (∃ x : α, p x) =>
          Exists.elim hp
            (fun w : α =>
              fun hw : p w =>
                Exists.intro w (Or.inl hw)))
        (fun hq : (∃ x : α, q x) =>
          Exists.elim hq
            (fun w : α =>
              fun hw : q w =>
                Exists.intro w (Or.inr hw))))

[Bulhwi Cha]

But you can prove this exercise without using Classical.byCases. I think that's what matters.

[Damiano Testa]

From a mathematical point of view, I would say that there is little difference between a proof that is long and slow and one that is short and fast.

From the point of view of maintaining a library of mathematical results, I would say that short and fast proofs are usually preferable, since they are likely easier to fix, quicker to compile and generally probably more streamlined.

As a mathematician, I find the issue with axioms secondary and generally tend to prefer using all axioms at my disposal!

[Kevin Buzzard]

In good mathematics writing you'll often find that the key ideas are emphasized and tedious technical clutter is dealt with carelessly or skipped, because it's the ideas which we're excited about rather than the details. So I can see appeal in a proof of this of the form by finish or by aesop or whatever, which is much shorter to read and takes much longer to run.

[Bulhwi Cha]

If someone is new to type theory and wants to understand how the propositions-as-types paradigm works, it can be helpful for them to write proofs of the exercises in Chapters 3–4 of #tpil4 without using convenient abbreviations. But after all, it's a matter of preference.

[Kevin Buzzard]

When I was new to type theory, I found the following kind of proof much more helpful than the verbose solutions above:

example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
⟨λ ⟨x, h⟩ => h.elim (λ hpx => Or.inl ⟨x, hpx⟩) $ λ hqx => Or.inr ⟨x, hqx⟩,
 λ h => h.elim (λ ⟨x, hx⟩ => ⟨x, Or.inl hx⟩) $ λ ⟨x, hx⟩ => ⟨x, Or.inr hx⟩⟩

It hammers home the fact that a proof is a function. I find it also much easier to write than the more verbose solutions above, where you can lose track of things like parentheses.

[Patrick Massot]

Kevin, I think your syntax is a mix of Lean 3 and Lean 4 that doesn't exist anywhere.

[Marcus Rossel]

(deleted)

[Kevin Buzzard]

The code I posted compiles in current lean 4

variable (p q : α → Prop)

example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
⟨λ ⟨x, h⟩ => h.elim (λ hpx => Or.inl ⟨x, hpx⟩) $ λ hqx => Or.inr ⟨x, hqx⟩,
 λ h => h.elim (λ ⟨x, hx⟩ => ⟨x, Or.inl hx⟩) $ λ ⟨x, hx⟩ => ⟨x, Or.inr hx⟩⟩

[Eric Wieser]

Since when was λ valid in lean 4 for that? I thought it was "reclaimed" as a variable name!

[Kevin Buzzard]

Oh lol I must have missed the memo

[Kevin Buzzard]

I think the answer is "since forever" btw

[Mario Carneiro]

yep, both lean 3 and lean 4 support \lam and fun as synonyms

[Mario Carneiro]

it was only the style guide that changed