Auto include variables

Stream: lean4

[Riccardo Brasca]

Is the following behavour expected?

import Mathlib.RingTheory.RootsOfUnity.Basic
import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

open minpoly Polynomial

variable {n : ℕ} {K : Type _} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n)

theorem foo : IsIntegral ℤ μ := by
  use X ^ n - 1
  constructor
  · exact monic_X_pow_sub_C 1 (ne_of_lt hpos).symm
  · simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, eval₂_one, eval₂_X_pow, eval₂_sub,
      sub_self]

variable [IsDomain K] [CharZero K]

theorem bar : minpoly ℤ μ ∣ X ^ n - 1 := by
  rcases n.eq_zero_or_pos with (rfl | h0)
  · simp
  apply minpoly.isIntegrallyClosed_dvd (foo h h0)
  simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, aeval_X_pow, eq_intCast, Int.cast_one,
    aeval_one, AlgHom.map_sub, sub_self]

#check bar --bar ... (h : IsPrimitiveRoot μ n) (hpos : 0 < n) ...

I am a little surprised that bar now has hpos as assumption, since it is never used, now in the statement nor in the proof in the proof.

[Damiano Testa]

Didn't you use hpos on the last exact?

[Riccardo Brasca]

Ops

[Riccardo Brasca]

Mmm, indeed if I use h it doesn't, good.

[Damiano Testa]

May I interst you in the prune tactic #5062?

[Riccardo Brasca]

This came up in !4#5119, where hpos is really not used, but it shows up in the statement. Let me try to minimize.

[Riccardo Brasca]

OK, I just copied/pasted the PR. My question is not how to fix it (it is enough to write hpos in the statement of foo instead of the variable line), but this is weird, isn't it?

[Damiano Testa]

I still see that you used foo in bar, right?

[Damiano Testa]

Ah, you have fabricated your internal hpos!!

[Damiano Testa]

(Sorry, I am downloading the cache and will look at this in Lean soon!)

[Riccardo Brasca]

Exactly! In mathlib3 the thing was

include hpos

theorem foo : ... --uses hpos

omit hpos

theorem bar : ...
--if `n=0` then blah blah, otherwise use `bar`, but no need to suppose `hpos` from the beginning

[Damiano Testa]

I would go as far as saying that it is not just weird, I would consider this wrong...

[Damiano Testa]

Yes, omit/include have to be replaced by sectioning. In fact, my motivation for prune was exactly from a similar issue when porting RatFunc.

[Damiano Testa]

If you begin the proof of bar with clear hpos, then hpos does not appear in the final expression.

[Riccardo Brasca]

Ah, my understand was that Lean is now smart enough to include/not include variables in the expected way.

[Damiano Testa]

No, Lean is smart enough to use a superset of what is needed.

[Riccardo Brasca]

OK, so we should just be extra careful when porting, since in my example above bar is not anymore the mathlib3 statement, and if it not used in the file being ported (but only in later files) the problem can show up later and being quite confusing.

[Damiano Testa]

Here is where something similar happened, though it was not the first time.

[Damiano Testa]

Riccardo Brasca said:

OK, so we should just be extra careful when porting, since in my example above bar is not anymore the mathlib3 statement, and if it not used in the file being ported (but only in later files) the problem can show up later and being quite confusing.

Indeed: the issue with RatFunc was reported by Yuri porting Laurent.

[Damiano Testa]

I am hoping that using prune 0 at the beginning of proofs will mitigate this, but prune is not in Mathlib.

[Damiano Testa]

The issue that I am referring to is #4513.

[Sebastien Gouezel]

It looks like an issue with rcases and rfl: using rfl in the first branch modifies hpos to 0 < 0, so it is indeed involved in the proof then.

import Mathlib.RingTheory.RootsOfUnity.Basic

variable {n : ℕ} (hpos : 0 < n)

theorem bar : n = n  := by
  rcases n.eq_zero_or_pos with rfl | h0
  sorry
  sorry

#check bar --bar ... (hpos : 0 < n) ...

[Riccardo Brasca]

Ah, well spotted!

[Sebastien Gouezel]

As a workaround, you can clear hpos before the rcases.

[Riccardo Brasca]

The solution in this particular case was very simple (I just wrote hpos in the statement of foo), but in general this looks like a regression from Lean3, since it's difficult to realize that hpos is included, and using sections can be more annoying than include/omit (since we have to rewrite the variable line at the beginning of every section needing them).

[Damiano Testa]

The same issue exists in Lean, not just in mathlib:

variable {n : Nat} (hpos : 0 < n)

theorem foo : 0 < n := hpos

theorem bar1 : n = 0 ∨ 0  < n := by
  cases n
  . exact Or.inl rfl
  . exact Or.inr (foo (Nat.succ_pos _))

theorem bar2 : n = 0 ∨ 0  < n := by
  clear hpos
  cases n
  . exact Or.inl rfl
  . exact Or.inr (foo (Nat.succ_pos _))

#check bar1 -- bar1 {n : ℕ} (hpos : 0 < n) : n = 0 ∨ 0 < n
#check bar2 -- bar2 {n : ℕ} : n = 0 ∨ 0 < n

