variable!

Stream: mathlib4

[Scott Morrison]

!4#3162 adds the long-dreamed-of feature:

variable! [Module R M]

meaning the same thing as:

variable [Semiring R] [AddCommMonoid M] [Module R M]

(Not this is only available as a variant of variable: you can't use this inline in a declaration.

The question is whether to allow this syntax in committed code. It has a variable!? mode that gives a "Try this:", so it is easy to remove, either immediately or later if we change our minds.

Pros: It's lovely, and avoids giant incantations to summon objects.
Cons: Maybe it is fragile or buggy in some way that won't appear until it is used widely, and creates an extra place where confusing typeclass problems can arise.

Jireh pointed out that it could cause strange problems if someone generalizes a typeclass to only require weaker typeclass hypotheses, and this then changing the effect of every downstream variables!, possibly breaking proofs. It's possible this is a feature, not a bug, however, as it forces you to consider whether downstream generalizations are possible too!

[Scott Morrison]

/poll Should we allow variable! in committed mathlib4 code?

[Eric Wieser]

A more conservative option would be to wait for usage feedback from variable!? (which is certainly a good thing) to see what traps we might be falling into

[Kyle Miller]

Another con for variable! is that its mechanism relies on typeclass inference failure to decide when to add new instance arguments, and failing is not a particularly fast.

[Kyle Miller]

Maybe a more conservative middle ground is to have a version that keeps both the original binders passed to variable! along with the cached full variable command, and then you could delete the cached version to get it to regenerate.

[Eric Wieser]

How is that different to asking a user to write !? to regenerate?

[Yury G. Kudryashov]

So, variable!? should produce something like this?

-- variable! [Module R M]
variable {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M]

[Yury G. Kudryashov]

The difference is that we can see both "short" and "long" verisons in the output.

[Eric Wieser]

I don't think we want it as a comment, because then it can (and will) go out of sync

[Kyle Miller]

Yeah, or maybe something like

variable! [Module R M] => {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M]

since variable! can still issue the variable command

[Scott Morrison]

I really like the general approach of having Try this instructions give you something that preserves the original invocation.

[Scott Morrison]

I especially like Kyle's proposed syntax as restoring the original call is just removing a suffix.

[Yury G. Kudryashov]

After some time, if we're satisfied with the variable! output, then we can drop the => parts.

[Eric Wieser]

Is CI (maybe just the linter) still responsible for checking that the thing before the => actually produces the thing after?

[Kyle Miller]

Do you mean drop the part before the => or after it Yury?

[Yury G. Kudryashov]

Once a week?

[Yury G. Kudryashov]

I mean after.

[Yury G. Kudryashov]

(If variable! is also fast)

[Kyle Miller]

The point of this => clause is to cache the result, since typeclass inference failure isn't very fast

[Kyle Miller]

though maybe someone can come up with a better algorithm than relying on inference failure

[Yury G. Kudryashov]

Then we don't drop it.

[Eric Wieser]

Kyle, were you responding to me, Yury, or both of us?

[Kyle Miller]

I was just elaborating on "then we can drop the => parts"

[Kyle Miller]

Re your point about CI, that issue was something I was going to bring up too, making sure the expansion is still accurate

[Kyle Miller]

Do you have an idea how that would look? Does it seem plausible that you could write a linter for this?

[Kevin Buzzard]

How do I say "let R be a commutative ring and let M be an R-module"? I have no interest in semirings.

[Yury G. Kudryashov]

If you want M to be an additive commutative group, then you still need to tell all the arguments.

[Eric Wieser]

But, as the PR shows, you can also make a VectorSpace alias

[Eric Wieser]

My fear is that using such an alias just creates more work when generalizing results to modules though

[Kyle Miller]

@Kevin Buzzard I've been thinking of how to get that to work, where you specify the "root" classes you care about, but it's not there yet

[Kevin Buzzard]

I was about to reply "ok then can I override the defaults?" but then I realised that a line overriding the defaults would be just as long as a line typing it the old way :-)

