RFC: delete variables

Stream: mathlib4

[Kenny Lau]

I've wanted this feature for a while, I know how to write it, basically I see a lot of cases where we want [Ring R] in one section of a file and then [Field R] in another section, but you can't delete the instance, so you either have to separate them into sections or just shadow the variables, both of which feel a bit undesirable

Proposed syntax:

import Mathlib

variable (R : Type*) [Ring R]

theorem foo : 37 = 37 := rfl

variable -[Ring R] [Field R]

theorem foo2 : 37 = 37 := rfl

[Alex Meiburg]

This is roughly what omit is supposed to do. But it has other issues

[Kenny Lau]

omit doesn't really forget it iiuc

[Kenny Lau]

oh wait, it does? hmm i remember encountering some problems earlier

[Kenny Lau]

what are the other issues you're mentioning?

[Alex Meiburg]

Kenny Lau said:

omit doesn't really forget it iiuc

Yeah, hence the "roughly". In fact, see #lean4 > omitting a type-class argument doesn't always work which is pretty much what you describe.

I think any "delete variable" feature you describe is what omit ought to be doing. Or, omit should be removed, with this variable -... syntax. But I think it's the same objective.

[Kenny Lau]

well, i guess there's nothing i can do since it's in core lean :shrug:

[Damiano Testa]

I have a vague memory that omit was intended to be the negation of include and not of variable.

[Kenny Lau]

yeah, exactly

[Damiano Testa]

So, I don't think that there is a way of unvariable a variable.

[Kenny Lau]

or at least it hasn't been written yet (as I said, I know how to do it)

[Damiano Testa]

There was a thread a while ago started by David Loeffler about this, I think. (I'm on mobile with limited search abilities.)

[Kenny Lau]

import Mathlib

namespace Lean.Elab.Command

elab "#print_vars" : command => do
  logInfo m!"{(← getScope).varDecls}"

end Lean.Elab.Command

variable (R : Type*) [Ring R]

theorem foo (x : R) : x + x = x * x := sorry

#print_vars -- "R", [Ring R]

omit [Ring R]

#print_vars -- "R",[Ring R]

variable [Field R]

#print_vars -- "R",[Ring R], [Field R]

theorem foo2 (x : R) : x + x = x * x := sorry

[Kenny Lau]

this code shows that omit is not unvariable

[Kenny Lau]

image.png

[Kenny Lau]

in fact the variables, included variables, and omitted variables are all stored separately (????)

[Kim Morrison]

This is by design. We want people to use section.

[Floris van Doorn]

Note: this is lean#5595. Consider upvote that issue.

[Kenny Lau]

@Floris van Doorn is there a way to see the most upvoted issues? (edit: nvm found it)

[Violeta Hernández]

I have to agree with Kim. I dread the PRs that would arise if we were able to carelessly add and remove variables every ten lines...

[Floris van Doorn]

There is a difference between what Lean should allow and what style Mathlib should adopt. I think section is much nicer for Mathlib, but annoying if you want to quickly add a lemma in your own project.