[Sebastien Gouezel]

I agree that the automatic inclusion of all the variables in scope (instead of the ones that show up in the statement) looks like a regression to me. It was a very nice idea to start with, but my impression is that the drawbacks are outweighing the gains.

[Damiano Testa]

So, clearly, the proof where hpos is written is the one that does not contain it...

[Riccardo Brasca]

Damiano Testa said:

So, clearly, the proof where hpos is written is the one that does not contain it...

Yeah, the real problem here is that it's very difficult to realize there's a problem...

[Damiano Testa]

Yes, I have already asked about restoring the "old" behaviour of including assumptions, but my understanding is that this is not really possible and the solution is sections.

[Mario Carneiro]

Another approach which is intermediate between the lean 3 and lean 4 methods but will mostly result in a variable set like lean 3 is to use the statement of the theorem only to determine the variable set. But we will definitely need something like include for the cases where this is the wrong answer

[Damiano Testa]

May I again interest you in prune #5062? :smile:

[Mario Carneiro]

I'm talking about default behavior

[Damiano Testa]

Ah, default pruneing would be excellent!

[Mario Carneiro]

also I think prune is too aggressive, it removes even actual variables in the definition itself

[Damiano Testa]

Somehow, in the previous discussions, I got the impression that this was not going to happen...

[Riccardo Brasca]

A related (but less important) issue is that I've seen files where the infoview is practically unusable, because at the beginning there are like 50 variables declared, and now all of them are shown, even if for each declaration only a couple are really used.

[Damiano Testa]

Mario Isn't this what happened in Lean 3: if a variable does not appear in the type, then it does not appear in context?

[Mario Carneiro]

Riccardo Brasca to be fair that was a problem in lean 3 as well

[Mario Carneiro]

Damiano Testa no, the rule was that if it appeared outside of a begin end block then it was included automatically

[Mario Carneiro]

which is a weird rule

[Damiano Testa]

The presence of lots of variables in context would be mitigated by not having the ones that do not appear in the type, at least...

[Mario Carneiro]

lots of definitions have simple types though, so you can't rely on the type alone

[Mario Carneiro]

just think of any plain programming function, the types are all very simple

[Damiano Testa]

Anyway, if you have suggestions about improvements to prune, I am happy to hear and implement them! Also, you are not required to use the tactic, but it might be useful to have the option to use it, in case you do want it!

[Mario Carneiro]

those will be hit hardest by a rule like that

[Mario Carneiro]

I'm interested in brainstorming what is actually the expected behavior here

[Damiano Testa]

I was certainly not advocating to use prune by default, but that most of the issues that have been brought up with include/omit would be at least partially mitigated by something along the lines of prune.

[Mario Carneiro]

keep in mind that there is no reason at all we can't just straight up have include and omit

[Mario Carneiro]

it was just a gamble to see whether the new variable inclusion behavior would suffice for everything

[Damiano Testa]

Honestly, I think that include/omit was better than the current system, but not ideal.

[Riccardo Brasca]

Mario Carneiro said:

Riccardo Brasca to be fair that was a problem in lean 3 as well

In Lean3 only the variables used in the statement are displayed, right?

[Mario Carneiro]

yes but you can still have a ton of things in the statement

[Damiano Testa]

Riccardo, there was also the fact that named instances were not included by default.

[Riccardo Brasca]

Sure, but then I am ready to see all of them in the infoview...

Maybe it's just that I am used to it, but I find the Lean3 behavior very natural.

[Riccardo Brasca]

Damiano Testa said:

Riccardo, there was also the fact that named instances were not included by default.

Yes, that was strange.

[Mario Carneiro]

also it is weird to me that you would have so many unnecessary variables, that sounds like bad sectioning and hard to read besides

[Damiano Testa]

How about this:

• variables that appear between theorem and := are kept, as well as implied dependencies;
• variables that are needed to make the theorem typecheck are included, as well as dependencies;
• a mechanism for including more than this, if desired.

[Mario Carneiro]

so variable (x : Nat) in example := x fails?

[Damiano Testa]

Mario, I think that the bad sectioning is a consequence of porting files that exploited omit/include and not used sections. For native Lean 4 files, I think that people would start sections when they got annoyed by the amount of available variables...

[Riccardo Brasca]

To give an example, the file I am thinking about is Mathlib.Analysis.NormedSpace.LinearIsometry, that starts with

