Should boolean `or_assoc` be a `simp` lemma?

Stream: mathlib4

[Kevin Buzzard]

In mathlib3, bor_assoc is a simp lemma; in core Lean 4 it's not. [Edit: actually what I mean here is "it's not tagged @[simp] when it's declared; I realise I don't know how to check if something is a simp lemma in Lean 4, #print no longer seems to tell me] Do I leave it as not a simp lemma? Edit: same question for band_assoc.

Random remark: boolean or is left associative; proppy or is right associative.

[Kevin Buzzard]

PS why the heck does this work?

example : ∀ (a b c : Bool), ((a || b) || c) = (a || (b || c)) := by simp only

What does simp only do in Lean 4? [Oh -- got it -- it uses decidability]

PPS

example : ∀ (a b c : Bool), (a || b) || c = a || (b || c) := by simp only

also works but it doesn't say what you think it says ;-)

[Scott Morrison]

Do we need a new command to ask if something is a simp lemma? This is essential information about the API.

[Scott Morrison]

I'd suggest preserving the @[simp] status of lemmas during the port as much as possible, even if that means adding simp attributes in mathlib4 to things defined in core. Anything else is a recipe for confusing proof failures later.

[Kevin Buzzard]

So #print is supposed to no longer work?

[Kevin Buzzard]

For the lemmas which weren't simp in lean 4 but were in lean 3, the linter complains that simp can already prove them, because lean 4 simp seems to use decide and decide can prove all the standard bool lemmas

[Scott Morrison]

It's become a bit more complicated in Lean 4, because each attribute is responsible for tracking itself, and while I think there was a proposal to have some uniform mechanism for looking up attributes, as far as I know it hasn't happened .... ? Thus for any given attribute one could teach #print to show it (and if this were to happen for any as a one-off, it should be simp), but perhaps there isn't a general mechanism.

[Scott Morrison]

I heard from Leo and/or Gabriel that they will probably change the flag that controls whether simp uses decide to false by default. I guess we want a decision on this sooner rather than later.

[Scott Morrison]

I tried disabling setting the default to decide := false (although turning it back on in simp_arith), but I'm running into the problem that simp! leaves True behind as a goal sometimes, and I'm not sure why.

[Mario Carneiro]

I intend to make #print work eventually, this will require a new subsystem in lean 4 to manage "attribute delaborators"