[Kyle Miller]

Eric Wieser said:

My fear is that using such an alias just creates more work when generalizing results to modules though

On the plus side, the VectorSpace alias does not work as a variable to a theorem (sort of intentionally), so this generalization problem is localized to variable commands

[Eric Wieser]

I think having the expansions available after a => as discussed above makes the concern moot anyway

[Eric Wieser]

(also, I think I found a trap, variable!? (A : ℕ → Type) [∀ i : ℕ, Module R (A i)] [∀ i : ℕ, Algebra S (A i)]. See GitHub for the output)

[Kevin Buzzard]

Well we could always go back to semimodules over semirings and have modules over rings ;-)

[Mario Carneiro]

One reason I am wary of variable! alone in code is that it makes it very hard to determine the actual statement of a theorem by looking at lean code. You would basically have to do typeclass inference in your head, where the instances themselves might be declared by variable! and hence you would need to read who knows how much of the library. I think it is broadly going against the spirit of the "no global inference" rule that leads to def and theorem having a type that can be elaborated separately from the body

[Mario Carneiro]

Ideally, I would like this effect to be a general purpose code action whenever a typeclass problem fails: just suggest to add a variable in the variables line or the function args with the assumption (although I can also imagine this causing a lot of nonsensical assumptions in newbie questions)

[Kevin Buzzard]

I think that this objection is spurious from a mathematical point of view because we all know what VectorSpace k V entails.

[Kevin Buzzard]

Also, it's no less readable than variable [AddComnGroup M] 300 lines earlier (which IIRC you don't like either :-) )

[Thomas Murrills]

Is there a reason you can’t simply mouseover the def to read off what instances get used (instead of doing typeclass inference in your head)? (This doesn’t address the ‘separation of elaborations’, though)

[Mario Carneiro]

I'm talking about reading lean code without lean

[Mario Carneiro]

e.g. on github

[Mario Carneiro]

which, I know, is a lost art

[Mario Carneiro]

it's obviously a balancing act how much to actually make this practically doable vs just putting all our eggs in the "IDE support" basket

[Mario Carneiro]

I think that it should be more or less possible to understand theorem statements by reading the file without assistance, modulo typeclass instance arguments on things like +

[Thomas Murrills]

Hmm, yeah, definitely a trade-off. I like variable! … => … syntax: it exposes what you really want while not hiding what’s really happening. (Well, at the whole-file level, in any case, if not at the definition level—but the existence of variable does break total legibility at the definition level anyway.)

[Mario Carneiro]

(which BTW is why I prefer autoImplicit over variable)

[Mario Carneiro]

variable! ... => ... does solve this issue, but it also seems to just be a more verbose version of variable

[Mario Carneiro]

a self-replacing variable! would be just as good, except that it doesn't react to upstream changes to what variable! would have inferred

[Thomas Murrills]

Imo => has some advantages because it’s

1. more legible (an unstructured variable followed by a dozen instances is, to me, an obstacle to plaintext understanding; with => we can immediately skip the rhs reading left-to-right, saying “oh, okay, that’s what we want” as soon as we see the lhs)
2. automation-supporting over upstream refactors, as you mentioned; not only does it error and alert you (at some point), but it also lets you re-run the inference for what you want and complete the refactor more easily

[Thomas Murrills]

I guess if you wanted to boil what I like about it down to slogan it’d be something like “reflecting intent losslessly”.

[Jireh Loreaux]

(FYI: I added an option to the poll, in case those who already voted want to have a second opinion.)

[Johan Commelin]

@Mario Carneiro The amount of lines of variable incantations that you need to get a smooth vector bundle on a complex manifold is really unwieldy. I think it hampers readability and having a variable! version would actually be very helpful there.

[Kyle Miller]

If you want to try this out, it's now in mathlib as the variable? command, once you do import Mathlib.Tactic.Variable.