variable {R R₂ R₃ R₄ E E₂ E₃ E₄ F 𝓕 : Type _} [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring R₄]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₁₄ : R →+* R₄}
  {σ₄₁ : R₄ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₂₄ : R₂ →+* R₄} {σ₄₂ : R₄ →+* R₂}
  {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]
  [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂]
  [RingHomInvPair σ₃₂ σ₂₃] [RingHomInvPair σ₁₄ σ₄₁] [RingHomInvPair σ₄₁ σ₁₄]
  [RingHomInvPair σ₂₄ σ₄₂] [RingHomInvPair σ₄₂ σ₂₄] [RingHomInvPair σ₃₄ σ₄₃]
  [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄]
  [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [RingHomCompTriple σ₄₂ σ₂₁ σ₄₁] [RingHomCompTriple σ₄₃ σ₃₂ σ₄₂] [RingHomCompTriple σ₄₃ σ₃₁ σ₄₁]
  [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃]
  [SeminormedAddCommGroup E₄] [Module R E] [Module R₂ E₂] [Module R₃ E₃] [Module R₄ E₄]
  [NormedAddCommGroup F] [Module R F]

[Mario Carneiro]

are those all being used in a single theorem?

[Mario Carneiro]

that's horrific

[Damiano Testa]

Mario Carneiro said:

so variable (x : Nat) in example := x fails?

Let me see how Lean 3 handled this.

[Mario Carneiro]

it's not in a begin end block

[Riccardo Brasca]

Mario Carneiro said:

are those all being used in a single theorem?

I would be very surprised if they're all needed in a single declaration.

[Mario Carneiro]

example := by exact x will fail in lean 3

[Damiano Testa]

Ok, so I would be happy with failure also in Lean 4... :upside_down:

[Mario Carneiro]

@Riccardo Brasca that's also terrible because now you have to remember what implications each of those definitions has

[Damiano Testa]

... unless there was a mechanism for detecting that a variables comes from an in, in which case you really intended it to be present. I suspect this is not possible, though.

[Mario Carneiro]

even if you could, section variable (x : Nat) example := x end isn't that unusual either

[Damiano Testa]

Ultimately, I think that if you really want a variable to appear in the signature, it is your responsibility of making it appear...

[Damiano Testa]

Mario, sure, but we already lived with that not working in Lean 3, right?

[Mario Carneiro]

We could do heuristic name resolution of the body to see whether any variables are being referred to

[Damiano Testa]

Especially since with section variable (x y : Nat) example := x end, I would not want y to appear, but this requires processing the whole proof, before realizing that y was not needed...

[Damiano Testa]

So it is not really good for writing the proof, only as an afterthought (for which the unused_variables linter is pretty good).

[Damiano Testa]

Moreover, with regards to readability of source code, having a variable defined at the beginning of a file and then passed though hundreds of lines of code with no further explicit mention is not always the best...

[Damiano Testa]

My conclusion is that Lean should aim to err on including too little, rather than too much. And the choice should be made at the beginning of the proof and not modified after the proof.

[Damiano Testa]

Right now, you only see which variables make it into the final type if you #check it after the fact.

[Mario Carneiro]

TBH it seems like the current strategy has actually worked pretty well

[Damiano Testa]

For me, once I am inside the := by ... block, I want to assume that everything that I see is going to show up in the declaration.

[Mario Carneiro]

it has got us through most of mathlib which I don't think you can say the same for the lean 3 style, there are lots of include/omit

[Mario Carneiro]

how common is it to need to use clear or prune, as a percentage of all theorems?

[Mario Carneiro]

vs include/omit

[Damiano Testa]

My experience with the porting of include/omit was that they had to be sectioned. Of course, this is probably due to the fact that the initial file was written leveraging an option that is no longer available. However, excessive assumptions in a statement that do not eventually appear in the type is somewhat annoying.

[Riccardo Brasca]

I think clear/prune are much less used than include/omit

[Damiano Testa]

Certainly prune is never used, since it does not exist in mathlib! :smile:

[Damiano Testa]

It would be interesting to see how many proofs can begin with clear ... and still produce the same declaration. My guess is that "a huge number" is the answer.

[Reid Barton]

I assume that in the future people will want to write in mathlib 4 directly rather than using mathport. I think it is fair to say we have close to no experience with what works well for this.

[Damiano Testa]

Reid, agreed. You said better what I had meant!

[Mario Carneiro]

I'm not sure which side that argument is defending Reid Barton , other than "we don't know yet"

[Mario Carneiro]

Of course the goal here is to find a strategy that requires the fewest annotations on average, and it is hard to tell how biased our current data set is by its lean 3 -> mathport provenance

[Damiano Testa]

Anyway, I think that I prefer to not have x in context here

variable (x : Nat)

theorem ex : Nat := by -- would like no `x` here

[Reid Barton]

Here is a suggestion that I haven't given too much thought, but tries to balance concision and explicitness, as well as predictability and familiarity.

• Variables are automatically included if they appear in the statement/type. Relevant instance arguments are also included according to whatever the Lean 3 rules were.
• There is a lightweight, per-declaration mechanism for including more variables. For instance, propositional hypotheses about variables will pretty much always need to be included in this way. I suggest the mechanism is to write simply (x) in the argument list to include the variable x. I would also suggest that this can be used to override the implicit/explicitness of a variable on a per-declaration basis.

[Mario Carneiro]

unfortunately this clashes with existing use of (x) in the argument use to mean the opposite thing

[Reid Barton]

what is the opposite thing?

[Mario Carneiro]

i.e. to declare a new (x) without any of the baggage (typeclass instances) of the variable

[Reid Barton]

With no type?

[Mario Carneiro]

sure, that's quite common

[Mario Carneiro]

I write {α} binders all the time

[Reid Barton]

Really??

[Reid Barton]

you can just write : _ if you want that

[Mario Carneiro]

24 hits for {α} in std4, 750 in mathlib4

[Mario Carneiro]

127 of those 750 are variable {α}

[Mario Carneiro]

it's harder to grep for occurrences of {α} where there is already a variable {α : ...} in scope

[Damiano Testa]

For me, what is most confusing is that the variables that appear in the infoview may not actually appear in the declaration. Whatever aggressive/permissive convention on variable inclusion is used, I would like to be sure that if I see a variable, then it means that it is really there, not that it may disappear after closing the goal and Lean deciding that it was not used.

[Damiano Testa]

If this rule is enforced, then new Lean 4 files will have to find their way of dealing with not declaring lots of unused variables.

[Mario Carneiro]

hm, I wasn't planning on changing that

[Mario Carneiro]

it's one of the cheaper things to do

[Damiano Testa]

For the mathport ones, well, not many are missing and they are slightly annoying but temporary.

[Damiano Testa]

Mario, changing this, will mean that a lot of the mathported files will no longer compile.

[Mario Carneiro]

?

[Mario Carneiro]

first of all, my concern is not primarily with mathported files

[Damiano Testa]

A lot of files begin with variable {X Y : Type} and then a bunch of lemmas using only X.

[Mario Carneiro]

sure and that should work

[Mario Carneiro]

that's the point of the variable command

[Damiano Testa]

Ok, so you are thinking of changing also the convention of what variables get included by default, right?

[Mario Carneiro]

yes

[Damiano Testa]

Sure, then I think that making this change and testing it with the mathported files will give a very good indication of what people expect!

[Mario Carneiro]

but no matter what you do on entry, it's still possible to post process and remove the unused variables on exit

[Damiano Testa]

I am perfectly happy (and look forward to) Lean giving me an error for having included an unnecessary hypothesis after the fact. But I do not want it to exclude one silently.

[Mario Carneiro]

you have better information on exit than on entry so one would expect you can make a better decision

[Mario Carneiro]

we're not talking about hypotheses you explicitly included

[Mario Carneiro]

the question is about auto-included variables

[Damiano Testa]

Right now, in the infoview after variable {X Y}, both X and Y are available, but if one does not get used, then it disappears in the declaration and I do not know this, unless I #check it.

[Mario Carneiro]

if you include a variable explicitly by whatever syntax, it's not going to be removed

[Damiano Testa]

Mario, maybe we mean different things by "variable"...

[Damiano Testa]

Let me write an example.

[Mario Carneiro]

by the way, in case you hadn't noticed a simpler alternative to #check is to put the cursor on the declaration name

[Mario Carneiro]

the type of the declaration shows up in the "expected type" view

[Mario Carneiro]

I understand what you are saying, maybe the variables should be shown in a different color or something

[Mario Carneiro]

or hidden

[Damiano Testa]

variable {α β : Type} {a : α}

theorem silly : α := by
  /-
  α β: Type
  a: α
  ⊢ α
  -/
  exact a

#check silly  -- silly {α : Type} {a : α} : α

[Damiano Testa]

My point is that I have β in the infoview, but not in the final declaration, nor do I get an error for it being there uselessly.

[Mario Carneiro]

I know

[Damiano Testa]

(The error would be at the conclusion of the proof).

[Mario Carneiro]

it's not really there, it's available for use

[Damiano Testa]

Sure, but removing it silently is annoying.

[Mario Carneiro]

why?

[Sebastien Gouezel]

I think I like Reid's idea that {x} in a def or theorem means "include the variable x which has previously been declared, possibly changing its binder type" and {x : Type_} means "declare a new variable x". Together with automatic inclusion of variables that show up in the statement (and their typeclasses), but only those. And no omit or include as they lead to readability issues.

[Mario Carneiro]

I would amend the first point to {x} in a def or theorem when a variable {x : ...} has been previously declared

[Damiano Testa]

Mario Carneiro said:

why?

Because it has been reported several times that Lean includes variables that can be cleared and the proof keeps working.

[Mario Carneiro]

and why is that a problem?

[Mario Carneiro]

it is quite common that you can stick a clear in the middle of a proof, delete half the variables and things still work

[Damiano Testa]

It is a problem when you apply your theorem and now you have to provide a hypothesis that was not intended to be there...

[Mario Carneiro]

that's a problem with the entry heuristic, not the exit heuristic

[Mario Carneiro]

the entry heuristic being: given the set of variables, what to put in the initial context? and the exit heuristic being: given the finalized proof body, what to put in the environment?

[Damiano Testa]

I think that the exit heuristic should be "everything that came in, plus error if something could have been removed".

[Mario Carneiro]

that sounds even worse

[Damiano Testa]

Then, I do not care what enters: it will be removed by fixing the errors on exit.

[Mario Carneiro]

how will you fix the errors?

[Damiano Testa]

By removing unnecessary hypotheses.

[Damiano Testa]

Like how I remove the "unused_variables" issues.

[Mario Carneiro]

but these are auto-included variables

[Mario Carneiro]

you didn't write syntax to include them in the first place, the entry heuristic decided to include them

[Damiano Testa]

If they had been sealed in a section they would not have entered, right? So, the answer is to use a section.

[Damiano Testa]

This is what is happening now anyways, but there is no certainty about what comes out after the proof. Sometimes the assumptions that lean chooses are correct (very often), sometimes, they are not (rare, but does happen).

[Mario Carneiro]

This will have a very high failure rate on mathlib

[Mario Carneiro]

Can you give an example where the behavior is undesirable?

[Damiano Testa]

I agree, so this should be disabled on mathlib, but I think that it would be an improvement for new files over the current system.

[Damiano Testa]

The one at the beginning of this thread.

[Damiano Testa]

The hpos assumption making it in the declaration, when it was not needed, nor wanted.

[Mario Carneiro]

that's the entry heuristic failing

[Mario Carneiro]

not the exit heuristic

[Damiano Testa]

You can also say that it is the exit heuristic: the variable was not used, so why did it stay?

[Mario Carneiro]

the variable was used

[Mario Carneiro]

it was used by cases / induction

[Mario Carneiro]

rcases in this case I guess

[Mario Carneiro]

because those tactics generalize everything in the context

[Mario Carneiro]

so if the entry heuristic puts too many things in the context, these tactics pick it up and now the exit heuristic can't remove them

[Mario Carneiro]

by the time you run cases on the bigger context it's already too late

[Damiano Testa]

Sure, this is then an issue with the entry heuristic. And I can measure this by looking at the context and being certain that everything that I see when starting a proof will be there at the end. Otherwise, I might think that hpos has not been touched explicitly, so it will disappear and then be surprised when it doesn't.

[Damiano Testa]

I think that "include everything" and "purge out as much as I can" should not be used together. I prefer "conservative inclusion" and "warning on excludability" as policies.

[Damiano Testa]

However, it is also true that the theorems that entering mathlib4 now have a lot of assumptions appearing in context, because they came from mathported files, where those assumptions were not in context.

[Damiano Testa]

I imagine that, for native Lean 4 files, this would have been mitigated beforehand by using sections more profusely.

[Mario Carneiro]

The statement "everything I see when starting a proof will be there at the end" is saying "the exit heuristic is a no-op"

[Mario Carneiro]

which is not the current situation

[Damiano Testa]

I know: right now, I do not know if what I see in context will survive the end of proof or not. I am not very happy about this behaviour.

[Mario Carneiro]

but let's say that the entry heuristic was smarter but the entry heuristic was still "remove unused things"

[Mario Carneiro]

so you see a smaller context at the beginning of the proof but some things might still be removed later

[Damiano Testa]

I would still prefer "remove unused things and tell me about it!".

[Mario Carneiro]

and let's also say that the variables that the exit heuristic would remove are hidden from the context

[Mario Carneiro]

so now you can't see them at all, problem solved

[Damiano Testa]

So I can go back and remove them explicitly. Otherwise, I do not know if something that I was expecting not to be used, like hpos above, really has been removed or not.

[Mario Carneiro]

but if you refer to them then oops I guess they are used and now they appear in the context

[Damiano Testa]

Partially better, but "touching" in the case of hpos meant using a tactic that did it under the hood...

[Damiano Testa]

So, true, they appear in context after I use cases: better than never showing up, but still very sneaky...

[Mario Carneiro]

I think these variables can be marked in such a way so as to tell tactics to ignore them

[Mario Carneiro]

this already exists

[Yaël Dillies]

Mario Carneiro said:

but if you refer to them then oops I guess they are used and now they appear in the context

So if I use induction I will suddenly get a bunch of variables appearing in my context? That will be very surprising behavior.

[Yaël Dillies]

Oh I guess marking them as "for manual consumption only" fixes my concern.

[Damiano Testa]

I agree with Yael: I think that taking the extra effort of making sure that what you see at the beginning of a proof is what comes out of it is part of the game. Heuristics can help with what you get to begin with, but messing with it after/during the proof is very doubtful.

[Mario Carneiro]

you aren't actually adding or removing variables here, that would be almost impossible. You are just hiding and unhiding variables that were always there, and/or telling tactics to ignore those variables

[Reid Barton]

Including variables in the type of the theorem statement or not based on the proof is just clearly the wrong thing to do. Imagine you have some theorem with an expensive proof and so for development purposes you temporarily replace the proof by sorry. Now the rest of the file cannot type check because the theorem type was changed to omit some arguments?

[Damiano Testa]

Sure, I am happy to have every variable ever created in mathlib being imported invisibly and unusably by any proof and then not showing up in the declaration. For me, this counts as not including.

[Mario Carneiro]

I actually agree with that @Reid Barton , that's part of why I dislike variables to begin with

[Mario Carneiro]

but it also seems likely to me that when you use variable in def it will almost always be in the body and not the type

[Mario Carneiro]

then again, maybe programming just doesn't use variable

[Reid Barton]

Likewise if I am proving a theorem T and I decide to split off some of the work into a lemma L to be proved later, then I want to make the proof sorry for now (because maybe the lemma statement is not quite right for my purpose anyways). Then I will need to jump through some hoops anyways, to make sure that L takes the specific hypotheses needed for it to be provable, even though they are obviously not used yet.

[Yaël Dillies]

I am just going to state that in the immense majority of cases we only ever care about variables that are used in the type of a declaration, so I think completely ignoring what comes after := is a good heuristic. That also means restoring include/omit.

[Damiano Testa]

I can live with different conventions on what to include/exclude between def and theorem, but I think that variables in the infoview that disappear from the final declaration leads to issues.

[Mario Carneiro]

here's a programming example from lake:

namespace Module

/-- Build info for the module's specified facet. -/
abbrev facet (facet : Name) (self : Module) : BuildInfo :=
  .moduleFacet self facet

variable (self : Module)

abbrev imports            := self.facet importsFacet
abbrev transImports       := self.facet transImportsFacet
abbrev precompileImports  := self.facet precompileImportsFacet
abbrev leanBin            := self.facet leanBinFacet
abbrev importBin          := self.facet importBinFacet
abbrev olean              := self.facet oleanFacet
abbrev ilean              := self.facet ileanFacet
abbrev c                  := self.facet cFacet
abbrev o                  := self.facet oFacet
abbrev dynlib             := self.facet dynlibFacet

end Module

[Sebastien Gouezel]

We don't need include/omit if we follow Reid's suggestion as in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Auto.20include.20variables/near/366763546

[Yaël Dillies]

Or maybe it's desirable to have different elaboration procedures for def/abbrev/structure/class vs theorem/lemma?

[Mario Carneiro]

most of the examples I am finding in lean core are in types or typeclasses

[Mario Carneiro]

oh also this trick

variable {α} (ctx : Context α) (builtin : Bool) in
def compileEmbeddedParsers : ParserDescr → MetaM Unit
  | ParserDescr.const _                => pure ()
  | ParserDescr.unary _ d              => compileEmbeddedParsers d

[Damiano Testa]

Maybe we should have a set_option math and set_option programming...

[Mario Carneiro]

using variable like this means you don't have to refer to them in recursive calls

[Damiano Testa]

I think that for math theorems, having to go the extra mile to include a variable that is not present in the type, means that almost always you will not need to do the extra work.

[Reid Barton]

Wait why does that recursive example work?

[Reid Barton]

Is there such a thing as variable [...] in section [...] end?

[Mario Carneiro]

I don't think that works

[Mario Carneiro]

section would be read as a single command so you get section variable [...] section end [...] end which... seems wrong?

[Mario Carneiro]

actually it kinda works :upside_down:

[Reid Barton]

Are there like... really big parentheses I can use?

[Mario Carneiro]

what's the application?

[Mario Carneiro]

mathlib defines big parentheses by the name stop_at_first_error

[Reid Barton]

Basically parameters. But probably I am misunderstanding that recursive example.

[Mario Carneiro]

I think so

[Mario Carneiro]

here we are using variable [...] in to scope just over the def which is recursive

[Mario Carneiro]

the trick is that this is the new way to write variables "left of the colon"

[Mario Carneiro]

because the recursive call doesn't have to refer to the variables (in fact it cannot)

[Mario Carneiro]

so they are fixed parameters

[Mario Carneiro]

variable (a : Nat) in
def add : Nat -> Nat
  | 0 => a
  | b + 1 => add b + 1

lean 3 style

[Mario Carneiro]

compare:

def add (a : Nat) : Nat -> Nat
  | 0 => a
  | b + 1 => add a b + 1

[Reid Barton]

Can I write say a sequence of ten (non-mutually recursive, just ordinary) definitions after variable [...] in?
This is how Agda anonymous modules work.

[Mario Carneiro]

no, the in scopes after only one definition, that's the point

[Mario Carneiro]

if you want to scope over ten definitions just use section normally

[Reid Barton]

But then I don't get parameter-like behavior.

[Mario Carneiro]

section
variable (a : Nat)
def add : Nat -> Nat
  | 0 => a
  | b + 1 => add b + 1

def mul : Nat -> Nat
  | 0 => 0
  | b + 1 => add (mul b) a
end

[Mario Carneiro]

no, the reason for this behavior is because the auxiliary local variable add in the definition of add has the type Nat -> Nat

[Mario Carneiro]

the actual constant still has the type Nat -> Nat -> Nat which is why in the next definition you refer to it with two args

[Reid Barton]

ok, I think I see. Because add in its own definition is not a real reference to a definition anyways, it is something that will be processed by the equation compiler.

[Mario Carneiro]

if you make them all part of a mutual block, possibly you will get the desired behavior

[Mario Carneiro]

variable (a : Nat) in
mutual
def add : Nat -> Nat
  | 0 => a
  | b + 1 => add b + 1

def mul : Nat -> Nat
  | 0 => 0
  | b + 1 => add (mul b)
end

there's your big parentheses

[Mario Carneiro]

note that this is a "non-mutual mutual block", the equation compiler will notice that the definitions are not an SCC and compile them in order

[Johan Commelin]

$\Bigg(\text{hello big parentheses}\Bigg)$

[Reid Barton]

But I guess other random stuff will not quite work, e.g., if add has @[simp] then maybe simp will not apply it by default in mul because the declaration is not actually added to to the environment yet

[Damiano Testa]

On the topic of the "entry heuristic", I think that most math theorems would work if you begun their proof with prune 0.

[Mario Carneiro]

most meaning 99%? Because that's still thousands of lines to fix

[Damiano Testa]

No, I think that for the mathported files there is no hope to get something good...

This would be for the native Lean 4 files.

[Damiano Testa]

The point is that while porting, people worked around the different conventions in Lean 3/4 and did a great job at it!

[Mario Carneiro]

I don't see why it would be any different for non-mathported files

[Damiano Testa]

But the juggling of variables that had to be done for porting, should not be done for new files, I think.

[Damiano Testa]

Well, as you pointed out, for the vast majority of files, there would be no difference. But there will always be the odd lemma that uses an unusual hypothesis...

[Damiano Testa]

The way of dealing with these outliers will be different in mathported files and in native ones, I think.

[Mario Carneiro]

I think the fact that they are mathported files matters less than the fact that they are pre-existing files

[Mario Carneiro]

you would have to fix any errors up-front

[Damiano Testa]

Sure, I meant files that were written with a different convention in mind.

[Mario Carneiro]

What convention change?

[Damiano Testa]

Also, I do not think that a new heuristic will result in less work than the current one. Just that it would be more natural.

[Damiano Testa]

The convention between what you see in the infoview and what appears in the final declaration.

[Mario Carneiro]

I would like a heuristic that results in less work

[Mario Carneiro]

that's not a convention

[Damiano Testa]

I think that both conventions work well on the majority of files, so less work is really referring to very few situations.

[Mario Carneiro]

changing what you see in the infoview without changing what makes a lean file valid is easy

[Damiano Testa]

Maybe convention is not the right word, but in Lean 3 I expect that everything that I see in the infoview makes it into the declaration, whereas what I see in the infoview in Lean 4 is subject to unknown pruning.

[Mario Carneiro]

I think that is the least important problem to solve

[Damiano Testa]

Maybe it is not important, but I do like to have some certainty about what comes out as a hypothesis in a declaration.

[Mario Carneiro]

That is to say, maybe it should be discussed separately

[Damiano Testa]

And I prefer to know it beforehand, possibly of course including stuff that I can later omit, rather than having to wait until the end of the proof and then re-inspecting it after the fact.

[Damiano Testa]

How hard would it be to have various versions of prune being auto-inserted in a random selection of theorems and seeing how many still typecheck?

[Damiano Testa]

(I am saying prune simply because it is already there. Any other heuristic for removing assumptions would be good.)

[Damiano Testa]

E.g., you said above "99.9%": this was probably a guess. Can we maybe have a montecarlo approach for checking this proportion?

[Damiano Testa]

For instance, how hard it is to make theorem ... := by be parsed as theorem ... := by prune; and then seeing what percentage of proofs break?

[Damiano Testa]

(Note that prune is the most conservative. I would argue that prune 0, the least conservative, would still work for a good proportion of theorems. I would also expect the difference between prune and prune 1 to be really small.)

[Mario Carneiro]

actually if I were to hazard an actual guess I would say something closer to 95%, and heavily biased to certain kinds of files

[Mario Carneiro]

a.k.a. "tons of breakage"

[Mario Carneiro]

it is fairly easy to do that test, just override theorem

[Damiano Testa]

This means adding a macro for theorem?

[Kyle Miller]

Damiano Testa said:

May I interst you in the prune tactic #5062?

This has been a long topic so maybe I missed where it might be discussed, but I'm not sure how prune would help with this problem. I'd guess that most of the time the additional hypotheses involve variables that appear in the goal. For example, even with a simplification of the motivating example, prune will keep h:

variable (n : Nat) (h : 0 < n)

theorem thm : n = n := by
  prune
  -- h is still a goal
  rcases n.eq_zero_or_pos with (rfl | h0) <;> rfl
#check thm
-- thm (n : ℕ) (h : 0 < n) : n = n

Dealing with prune n for varying n isn't a general solution either because it takes manual intervention, and also I don't think you can use this number to delete exactly the right things (or really be able to predict what will happen for varying n).

[Damiano Testa]

Kyle, yes, I had intended prune with a different goal in mind, but I think that it can be adapted to a solution to the current problem.

[Damiano Testa]

(that is, when a solution is agreed upon!)

[Kevin Buzzard]

The reason I would be against banning variable completely is that sometimes you have parameters like a prime number p and variable {p : Nat} [fact p.prime] and there are files when you'd need this in every declaration if you didn't have variables. I would definitely be able to adapt to just writing {p} in every declaration but I wouldn't want to write much more.

[Mac Malone]

Mario Carneiro said:

then again, maybe programming just doesn't use variable

In programming, one of the most common uses of variable in a section is to equipped a monad m with all the relevant operations (e.g., [Alternative m], [MonadLog m], [MonadEnv m], etc.) for whatever set of monadic combinators is being written.

[Riccardo Brasca]

To give an example of the fact that this can go wrong, look at docs#Fin.card_Ioi and its mathlib3 version docs3#fin.card_Ioi. The mathlib4 version has a sporious (b : Fin n) that has auto included for some reason. Since the result is only used in a later file, nobody noticed it.

[Sebastien Gouezel]

Same problem in several lemmas in this file!

[Sebastien Gouezel]

e.g. docs#Fin.map_valEmbedding_Ici, docs#Fin.map_valEmbedding_Ioi, docs#Fin.card_Ici, docs#Fin.card_fintypeIci, docs#Fin.card_fintypeIoi.

[Riccardo Brasca]

Yes, I am fixing those

[Riccardo Brasca]

#5382

[Alex Keizer]

Kevin Buzzard said:

The reason I would be against banning variable completely is that sometimes you have parameters like a prime number p and variable {p : Nat} [fact p.prime] and there are files when you'd need this in every declaration if you didn't have variables. I would definitely be able to adapt to just writing {p} in every declaration but I wouldn't want to write much more.

This seems like an interesting middle road, we keep variable to declare the type and possibly associated typeclasses, and the for each definition/theorem we explicitly opt in to which variables we want by writing {p x y}, but we then don't have to repeat the types nor typeclasses. This gets rid of a lot of the implicit magic (which isn't perfect, and hard to detect when the magic went wrong), but means we don't have to repeat too much.

