local attribute [- ...]

Stream: mathlib4

[Heather Macbeth]

Is there a way of spelling local attribute [-...] in Lean 4? I used to be able to do

import tactic.norm_num

local attribute [-norm_num] norm_num.eval_nat_int_ext

to disable a norm_num extension, this doesn't seem to work in mathlib 4 or maybe I have the wrong syntax?

import Mathlib.Tactic.NormNum.Basic

attribute [-norm_num] Mathlib.Meta.NormNum.evalPow
-- attribute cannot be erased

[Heather Macbeth]

That one's for teaching, but there are also a number of uses of local attribute [-instance] in mathlib.

[Mario Carneiro]

This seems to be spelled attribute [-foo] now; erasing is only supported locally so there is no syntax like attribute [local -foo]

[Mario Carneiro]

the reason it doesn't work for norm_num is because attributes have to explicitly opt-in to being erased and you have to write some extra code to support it. Most mathlib4 tactics don't support erasing right now

[Heather Macbeth]

Ah great. Indeed instance erasing works just fine (I guess the fact that it was local automatically is what I hadn't realised):

import Mathlib.Data.Int.Order.Basic

example {a : ℤ} {b : ℤ} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a < b ↔ a * a < b * b :=
  mul_self_lt_mul_self_iff h1 h2 -- works

attribute [-instance] Int.linearOrderedCommRing

example {a : ℤ} {b : ℤ} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a < b ↔ a * a < b * b :=
  mul_self_lt_mul_self_iff h1 h2 -- fails

[Heather Macbeth]

How hard would it be to make norm_num erasable? Is there any similar example already implemented that could serve as a model?

[Heather Macbeth]

Do you mind if I add this as an issue? (If there's no reason in principle why it couldn't be done?)

[Mario Carneiro]

Heather Macbeth said:

Do you mind if I add this as an issue? (If there's no reason in principle why it couldn't be done?)

Yes please, there is no fundamental issue with implementation. A similar example might be simp: you keep a map for erased norm_num extensions in addition to the regular map, and if the regular map produces a result, we first check the erased map to make sure the extension has not been erased, and if it is we skip it

[Heather Macbeth]

mathlib4#1308, feel free to make any corrections.

[Thomas Murrills]

@Sarah Smith reached out to me about trying this—I'm going to give it a shot, if that's alright :) I'll open a branch + PR for it and start committing!

[Thomas Murrills]

If anyone has some good simple examples of norm_num erasure (cases where something can't be proved when something is erased) for the test file, they're welcome here :)

[Thomas Murrills]

Also, for anyone familiar with the existing code: is there a reason we don't keep track of the Entry list when we use addImportedFn? Currently it returns pure ⟨[], dt⟩.

I'm a little unsure of when we actually use the list of Entrys, to be honest...

[Heather Macbeth]

Here's one:

example : 3 ^ 3 + 4 = 31 := by
  norm_num1
  with_reducible rfl

fails if you put it before the evalPow extension, succeds if you put it after.

[Heather Macbeth]

So you'd like it to fail if you disable the evalPow extension.

[Thomas Murrills]

It works! :) Up to the above details about the Entry list.

[Thomas Murrills]

Is there a way to restore an attribute after erasing it? I would have expected

attribute [norm_num] Mathlib.Meta.NormNum.evalPow

but that doesn't work.

[Heather Macbeth]

Can you mark the erasure with

attribute [-norm_num] in
lemma ....

to make it local to that lemma?

[Heather Macbeth]

Or enclose the erasure in section/end?

[Thomas Murrills]

Hmmm...I would have expected both of those to work, but neither of them do.

[Thomas Murrills]

Interestingly it doesn't complain about attribute [-norm_num] ... in, but nonetheless it doesn't work as expected. I wonder if that's something I can fix inside norm_num or if it has to do with how [-_] is elaborated...

[Heather Macbeth]

I have no idea, hopefully an expert will comment.

[Mario Carneiro]

Thomas Murrills said:

Also, for anyone familiar with the existing code: is there a reason we don't keep track of the Entry list when we use addImportedFn? Currently it returns pure ⟨[], dt⟩.

