New variable behaviour

Stream: lean4

[Calle Sönne]

It seems that lean has some new variable behaviour (I think?), and when I updated an old PR I get an error due to this. What would be the best way to resolve it? Here is the code (and variable statement)

variable {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [IsCocartesian p f φ]

/-- Given a cocartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and two morphisms
`ψ ψ' : b ⟶ b'` lifting `𝟙 S` such that `φ ≫ ψ = φ ≫ ψ'`. Then we must have `ψ = ψ'`. -/
protected lemma ext {b' : 𝒳} (ψ ψ' : b ⟶ b') [IsHomLift p (𝟙 S) ψ] [IsHomLift p (𝟙 S) ψ']
    (h : φ ≫ ψ = φ ≫ ψ') : ψ = ψ' := by
  rw [map_uniq p f φ (φ ≫ ψ) ψ rfl, map_uniq p f φ (φ ≫ ψ) ψ' h.symm]

I think I get an error since f is not mentioned in the lemma statement itself, so f is not defined when I try calling map_uniq p f φ (φ ≫ ψ) ψ rfl in the rw statement below.

How do I deal with this in the cleanest way? Should I include the instance [IsCocartesian p f φ] in the statement, so that f will get recognized? Or is there some other way I can make f (and the instance [IsCocartesian p f φ]) get added as hypotheses?

[Patrick Massot]

You could use variable … in …. But having explicit arguments in variable is not encouraged anyway.

[Kim Morrison]

Just move [IsCocartesian ...] into the lemma statement.

[Calle Sönne]

Thanks a lot!

[Calle Sönne]

Patrick Massot said:

You could use variable … in …. But having explicit arguments in variable is not encouraged anyway.

How come? Because it makes it harder to read?

[Patrick Massot]

It makes it harder to know how to use the lemma by looking at it in the source code.

[Mario Carneiro]

you could also include f in the lemma here

[Adomas Baliuka]

Is there a writeup how the new variable command works in the docs/books somewhere?

I saw the thread discussing the Mathlib "port" but couldn't quite understand what exactly the change did.

[Shreyas Srinivas]

I am recollecting what @Yury G. Kudryashov explained last month: Basically the list of variables which are included in a theorem's statement is computed entirely from the variables mentioned in the statement and its dependencies.

[Shreyas Srinivas]

So adding [IsCocartesian p f ...] will also include the variables p and f and the variables mentioned in their declaration and so on

[Shreyas Srinivas]

What makes it different from before is that it won't include hypothesis that are only referred to in the proof.

[Shreyas Srinivas]

The reasoning is roughly that in the earlier variant, a proof had to be processed before a theorem's statement could be fully determined, and this might affect how tactics work with that theorem in downstream proofs. For example the apply t tactic needs to know which hypotheses t needs . With the new version of variable, a theorem's assumptions are known by reading it's statement alone and proofs can be elaborated in parallel.

[Tomas Skrivan]

What is the deal with the new linter warning about unused type classes?

mwe

import Mathlib

variable {I} [Fintype I] [DecidableEq I]

def sum (f : I → ℕ) := ∑ i, f i

-- linter warning: included section variable '[DecidableEq I]' is not used in 'sum_sum', consider excluding it
theorem sum_sum (f : I → ℕ) : sum f = ∑ i, f i := by rfl

-- linter warning: included section variable '[Fintype I]' is not used in 'if_eq_true', consider excluding it
theorem if_eq_true (i : I) : (if i = i then 1 else 0) = 1 := by simp

Very often I have a list of theorem where I have {I} [Fintype I] [DecidableEq I]. Only few of the theorems use [DecidableEq I] and I get bunch of linter warning that I find really annoying. Sure I could group all those theorems that need [DecidableEq I] to a separate section but they are grouped based on different criteria which is more meaningful then the requirement of [DecidableEq I].

Honestly I usually opt out with

set_option deprecated.oldSectionVars true

Is there an option to turn off the warning about unused type class instance?

[Mario Carneiro]

do you want the theorems in question to use the variables or not?

[Tomas Skrivan]

I want sum_sum to only use [Fintype I] and if_eq_true only use [DecidableEq I].

[Mario Carneiro]

AFAIK there isn't any way to really express this in the new system short of using omit or include on almost every theorem, which I find unsatisfactory

[Mario Carneiro]

in fact, the version that actually shipped doesn't even have omit and include alone doesn't help, you have to use variable ... in on every theorem instead

[Tomas Skrivan]

This is quite unsatisfactory.

Consider this

import Mathlib

variable {I} {X} [AddCommMonoid X]

variable [Fintype I] in
def sum (f : I → X) := ∑ i, f i

The type of sum is

{I : Type u_1} → {X : Type u_2} → [inst : AddCommMonoid X] → [inst : Fintype I] → (I → X) → X

The order of the typeclasses is mixed up.
I prefer either one of these two styles:

1. type binder followed with typeclasses for that type e.g. {I} [Fintype I] {X} [AddCommMonoid X]
2. all type binders first and then type class binders for those types in the same order e.g. {I X} [Fintype I] [AddCommMonoid X]

I can't easily achieve neither with the new variable command.

[Sebastian Ullrich]

There shouldn't be any change in the behavior of def

[Sébastien Gouëzel]

If few of your theorems us [DecidableEq I], the best solution is probably to remove it from the variables line and write for each of them

theorem foo [DecidableEq I] ...

[Sebastian Ullrich]

Adomas Baliuka said:

Is there a writeup how the new variable command works in the docs/books somewhere?

https://github.com/leanprover/lean4/blob/master/releases_drafts/new-variable.md