[Merged by Bors] - feat: make norm_num erasable (and scoped)

[thorimur]

As per #1308, we give norm_nums the capability to be erased. E.g.

attribute [-norm_num] Mathlib.Meta.NormNum.evalPow

This required us to switch the implementation from a PersistentEnvExtenstion to a ScopedEnvExtension so that the attribute could be erased in a section (or via attribute [-norm_num] ... in) in a way the user would expect.

This also easily lets us now make norm_num a localizable attribute. (I imagine that's a rare occurrence, but may as well—the functionality comes for free with ScopedEnvExtension, and all we have to do is not prevent it.)

The following explains in detail what changes I make, but the actual changes to the code are small. If you're reviewing this, it might make more sense just to read the code.

---

To handle erasure:

• We turn the state of the attribute into a structure and add the erased field
• We add the name field to the extension structure and give it an autoparam to capture the name of the norm_num extension at hand
• In erasing the attribute, we remove it from the state's Entrys if present, and when adding the attribute, we remove it from erased if present—the latter shouldn't ever need to happen, but simp apparently does it sometimes (but I don't know why), so I left it in there just to avoid unanticipated edge cases.
• We perform the check that the attribute can be erased by confirming that it's present somewhere in the DiscrTree and that it's not already erased. If it can't be erased, we throw an error saying that the identifier does not have the norm_num attribute, like simp does.

To switch to ScopedEnvExtension, we:

• remove exportEntriesFn, since ScopedEnvExtension performs an equivalent .toArray.reverse operation automatically.
• refactor the fields of the extension as necessary (e.g. addImportedFn to ofOLeanEntry plus addEntry, with the rest being taken care of by ScopedEnvExtension's built-in addImportedFn)
• remove the entries field from the state, since that's now taken care of through ScopedEnvExtension directly

To make it localizable, we adjust the add field when registering the attribute to:

• remove the now-unnecessary guard on the kind
• change the setEnv and addEntry to ScopedEnvExtension's add (which calls modifyEnv and addEntry behind the scenes on appropriately-scoped values)

Misc:

• norm_num traces now print the name of the extension used for the rewrite, since it's now available (whereas it wasn't before).

[thorimur]

Q's:

• In derive, should we check whether erased is empty before looping over all matched extensions, or is it fast enough to check whether the extension is erased every pass?
• Should I add more tests? (There's only one.)
• Is the inline of parts of std4#56 handled appropriately? Resolved via appropriate import.

[hrmacbeth]

@thorimur Can you please use successIfFail here, even though there's no good way to make the with_msg part work?

[thorimur]

Hmm, I'm having a bit of trouble translating the monad operation successIfFail into this context. Would a syntactic guard_target be alright? Or is admit frowned upon?

attribute [-norm_num] Mathlib.Meta.NormNum.evalPow
example : 3 ^ 3 + 4 = 31 := by
  norm_num1
  guard_target =ₛ 3 ^ 3 + 4 = 31
  admit

[hrmacbeth]

I think that's a good approach! (Also you can probably change the admit to rfl, if you want to get rid of the warning.)

[hrmacbeth]

• Is the inline of parts of std4#56 handled appropriately?

I've never personally tried this, but can you update your lake-manifest to use the Std commit associated to std4#56? (If that breaks because that PR is too old, you might need to ask the author of that PR to merge master.)

[thorimur]

• Is the inline of parts of std4#56 handled appropriately?

I've never personally tried this, but can you update your lake-manifest to use the Std commit associated to std4#56? (If that breaks because that PR is too old, you might need to ask the author of that PR to merge master.)

I'll try! I am a little wary of making all of mathlib4 depend on a non-master branch of std4, though...is that what would be happening?

(Also I should link this conversation with @digama0, just so it's visible to everyone)

EDIT: I tried, but it doesn't seem to like it enough to build. Maybe someone more familiar with lake-manifests could get it to work, though.

EDIT 2: I removed the commits to make the rebase to master work well...but that seems to have changed the timestamps of all the commits. oh well.

[hrmacbeth]

Could you clarify what these comments refer to? Are they tests which you hoped would work but don't?

[thorimur]

Writing attribute [-norm_num] ... a second time should give the error that the identifier does not have the norm_num attribute, as it has already been erased. This comment tries to say that if you uncomment those lines of code, it should (and does) give that error—I'll clarify it so that it actually says that :)

Or maybe there's a way to use successIfFail here?

[thorimur]

Clarified! I couldn't find a way to make successIfFail work, though.

[hrmacbeth]

@thorimur Another possible approach to the dependency on leanprover/std4#56: If I understand correctly, @JLimperg made this PR in order to move some DiscrTree functionality in Aesop upstream to Std. Since Mathlib already imports Aesop, maybe we already have access to it? Do the methods in
https://github.com/JLimperg/aesop/blob/master/Aesop/Util/Basic.lean
do what you need?

[thorimur]

@thorimur Another possible approach to the dependency on leanprover/std4#56: If I understand correctly, @JLimperg made this PR in order to move some DiscrTree functionality in Aesop upstream to Std. Since Mathlib already imports Aesop, maybe we already have access to it? Do the methods in https://github.com/JLimperg/aesop/blob/master/Aesop/Util/Basic.lean do what you need?

Ah, great find! Importing Aesop.Util.Basic worked like a charm. :)

[JLimperg]

With #1447, the DiscrTree functionality will move to Std.Lean.Meta.DiscrTree.

[thorimur]

With #1447, the DiscrTree functionality will move to Std.Lean.Meta.DiscrTree.

Thanks for the heads up (and the functionality)! :) I've rebased and the import has been updated.

Note: I needed to delete some experimental lake-manifest commits in order for the rebase to go through smoothly; the rebase seems to have changed the timestamps of all the commits in the web interface. I should have merged master... 🙃

[digama0]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style