[Alex Keizer]

I'm currently having some issues with variables, because I have a lot of fairly trivial theorems over bitvectors, where some mention just two variable xs ys : Bitvec n and others also have a third variable zs : Bitvec n.

I could section these by the number of variables used (and that is what I now have to do as a work-around), but it's much nicer to section them by actual semantic content, so that theorems about similar operations are grouped.

However, if I have just variable (xs ys zs : Bitvec n) for the whole file, and then do an induction xs, suddenly the third variable gets included in theorems which don't need it.

[Sebastien Gouezel]

As a workaround, you can clear zs before the induction line.

[Riccardo Brasca]

Should we open a Lean issue? At least about rfl in rcases, that I suppose changes the value of all the variables of the appropriate type and so include all of them.

[Kevin Buzzard]

I think that Alex' example above is a perfectly reasonable issue, so sure open an issue (if there isn't one already)

[Jireh Loreaux]

I really like Reid's (sorry, I got this wrong the first time) suggestion above as an entry heuristic. Lean could then still look at the body and omit unused type classes from the declaration upon exit, but omitting implicit or explicit hypotheses would result in an error. In this case, it would be nice if we could also have some sort of linter which made sure each declared variable is actually used somewhere in the file.

To really flesh this out, this is a behavior I think might be reasonable, but I understand it is a pretty significant departure from what we have currently (although, as we have been discussing, what we have currently is suboptimal).

