bne_assoc

Stream: lean4

[Violeta Hernández]

I'm doing some Lean 4 programming and I stumbled across this: docs#Bool.bne_assoc is a simp lemma

[Violeta Hernández]

I don't really think this makes sense? For starters, associativity isn't the kind of stuff you really consider to be simplified one way or the other. But more annoyingly, this lemma is backwards! The Mathlib (Lean?) convention is that x * y * z means (x * y) * z.

[Violeta Hernández]

(minor note, a bit later down that file it says "coercision" instead of "coercion")

[Daniel Weber]

It's not backwards, it's in the same direction as docs#add_assoc, it just shouldn't be a simp lemma (btw, most operations being left-associative by default is a general programming thing, it's not specific to Lean)

[Kevin Buzzard]

Reminds me of the old days...

[Violeta Hernández]

Speaking of Beq jank

[Violeta Hernández]

!x == y parses as !(x == y), for whatever reason

[Violeta Hernández]

Admittedly it's not a big deal since these are logically equivalent, but it's still annoying

[Kim Morrison]

Trying out removing @[simp] from bne_assoc at lean#5390.

[François G. Dorais]

This is an ongoing issue about xor or bne for Bool. They do the same thing for Bool but they aren't actually synonymous. There are several old discussions about this on zulip and github. I can try to dig them up if needed.

Anyway, the core problem is that Bool.xor is an abbrev and therefore reducible. Because of this we can't separate Bool.xor_assoc, which makes perfect sense, from Bool.bne_assoc, which is dubious at best. The best solution is to make xor semireducible but that will require a reorganization of the Bool simp lemmas.

[Eric Wieser]

Kim Morrison said:

Trying out removing @[simp] from bne_assoc at lean#5390.

I guess this didn't succeed?

[Kim Morrison]

Yeah, it was a mess, and should be fixed by changing Bool.xor to not be an abbrev. I'm not super excited about doing that right now.