Zulip Chat Archive

Stream: new members

Topic: Is there a concept of 'efficiency' in Lean?


debord (Jan 22 2023 at 08:07):

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 (Jan 22 2023 at 09:19):

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 (Jan 22 2023 at 09:29):

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

Damiano Testa (Jan 22 2023 at 11:02):

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 (Jan 22 2023 at 11:30):

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 (Jan 22 2023 at 11:51):

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 (Jan 22 2023 at 18:07):

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 (Jan 22 2023 at 18:09):

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

Marcus Rossel (Jan 22 2023 at 18:19):

(deleted)

Kevin Buzzard (Jan 22 2023 at 18:30):

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 (Jan 23 2023 at 00:30):

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

Kevin Buzzard (Jan 23 2023 at 00:55):

Oh lol I must have missed the memo

Kevin Buzzard (Jan 23 2023 at 00:56):

I think the answer is "since forever" btw

Mario Carneiro (Jan 23 2023 at 04:47):

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

Mario Carneiro (Jan 23 2023 at 04:48):

it was only the style guide that changed


Last updated: Dec 20 2023 at 11:08 UTC