I'm a little unsure of when we actually use the list of Entrys, to be honest...

addImportedFn is responsible for setting up the initial state of the attribute after importing upstream modules (i.e. just after all the import lines). The first component of the pair is the list of entries defined in the current file, so it starts out empty. The list component is pushed to in addEntryFn, which is called when a new entry is added in the current file, and the list of entries is serialized into an array for future imports in exportEntriesFn

[Mario Carneiro]

Thomas Murrills said:

Is there a way to restore an attribute after erasing it? I would have expected

attribute [norm_num] Mathlib.Meta.NormNum.evalPow

but that doesn't work.

No, the only way to restore an erased attribute is to do it in a section and pop the scope

[Thomas Murrills]

Gotcha, makes sense!

[Reid Barton]

BTW is "erased" the official word for this? It has an unrelated, more common meaning in theorem proving/programming...

[Thomas Murrills]

I need a way to check if a name has [norm_num], though. I can't simply check if it's NormNumExt, because that doesn't account for already-erased attributes. The three options I can see are

1. get all NormNumExt nodes of the DiscrTree (yikes?)
2. add a field to the state that keeps track of active norm_nums
3. check if the name isNormNumExt by looking at the environment and check if not already erased

Which of these is best (or should I do something else)?

[Thomas Murrills]

Reid Barton said:

BTW is "erased" the official word for this? It has an unrelated, more common meaning in theorem proving/programming...

Yep: - in e.g. [-norm_num] is secretly an eraseAttr syntax node, and the functionality for erasing an attribute is given by including the field erase when registering it :)

[Mario Carneiro]

I'm okay with saying that the usage of the word "erase" in this context is dev-only though

[Mario Carneiro]

not that I have a better naming suggestion

[Mario Carneiro]

@Thomas Murrills in what context do you need to know if a name is @[norm_num] tagged?

[Thomas Murrills]

In defining the function erase

[Mario Carneiro]

to give an error message if it's not already tagged?

[Thomas Murrills]

It should throw an error if the name doesn't have [norm_num], yeah

[Thomas Murrills]

At least, patterning off existing erases

[Mario Carneiro]

what does simp do?

[Thomas Murrills]

simp carries around all of the lemma names it's using in the state, I think?

[Thomas Murrills]

My guess is that it has other reasons to do so, though

[Mario Carneiro]

oh I see, it's the lemmaNames field

[Mario Carneiro]

nope, it is used nowhere else

[Mario Carneiro]

except in a test

[Thomas Murrills]

oh! well how about that

[Thomas Murrills]

but would (3) work? it seems more lightweight

[Thomas Murrills]

plus we need to access the environment in the course of giving the erase field anyway, so it's available

[Mario Carneiro]

being a NormNumExt is technically unrelated to being a norm num extension, you could always just define a random def with that type

[Mario Carneiro]

If you want to avoid the extra state I would prefer (1)

[Mario Carneiro]

if it's a rare operation then a linear time operation over the discr tree seems fine, there is a small finite number of norm num extensions anyway

[Thomas Murrills]

Ok, nice; do you happen to know of a function to get all such nodes out of the DiscrTree or should I write it? I couldn't see it in DiscrTree.lean.

[Thomas Murrills]

(Also just to be clear the only reason I want to err on the side of avoiding the extra state is performance, which I don't have great intuition for—if it's fine to add to the state, that's probably easier, tbh.)

[Mario Carneiro]

Jannis had some DiscrTree operations in a PR to std I think

[Mario Carneiro]

std4#56

[Mario Carneiro]

you can steal the operations out of that and we can clean it up later

[Thomas Murrills]

sounds good! :) I'll leave a note.

[Thomas Murrills]

Mario Carneiro said:

Thomas Murrills said:

Is there a way to restore an attribute after erasing it? I would have expected

attribute [norm_num] Mathlib.Meta.NormNum.evalPow

but that doesn't work.

No, the only way to restore an erased attribute is to do it in a section and pop the scope

How exactly do you spell the scope pop? I was expecting maybe

namespace norm_num_erase
scoped[norm_num_erase] attribute [-norm_num] ...