The entry rule is something like this:

1. Types explicitly referenced in the declaration (allowing for the (α) or {α} to be an update to an existing variable instead of shadowing) are obviously entered.
2. Any type class in a variable declaration all of whose explicit arguments are already included get added to the context. (Maybe only explicit arguments which are not outParams are necessary to get included; the effect of this change in the above is that myF' would behave like myF.)
3. Type classes with an explicit argument not referenced are excluded.

I'm not sure exactly what the Lean 3 entry rule was, but it seems like it was a lot like the above. The key distinction I think is the allowing for forced inclusion of predeclared variables with (α) or {α}`

The exit rule is still looks at the body and deletes unused things.

variable {α β F : Type _} [Ring α] [StarRing α] [CommRing β] [Module β α] [RingHomClass F β α]

def myRingCopy (α) : Ring α := by -- only using tactic mode to show local context at various positions
  /-
  α: Type ?u.551797
  inst✝¹: Ring α
  inst✝: StarRing α
  -/
  exact ‹Ring α›

#check myRingCopy
-- Unitization.myRingCopy.{u_1} (α : Type u_1) [inst✝ : Ring α] : Ring α
/-  The `StarRing α` instance is omitted per the exit strategy, and note that even though `α` was declared as
an implicit variable, because of the `(α)` it is changed to explicit for the declaration. -/

example : Ring α := ‹Ring α› -- succeeds and has the same type signature as `myRingCopy` except `α` is implicit.

example {α : Type _} : Ring α := by
  /- local context only contains `α`, no instances because here we are shadowing the original `α` with `: Type _`.
  α: Type ?u.551783
  -/
  sorry

def myF {α β} (f : F) : F := by
  -- *all* the declared `variable`s are in context, because `α β F` are all mentioned, and hence the type classes
  -- depending on them.
  exact f
/- because most everything was unused, it all gets deleted (except for `α β f F` because they were all explicitly
declared, but now we get an unused variable warning as usual on `α β` -/

def myF' (f : F) : F := by
  -- only `F` and `f` are in context
  exact f

lemma my_add_comm (x y : β) : x + y = y + x := by
   /- context contains `CommRing β`, but crucially, not `Module β α` because `α` was never mentioned -/
  exact add_comm x y

-- at some point (maybe only with `#lint`) there is a liner error because the declared `[StarRing α]` variable
-- wasn't used anywhere.