Zulip Chat Archive

Stream: new members

Topic: Irrelevant asymmetry in definitions

Martin Dvořák (Jul 19 2022 at 08:20):

I am unhappy when I read definitions like:
https://github.com/leanprover-community/mathlib/blob/e1c8bded9d8a1cd0e74ab5573a0e0b9d5d30af54/src/data/set/basic.lean#L2403

From my perspective, it should be grouped as (a ∈ s ∧ b ∈ t) ∧ f a b = c not as a ∈ s ∧ (b ∈ t ∧ f a b = c) which it is (implicitly) now. I know it is irrelevant for the math but it is such a pet peeve of mine!

Does anyone else find it annoying? Or, on the contrary, do you prefer the definition as it is written? Sure, it has less parentheses, but my preferred version could also be written as f a b = c ∧ a ∈ s ∧ b ∈ t which would combine esthetic benefits of both.

Thomas Browning (Jul 19 2022 at 08:27):

You could also write it as ∃ a b ∈ s, f a b = c, I think.

Andrew Yang (Jul 19 2022 at 08:29):

I think people value good-looking code more than good-looking ASTs for these minor details.

Martin Dvořák (Jul 19 2022 at 08:31):

Thomas Browning said:

You could also write it as ∃ a b ∈ s, f a b = c, I think.

Yeah. That would be much nicer!

Martin Dvořák (Jul 19 2022 at 08:32):

Andrew Yang said:

I think people value good-looking code more than good-looking ASTs for these minor details.

Ah ok. I don't like it tho — the minor ugliness of AST carries over to asymmetry of my proofs (which I find ugly).

Yaël Dillies (Jul 19 2022 at 10:24):

I agree that it should be ∃ (a ∈ s) (b ∈ t), f a b = c. I meant to do the change a while back.

Eric Wieser (Jul 19 2022 at 11:11):

But that's not the simp-normal form!

Yaël Dillies (Jul 19 2022 at 11:15):

What is it then?

Yaël Dillies (Jul 19 2022 at 11:16):

∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ f a b = c has the annoying property that docs#finset.decidable_dexists_finset won't apply to it.

Martin Dvořák (Jul 19 2022 at 11:28):

Are we now talking about a version that will not have ∃ a b together?

Andrew Yang (Jul 19 2022 at 11:36):

∃ (a ∈ s) (b ∈ t), f a b = c is syntax sugar for ∃ (a) (ha : a ∈ s) (b) (hb : b ∈ t), f a b = c.

Martin Dvořák (Jul 19 2022 at 11:36):

Yeah. So it would be still closer to the current a ∈ s ∧ (b ∈ t ∧ f a b = c) wouldn't it?

Andrew Yang (Jul 19 2022 at 11:40):

Yes. The same thing happens for functions like (α × β) → γ. In lean (or any other FP languages) we tend to write it as α → (β → γ) (called currying), which is the "wrong" grouping in your sense, but is ubiquitous.

Yaël Dillies (Jul 19 2022 at 11:48):

The problem with your approach is that it will constantly require one more pair of ⟨⟩ brackets.

Martin Dvořák (Jul 19 2022 at 13:08):

Andrew Yang said:

Yes. The same thing happens for functions like (α × β) → γ. In lean (or any other FP languages) we tend to write it as α → (β → γ) (called currying), which is the "wrong" grouping in your sense, but is ubiquitous.

I like curried functions, so I am happy with how it is used now.

Yakov Pechersky (Jul 19 2022 at 13:20):

Hopefully the tooling of our language is powerful enough that it can deal with either/any of these definitions.

Yakov Pechersky (Jul 19 2022 at 13:21):

What's the clean proof you'd like to have, and what's the clunky proof you have now?

Yaël Dillies (Jul 19 2022 at 16:33):

Eric Wieser said:

But that's not the simp-normal form!

Let me also note that:

  1. Having it my way allows us to use docs#Exists₅.imp.
  2. We don't care that much about simp normal form for definitions

Last updated: Dec 20 2023 at 11:08 UTC