It's set up where variable? ... suggests variable? ... => ..., where the binders after the arrow are the expanded version, and the variable? command checks that the expanded version is indeed the expanded version. This way you can either delete the ? ... => part to get a plain variable command or edit what's before the => and then regenerate the expanded version. In all cases you can see from the source code exactly what's been inferred.

[Johan Commelin]

Can we make import Mathlib.Tactic.Variable available a.e. by some early import? Seems pretty harmless.

[Kyle Miller]

Yeah, it could be added to Mathlib.Tactic.Common. I didn't do it in this PR because the test file imports a good amount of algebra, which all imports this module, and I didn't want to recompile everything while developing it.

[Jireh Loreaux]

I want to know which files in mathlib have measure zero, and which (if any) are non-measurable. :laughing:

[Patrick Massot]

Mathlib/Data?

[Eric Rodriguez]

I see in another thread that that Kyle knows about the Type* bug; I can't seem to find a bug report on the github - is it worth doing so? It'd be nice to get it fixed to try and make my FunLike work simpler.

A #mwe:

import Mathlib.Tactic.Basic
import Mathlib.Tactic.Variable

class foo (β : Nat → Sort*) [CoeFun Nat (fun _ ↦ ∀ a : Nat, β a)] where

variable? {β : Sort*} [i : foo fun _ ↦ β] => {β : Sort*}
  [CoeFun Nat fun x ↦ (a : Nat) → (fun x ↦ β) a] [i : foo fun _ ↦ β]
-- error: Calculated binders do not match the expected binders given after `=>`.
-- the suggestion is however identical

[Kyle Miller]

Could you remind me about what the Type* bug is?

[Eric Rodriguez]

Let me dig up your old comment about it, but this seems to be a version of it - the code above is fine with Sort as opposed to Sort*

[Eric Rodriguez]

Replying to me, hah:

Kyle Miller said:

Eric Rodriguez said:

I think there was some progress to do this automatically via variables!/?, did Kyle Miller talk about this recently?

Unfortunately, the variable? mechanism is too simple here and fails because pretty printing isn't round tripping. (Yes, it needs to depend on pretty printing...) It seems to work if you set pp.analyze to true, but I wouldn't count on it, so I'll just say this doesn't work at the moment.

The issue is that IsFiniteMeasure (volume : Measure Ω) pretty prints as IsFiniteMeasure ℙ, without reference to Ω.

example

import Mathlib.Probability.Notation

open MeasureTheory ProbabilityTheory
open scoped ENNReal NNReal

@[variable_alias]
structure ProbabilitySpace (Ω : Type*) [MeasureSpace Ω] [IsFiniteMeasure (volume : Measure Ω)]

variable? {Ω : Type*} [ProbabilitySpace Ω]
/-
Can not satisfy requirements for [IsFiniteMeasure ℙ] due to metavariables.

(Use `set_option trace.variable? true` for step-by-step details.)
-/

-- This actually works:
set_option pp.analyze true
variable? {Ω : Type _} [ProbabilitySpace Ω]
-- It fails if you do `Type*`, but that's a bug in `variable?`.

[Eric Rodriguez]

(in the bottom of the example)

[Eric Rodriguez]

Just curious as to whether you think you'll have time to work on this soon - absolutely no rush if not! I just want to organise when I'll try the FunLike refactor attempt depending on that - if you think this is fixable soon, I'd rather wait for it:)

[Kyle Miller]

@Eric Rodriguez I just created #8908 to try to address it. I'm letting CI run the test file before putting it up for review.

[Kyle Miller]

There's an error I can't figure out right now. I'm trying to disable the linter when elaborating the expected binders, since it can have unused variables. This line was my attempt, but it doesn't seem to affect the linter output (hence the test failure in CI).

[Eric Rodriguez]

The x unused variables warning seems totally fair. But even after using i later, it seems to still lint against that; it seems to be a weird mix about what is linted and what isn't.