Zulip Chat Archive

Stream: lean4

Topic: Theorem Names


view this post on Zulip François G. Dorais (Mar 31 2021 at 20:45):

Some time ago, there was a decision to snake_case theorems in Lean 4. That change is not complete yet but that's fine, there are more important things to do. I'm puzzled about the implications. For example, which of these is the correct Lean 4 theorem name:

theorem beq_iff_eq (a b : Bool) : a == b  a = b := sorry
theorem beq_iff_Eq (a b : Bool) : a == b  a = b := sorry
theorem beq_Iff_Eq (a b : Bool) : a == b  a = b := sorry
theorem BEq_iff_Eq (a b : Bool) : a == b  a = b := sorry
theorem BEq_Iff_Eq (a b : Bool) : a == b  a = b := sorry

Perhaps this one is tricky because of the implicit coercion, but I would still like to know. (FWIW, my fave is #3 but I'd be fine with any one.)

view this post on Zulip Mario Carneiro (Mar 31 2021 at 20:46):

I think it is 3

view this post on Zulip Chris B (Mar 31 2021 at 20:51):

I got this from an earlier post by S. Ullrich lean4_naming.png , not sure if it's still good.

view this post on Zulip Chris B (Mar 31 2021 at 20:58):

I'm not sure how that applies actually. There's a theorem succ_Eq_add_one (n : Nat) : succ n = n + 1 and one called mod_eq_sub_mod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b, the capitalization of Eq is up in the air.

view this post on Zulip Leonardo de Moura (Mar 31 2021 at 21:00):

We are still experimenting with different styles for naming theorems.

view this post on Zulip Mario Carneiro (Mar 31 2021 at 21:00):

I would like Eq to not be capitalized, but I see why it is in the current convention

view this post on Zulip Eric Wieser (Mar 31 2021 at 22:16):

What if all type names in Prop were actually lower case, using the handwavy "well these are just like functions returning a bool" argument?

view this post on Zulip Eric Wieser (Mar 31 2021 at 22:17):

Not just in lemma names, but actually rename Eq back to eq etc

view this post on Zulip Mario Carneiro (Mar 31 2021 at 22:23):

I would support that, although that means changing Bool.true back to tt so that it doesn't clash with True

view this post on Zulip Eric Wieser (Mar 31 2021 at 22:34):

I can see why tt might seem unsatisfying to a user using Lean only for data / "regular programming"


Last updated: May 07 2021 at 13:21 UTC