but that doesn't seem to be right.

[Mario Carneiro]

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

...

end stuff
-- Mathlib.Meta.NormNum.evalPow is not erased

[Mario Carneiro]

attribute [-norm_num] Mathlib.Meta.NormNum.evalPow in
example : bla := ...

should have the same effect, if you just want to erase the attribute in one declaration

[Thomas Murrills]

Those are what @Heather Macbeth originally suggested, but neither work for some reason

section stuff
attribute [-norm_num] Mathlib.Meta.NormNum.evalPow
end stuff

example : 3 ^ 3 + 4 = 31 := by
  norm_num1
  guard_target =ₛ 3 ^ 3 + 4 = 31 -- no change; still erased
  rfl

[Thomas Murrills]

attribute [-norm_num] Mathlib.Meta.NormNum.evalPow in
example := true

example : 3 ^ 3 + 4 = 31 := by
  norm_num1
  guard_target =ₛ 3 ^ 3 + 4 = 31 -- no change; still erased
  rfl

[Mario Carneiro]

It could be an issue in how you implemented the erase function? That is how erasing attributes is supposed to work from the user side

[Thomas Murrills]

Maybe—I tried to pattern it pretty closely after existing ones, but I’ll poke around and see if I can figure it out.

[Thomas Murrills]

Update: really weird (to me): when I try to erase an imported norm_num, it works, but exhibits the above bad behavior. When i try to erase a norm_num extension defined in the same file, I get the error attribute cannot be erased—apparently AttributeImpl.erase is being called.

[Thomas Murrills]

My guess currently is that e.g. simp uses a ScopedEnvExtension whereas norm_num just uses a PersistentEnvExtension?

[Mario Carneiro]

A ScopedEnvExtension is just a PersistentEnvExtension with extra logic that has been inlined into the norm_num extension

[Thomas Murrills]

...Which I guess means that erase needs that extra logic to be inlined as well in order to work correctly? Or am I misinterpreting

[Mario Carneiro]

yes, most likely

[Thomas Murrills]

Ok, thanks, that's helpful...I think I know where to look now

[Thomas Murrills]

Hmm, I'm not totally sure the norm_num attribute does inline that extra logic yet. ScopedEnvExtension uses a StateStack which comes with pushScope and popScope functionality, but I don't see any circumlocutions for the state stack and scopes etc. in norm_num.

[Thomas Murrills]

Am I correct in thinking that it's these functions which are responsible for managing the relevant scopes when e.g. section/end occurs?

[Mario Carneiro]

yes

[Thomas Murrills]

Cool. Given that the extra logic doesn't exist yet, is it still a good idea to inline the necessary logic, or is it better to just switch to a ScopedEnvExtension?

[Thomas Murrills]

still not sure what's going on with AttributeImpl.erase, though, and I wonder if it would be magically solved by using a ScopedEnvExtension.

[Mario Carneiro]

I saw something about calling .erase on the list of erased attributes on your PR, which seems wrong

[Thomas Murrills]

That's when a norm_num extension is added (to make sure it's no longer erased). Not sure it really would ever apply, though.

[Thomas Murrills]

Also it's just the hash map .erase, not the attribute's erase

[Thomas Murrills]

It's patterned off of what SimpTheorems.addConst does

[Mario Carneiro]

that should never happen because you can't add the norm_num attribute to a definition twice

[Thomas Murrills]

Yeah, that's what I thought, but I didn't want to fail to account for some edge case I couldn't anticipate

[Thomas Murrills]

I mean, it doesn't have anything to do with solving this scoping problem, though, right?

[Mario Carneiro]

I thought you were trying to do scopes that way

[Thomas Murrills]

I don't follow—which way?

[Mario Carneiro]

by erasing things from the map

[Mario Carneiro]

which is wrong and explains the issues you were having earlier

[Thomas Murrills]

Currently I don't do scopes, is the point, I think.

[Mario Carneiro]

to answer your question from before, using ScopedEnvExtension would make sense; the reason I avoided it before was because we didn't need scopes

[Thomas Murrills]

