Theorem Names

Stream: lean4

[François G. Dorais]

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.)

[Mario Carneiro]

I think it is 3

[Chris B]

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

[Chris B]

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.

[Leonardo de Moura]

We are still experimenting with different styles for naming theorems.

[Mario Carneiro]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Mario Carneiro]

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

[Eric Wieser]

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