Could assumptions be used in `variable`?

Stream: mathlib4

[Shuhao Song]

I have a file with many lemmas using the condition (hp : p.IsHamiltonianCycle). However, in my earlier PR #15578, @Yury G. Kudryashov advised me not to use assumptions in variable.

[Johan Commelin]

If you are in the namespace Path.IsHamiltonianCycle then I think that could be an exception to the rule that Yury stated.

[Yury G. Kudryashov]

I'm afraid that the new variables algorithm will require an explicit include hp, and there was a discussion saying that we shouldn't allow include hp, only include hp in.

[Yury G. Kudryashov]

Let's ask @Kim Morrison about possible exceptions.

[Shreyas Srinivas]

why should assumptions not be placed in variable declarations?

[Shreyas Srinivas]

I have been doing this in some of my demo projects

[Shreyas Srinivas]

(not mathlib)

[Shreyas Srinivas]

also, in what ways is the new variable mechanism going to differ from the current one. I am asking before I perform some toolchain updates to know what to watch out for.

[Eric Wieser]

Yury G. Kudryashov said:

and there was a discussion saying that we shouldn't allow include hp, only include hp in.

Perhaps this should be a mathlib-only linter

[Yury G. Kudryashov]

I was doing this too before @Sébastien Gouëzel told me not to a few years ago. There are 2 reasons:

• if you have a long section, then a reader looking at the code (not at the generated HTML docs) may not realise that you have a running assumption;
• Lean 4.10.0 and newer uses a new algorithm for variable inclusion, and (hp : p < 5) won't be available in a tactic proof unless you add an explicit include.

P.S.: the new algorithm is very similar to the one Lean 3 used to have.

[Shreyas Srinivas]

Okay, but now I have another question. When is variable useful? If I have to explicitly include it in every proof, I might as well add the assumptions in the theorem statement right? My intuition for variable was, when dealing with a topic we make some ambient assumptions and those go into variable declarations.

[Shreyas Srinivas]

Also, the clutter up will get significant in many theorem statements if I have to add the same list of instances every time.

[Shreyas Srinivas]

How should one include unnamed instances?

[Yury G. Kudryashov]

I usually use something like

variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X}

theorem mythm (h : Continuous f) : True := by
  exact trivial

[Shreyas Srinivas]

I am still confused because this example seems to work without include very much like the old variable command.

[Shreyas Srinivas]

I almost never used lean3, other than porting stuff to lean4, so I have no experience with the variable command there.

[Yury G. Kudryashov]

Which example?

[Shreyas Srinivas]

I wrote this gist 2 months ago to help a PR. Currently, except some warnings about done, it works well on the web editor. It uses variable to encode assumptions throughout the namespace EFXAlloc. I think I would understand this change to variable better if I knew what would have to be changed to make it work.

[Shreyas Srinivas]

Yury G. Kudryashov said:

Which example?

The one below:
Yury G. Kudryashov said:

I usually use something like

variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X}

theorem mythm (h : Continuous f) : True := by
  exact trivial

[Yury G. Kudryashov]

This doesn't need include. Lean includes

• variables X, Y, and f, because they are mentioned in the theorem statement;
• variables [TopologicalSpace X] [TopologicalSpace Y], because they are instances and all variables mentioned in these instances are included.

[Yury G. Kudryashov]

OTOH, if you try something like

variable {f : ℝ → ℝ} (hf : Differentiable ℝ f)

theorem mythm : Continuous f := by
  exact hf.continuous

then you'll see that hf is not available in the proof.

[Ruben Van de Velde]

#15726 makes significant changes to how variable works. I suggest not investing time into understanding it until that landed

[Shreyas Srinivas]

So I guess as long as I use implicit variables, it is assumed that theorems refer to them and I don't have to include them. But if a variable uses the explicit parameter syntax like variable (hx : ...), I have to include them to use them

Yury G. Kudryashov said:

OTOH, if you try something like

variable {f : ℝ → ℝ} (hf : Differentiable ℝ f)

theorem mythm : Continuous f := by
  exact hf.continuous

then you'll see that hf is not available in the proof.

[Yury G. Kudryashov]

I'm describing the new algorithm. The current algorithm is "include everything, cleanup after we have a proof".

[Yury G. Kudryashov]

Shreyas Srinivas said:

So I guess as long as I use implicit variables, it is assumed that theorems refer to them and I don't have to include them. But if a variable uses the explicit parameter syntax like variable (hx : ...), I have to include them to use them

No, the difference is between "the variable is mentioned in the theorem statement (not proof) vs it isn't mentioned.

[Shreyas Srinivas]

Yeah I am also trying to understand what will break when the new algorithm lands.

[Yury G. Kudryashov]

E.g., you can have something like

variable {X : Type*} [TopologicalSpace X] {f : X → X} (hf : Continuous f)

theorem mythm (h : (⟨f, hf⟩ : C(X, X)) = .id) : f = id := by
  exact congr_arg DFunLike.coe h

because hf is mentioned in the statement.

[Shreyas Srinivas]

But isn't the whole point of variable not to have to repeat things?

[Shreyas Srinivas]

Yury G. Kudryashov said:

This doesn't need include. Lean includes

• variables X, Y, and f, because they are mentioned in the theorem statement;
• variables [TopologicalSpace X] [TopologicalSpace Y], because they are instances and all variables mentioned in these instances are included.

But the statement of mythm doesn't mention them at all. So are they "mentioned" transitively because f is mentioned?

[Yury G. Kudryashov]

Yes, f is mentioned, and it has the type X → Y, so X and Y are included as well.

[Shreyas Srinivas]

Is "mentioned" in a theorem transitive in the sense that if f is mentioned and f : X -> Y then X and Y are deemed to be "mentioned" in the theorem statement?

[Shreyas Srinivas]

oh right. that was a near simultaneous reply. Thanks :)

[Yury G. Kudryashov]

Lean includes (after the change)

• the minimal amount of variables needed to "understand" the theorem statement;
• all variable instances that don't use non-included variables

[Shreyas Srinivas]

okay. I am guessing this change is great because downstream theorem proofs can be elaborated in parallel since you know the full statement of upstream theorems in advance.

[Yury G. Kudryashov]

Also, in some cases a theorem in Mathlib included unneeded assumptions from variables, because a tactic like cases generalized too much.

[Yury G. Kudryashov]

See #mathlib4 > New variable inclusion mechanism for more information.