Would it make sense to implement scopes just for the hash set erased in the state somehow, without scoping the whole state?

[Mario Carneiro]

if there is a way to implement scopes in a more lightweight way which takes advantage of the fact that norm num erasure is very rare and @[norm_num] itself can't be scoped, then that would be good too

[Thomas Murrills]

Hmm. Can I inspect the current scope?

[Thomas Murrills]

From within IO Unit

[Mario Carneiro]

no

[Mario Carneiro]

certainly not just with that

[Mario Carneiro]

all of lean's state is up in some monad's Context or State type

[Thomas Murrills]

Right, I noticed it in e.g. CommandElabM's state, iirc—I wasn't sure if IO extended it or something (or not)

[Mario Carneiro]

no it's the other way around, IO is at the very bottom of the monad hierarchy

[Thomas Murrills]

ahh

[Thomas Murrills]

Hmm. erase operates in AttrM. Is that enough?

[Thomas Murrills]

Wait

[Thomas Murrills]

Let me read that type again

[Mario Carneiro]

AttrM is CoreM, which has a decent amount of state

[Mario Carneiro]

but I think you are asking the wrong question

[Mario Carneiro]

all of an extension's state has to live inside the EnvExtension

[Mario Carneiro]

so if your attribute has a scoping effect then it needs to have a scope stack of some kind

[Thomas Murrills]

Ok, makes sense

[Thomas Murrills]

But what sort of things can implement that?

[Mario Carneiro]

what do you mean?

[Thomas Murrills]

How can I get the scope state into the EnvExtension state?

[Thomas Murrills]

Or, is that not quite how things flow?

[Mario Carneiro]

it's the type variables in PersistentEnvExtension

[Mario Carneiro]

(see the doc comment too: docs4#Lean.PersistentEnvExtension)

[Thomas Murrills]

Right, ok...so, hmm. Let's say a section or end is encountered. some pushScope or popScope occurs, right? Is that meant to reach in and affect the state somehow?

[Mario Carneiro]

hm, looks like ScopedEnvExtensions do have an extra bit of magic: src4#Lean.pushScope

[Thomas Murrills]

I saw that! I was wondering how that worked

[Mario Carneiro]

section calls that function, which checks a global list of all ScopedEnvExtensions which is pushed to in registerScopedEnvExtension

[Mario Carneiro]

so that means that even if you make a scoping-like PersistentEnvExtension you won't get a callback so you can't detect scopes

[Thomas Murrills]

I seee

[Thomas Murrills]

Hmmm. So is the best option really to turn the whole thing into a ScopedEnvExtension? Or is there some tricky way we could, I don't know, set up a separate scoped extension just for keeping track of erased norm_nums, which the PersistentEnvExtension can keep a reference to? I'm not sure if that's possible, though. It seems like the persistent state can't access any of the information needed.

[Thomas Murrills]

Unless—could the auxiliary scoped extension reach in and update a field of the persistent extension when it encountered a new scope?

[Mario Carneiro]

you still have a fair amount of control with a scoped env extension, the interface is a little different though

[Mario Carneiro]

I don't think it should be a problem to scope only what you want to

[Thomas Murrills]

Ok, neat—one thing I noticed was that addImportedFn didn't seem to have a direct analogue type-wise

[Thomas Murrills]

This is in theDescr argument to registerScopedEnvExtension

[Thomas Murrills]

I thought the OLean fields might be related, but they don't quite do the same thing...

[Mario Carneiro]

you can see how they relate in src4#Lean.ScopedEnvExtension.addImportedFn

[Thomas Murrills]

Oh I see! That looks like it makes sense. Tyvm for taking the time to explain all this. I'm going to pick this back up sometime tomorrow if I can :)

[Thomas Murrills]

Ok, I think I got this working! mathlib4#1364

[Thomas Murrills]

(A bit worried about the necessary switch from two foldlM's to ScopedEnvExtension's nested for ... in's when building the tree on import, but I don't know—maybe it's the same behind the scenes?)

[Thomas Murrills]

Also, as I'm guessing scoped extensions should be, it's now localizable—though I doubt that will get much, if any, use :)