Zulip Chat Archive

Stream: mathlib4

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


Kevin Buzzard (Oct 21 2022 at 16:48):

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 (Oct 21 2022 at 16:54):

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 (Oct 23 2022 at 21:52):

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

Scott Morrison (Oct 23 2022 at 21:53):

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 (Oct 23 2022 at 22:14):

So #print is supposed to no longer work?

Kevin Buzzard (Oct 23 2022 at 22:15):

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 (Oct 23 2022 at 22:16):

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 (Oct 23 2022 at 22:17):

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 (Oct 24 2022 at 00:36):

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 (Oct 24 2022 at 03:26):

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


Last updated: Dec 20 2023 at 11:08 UTC