Introducing all dependent variables

Stream: mathlib4

[Kyle Miller]

Picking back up some discussion from while ago, this morning I was looking at how to automatically introduce all the dependencies you need to introduce a typeclass, or really anything that depends on a typeclass.

[Kyle Miller]

I've just done a few tests, but it looks promising:

section
variable! [Module R M]
/-
R: Type ?u.18467
M: Type ?u.18470
inst✝²: Semiring R
inst✝¹: AddCommMonoid M
inst✝: Module R M
-/
end

section
variable! [Algebra R A]
/-
R: Type ?u.18767
A: Type ?u.18770
inst✝²: CommSemiring R
inst✝¹: Semiring A
inst✝: Algebra R A
-/
end

section
variable! [Module R M] [Module S M'] (σ : R →+* S) (f : M →ₛₗ[σ] M')
/-
R: Type ?u.20902
M: Type ?u.20905
S: Type ?u.20932
M': Type ?u.20935
inst✝⁵: Semiring R
inst✝⁴: AddCommMonoid M
inst✝³: Module R M
inst✝²: Semiring S
inst✝¹: AddCommMonoid M'
inst✝: Module S M'
σ: R →+* S
f: M →ₛₗ[σ] M'
-/
end

[Kyle Miller]

code

import Lean
import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.Algebra.Basic
import Mathlib.Algebra.Module.LinearMap

namespace Mathlib.Command
open Lean Lean.Elab Lean.Elab.Command Lean.Parser.Term

private def bracketedBinderType : Syntax → Option (TSyntax `term)
  | `(bracketedBinderF|($_* $[: $ty?]? $(_annot?)?)) => ty?
  | `(bracketedBinderF|{$_* $[: $ty?]?})             => ty?
  | `(bracketedBinderF|[$[$_ :]? $ty])               => some ty
  | `(bracketedBinderF|[$ty])                        => some ty
  | _                                                => none

syntax (name := «variable!») "variable!" (bracketedBinder)* : command

/-- Try to elaborate `binders`, adding  -/
partial def expandBinder (depth : Nat) (binder : TSyntax `Lean.Parser.Term.bracketedBinder) :
    TermElabM (Array (TSyntax `Lean.Parser.Term.bracketedBinder)) := do
  if depth == 0 then
    throwError "Maximum recursion depth for variables! reached."
  withTheReader Term.Context (fun ctx => {ctx with ignoreTCFailures := true})
    <| Term.withAutoBoundImplicit
    <| Term.withSynthesize (mayPostpone := true)
    <| Term.elabBinders #[binder] fun _ => do
      let mut binders := #[]
      for mvarId in (← get).pendingMVars.reverse do
        let some decl ← Term.getSyntheticMVarDecl? mvarId | continue
        match decl.kind with
        | .typeClass =>
          let ty ← PrettyPrinter.delab (← mvarId.getType)
          let bi ← `(bracketedBinderF| [$ty])
          let binders' ← expandBinder (depth - 1) bi
          binders := binders ++ binders'
        | _ => pure ()
      return binders.push binder

@[command_elab «variable!»] def elabVariables : CommandElab
  | `(variable! $binders*) => do
    for binder in binders do
      if (bracketedBinderType binder).isNone then
        throwErrorAt binder "variable! cannot update pre-existing variables"
      let binders' ← runTermElabM fun _ => expandBinder 50 binder
      for binder in binders' do
        let varUIds ← getBracketedBinderIds binder |>.mapM (withFreshMacroScope ∘ MonadQuotation.addMacroScope)
        modifyScope fun scope => { scope with varDecls := scope.varDecls.push binder, varUIds := scope.varUIds ++ varUIds }
  | _ => throwUnsupportedSyntax

@[unused_variables_ignore_fn]
def ignoreVariable! : Lean.Linter.IgnoreFunction :=
  fun _ stack _ => stack.matches [`null, none, `null, `Mathlib.Command.variable!]

end Mathlib.Command

section
variable! (x : Nat) [DecidableEq α] -- works like `variable`
variable! [foo : DecidableEq Nat]
variable! {x} -- fails (intentionally doesn't support updating)
variable! (x) -- fails (same reason)
end

section
variable! [Module R M]
/-
R: Type ?u.18467
M: Type ?u.18470
inst✝²: Semiring R
inst✝¹: AddCommMonoid M
inst✝: Module R M
-/
end

section
variable! [Algebra R A]
/-
R: Type ?u.18767
A: Type ?u.18770
inst✝²: CommSemiring R
inst✝¹: Semiring A
inst✝: Algebra R A
-/
end

section
variable! [Module R M] [Module S M'] (σ : R →+* S) (f : M →ₛₗ[σ] M')
/-
R: Type ?u.20902
M: Type ?u.20905
S: Type ?u.20932
M': Type ?u.20935
inst✝⁵: Semiring R
inst✝⁴: AddCommMonoid M
inst✝³: Module R M
inst✝²: Semiring S
inst✝¹: AddCommMonoid M'
inst✝: Module S M'
σ: R →+* S
f: M →ₛₗ[σ] M'
-/
end

(v2 below)

[Kevin Buzzard]

Can it do unique factorization domains? :-) (I ask because I had no clue how to say "let R be a unique factorization domain" until a few weeks ago)

[Kyle Miller]

@Kevin Buzzard I think you'll have to give me a hint, since I'm at least a few weeks behind you there

[Kevin Buzzard]

My understanding is that right now you have to say variables (R : Type) [comm_ring R] [is_domain R] [unique_factorization_monoid R]

[Kyle Miller]

Ah, for that we could have a fake typeclass that implies those typeclasses and which doesn't itself appear in the final variables list.

section
-- Imagine this is marked in some way as being an alias for `variables!` purposes
class UniqueFactorizationDomain (R : Type _) [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R]

variable! [UniqueFactorizationDomain R]
/-
R: Type ?u.26397
inst✝³: CommRing R
inst✝²: IsDomain R
inst✝¹: UniqueFactorizationMonoid R
inst✝: UniqueFactorizationDomain R -- imagine it doesn't include this
-/
end

[Kyle Miller]

Here's a version that seems to be more robust. I was having a hard time juggling the pending metavariables and getting into the right local contexts, so instead this keeps inserting missing variables and re-elaborating until there are no more failures.

code v2

import Lean
import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.Algebra.Basic
import Mathlib.Algebra.Module.LinearMap
import Mathlib.RingTheory.UniqueFactorizationDomain

namespace Mathlib.Command
open Lean Lean.Elab Lean.Elab.Command Lean.Parser.Term

private def bracketedBinderType : Syntax → Option (TSyntax `term)
  | `(bracketedBinderF|($_* $[: $ty?]? $(_annot?)?)) => ty?
  | `(bracketedBinderF|{$_* $[: $ty?]?})             => ty?
  | `(bracketedBinderF|[$[$_ :]? $ty])               => some ty
  | `(bracketedBinderF|[$ty])                        => some ty
  | _                                                => none

syntax (name := «variable!») "variable!" (bracketedBinder)* : command

/-- Tries elaborating binders, inserting new binders whenever typeclass inference fails.
`i` is the index of the next binder that needs to be checked. -/
partial def completeBinders (gas : Nat)
    (binders : TSyntaxArray `Lean.Parser.Term.bracketedBinder) (i : Nat) :
    TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do
  if gas == 0 then
    throwError "Maximum recursion depth for variables! reached, likely due to a bug."
  else if i < binders.size then
    -- Try elaborating the binders so far and see if there are any pending metavariables
    withTheReader Term.Context (fun ctx => {ctx with ignoreTCFailures := true})
    <| Term.withAutoBoundImplicit
    <| Term.withSynthesize (mayPostpone := true)
    <| Term.elabBinders (binders.extract 0 (i + 1)) fun _ => do
      let mut binders' := #[]
      for mvarId in (← get).pendingMVars.reverse do
        let some decl ← Term.getSyntheticMVarDecl? mvarId | continue
        match decl.kind with
        | .typeClass =>
          let ty ← PrettyPrinter.delab (← instantiateMVars (← mvarId.getType))
          let bi ← `(bracketedBinderF| [$ty])
          binders' := binders'.push bi
        | _ => pure ()
      if binders'.isEmpty then
        completeBinders gas binders (i + 1)
      else
        let binders := binders.extract 0 i ++ binders' ++ binders.extract i binders.size
        completeBinders (gas - 1) binders i
  else
    -- One last check with the correct configuration.
    Term.withAutoBoundImplicit <| Term.elabBinders binders fun _ => pure ()
    return binders

@[command_elab «variable!»] def elabVariables : CommandElab
  | `(variable! $binders*) => do
    for binder in binders do
      if (bracketedBinderType binder).isNone then
        throwErrorAt binder "variable! cannot update pre-existing variables"
    let binders' ← runTermElabM fun _ => completeBinders 50 binders 0
    for binder in binders' do
      let varUIds ← getBracketedBinderIds binder |>.mapM (withFreshMacroScope ∘ MonadQuotation.addMacroScope)
      modifyScope fun scope => { scope with varDecls := scope.varDecls.push binder, varUIds := scope.varUIds ++ varUIds }
  | _ => throwUnsupportedSyntax

@[unused_variables_ignore_fn]
def ignoreVariable! : Lean.Linter.IgnoreFunction :=
  fun _ stack _ => stack.matches [`null, none, `null, `Mathlib.Command.variable!]

end Mathlib.Command

section
variable! (x : Nat) [DecidableEq α] -- works like `variable`
variable! [foo : DecidableEq Nat]
variable! {x} -- fails (intentionally doesn't support updating)
variable! (x) -- fails (same reason)
end

section
variable! [Module R M]
/-
R: Type ?u.18467
M: Type ?u.18470
inst✝²: Semiring R
inst✝¹: AddCommMonoid M
inst✝: Module R M
-/
end

section
variable! [Algebra R A]
/-
R: Type ?u.18767
A: Type ?u.18770
inst✝²: CommSemiring R
inst✝¹: Semiring A
inst✝: Algebra R A
-/
end

section
variable! [Module R M] [Module S M'] (σ : R →+* S) (f : M →ₛₗ[σ] M')
/-
R: Type ?u.20902
M: Type ?u.20905
S: Type ?u.20932
M': Type ?u.20935
inst✝⁵: Semiring R
inst✝⁴: AddCommMonoid M
inst✝³: Module R M
inst✝²: Semiring S
inst✝¹: AddCommMonoid M'
inst✝: Module S M'
σ: R →+* S
f: M →ₛₗ[σ] M'
-/
end

section
variable! (σ : R →+* S) [Module R M] [Module S M']
-- Limitation:
/-
R: Type ?u.24671
S: Type ?u.24674
M: Type ?u.24695
M': Type ?u.24727
inst✝⁷: NonAssocSemiring R
inst✝⁶: NonAssocSemiring S
σ: R →+* S
inst✝⁵: Semiring R
inst✝⁴: AddCommMonoid M
inst✝³: Module R M
inst✝²: Semiring S
inst✝¹: AddCommMonoid M'
inst✝: Module S M'
-/
end

section
variable! [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R]
/-
R: Type ?u.23587
inst✝²: CommRing R
inst✝¹: IsDomain R
inst✝: UniqueFactorizationMonoid R
-/
end

(edit: v3 below)

[Kyle Miller]

There's a limitation with this approach, though, where it doesn't do any computations to see whether some typeclasses imply others

section
variable! (σ : R →+* S) [Module R M] [Module S M']
/-
R: Type ?u.24671
S: Type ?u.24674
M: Type ?u.24695
M': Type ?u.24727
inst✝⁷: NonAssocSemiring R
inst✝⁶: NonAssocSemiring S
σ: R →+* S
inst✝⁵: Semiring R
inst✝⁴: AddCommMonoid M
inst✝³: Module R M
inst✝²: Semiring S
inst✝¹: AddCommMonoid M'
inst✝: Module S M'
-/
end

[Kevin Buzzard]

oh man, I want to change the defaults to make everything a comm_ring. Would that be possible? Heh, maybe I'm just asking for variable :-)

[Kyle Miller]

Putting some CommRing instances first definitely fixes this last problem:

section
variable! [CommRing R] [CommRing S] (σ : R →+* S) [Module R M] [Module S M']
/-
R: Type ?u.30154
S: Type ?u.30157
M: Type ?u.30320
M': Type ?u.30490
inst✝⁵: CommRing R
inst✝⁴: CommRing S
σ: R →+* S
inst✝³: AddCommMonoid M
inst✝²: Module R M
inst✝¹: AddCommMonoid M'
inst✝: Module S M'
-/
end

[Kyle Miller]

I could imagine there being a configuration option where you can give rules like "if you need a NonAssocSemiring, add a CommRing instead"

[Thomas Murrills]

Really nice! For the syntax, I wonder: should it use [[]] (or whatever brackets we end up using for that) instead of variable!? E.g. variable [[Module R M]]? This would be consistent with doing the same thing inside defs and theorems. Or is that impractical for some reason?

[Kyle Miller]

This has wider scope than a [[...]] binder:

variable! (σ : R →+* S)
/-
R: Type ?u.30490
S: Type ?u.30493
inst✝¹: NonAssocSemiring R
inst✝: NonAssocSemiring S
σ: R →+* S
-/

[Kyle Miller]

Also, we can't define our own binders, unfortunately.

[Thomas Murrills]

Ah, it also introduces dependencies for non-typeclass variables, got it!

[Thomas Murrills]

Kyle Miller said:

Also, we can't define our own binders, unfortunately.

Oh, that is unfortunate…!

[Kevin Buzzard]

But I want AddCommGroups! This is why I realise that I should probably just stick to variable. How about analysis? Does [normed_space 𝕜 E] fill in the right gaps? What about [normed_space ℝ E]?

[Kevin Buzzard]

What about differential geometry? How much more do I have to give than [smooth_manifold_with_corners I M]?

[Kyle Miller]

It doesn't seem that NormedSpace is ported yet.

[Kyle Miller]

What's your objection about AddCommGroup?

[Kevin Buzzard]

your M was a monoid.

[Kyle Miller]

Then you can add that it's an additive commutative group:

variable! [AddCommGroup M] [Module R M]
/-
M: Type ?u.31767
R: Type ?u.31770
inst✝²: AddCommGroup M
inst✝¹: Semiring R
inst✝: Module R M
-/

[Kevin Buzzard]

But now R isn't a commutative ring -- what I'm saying is that I'm now understanding that actually I'd be better off with variable because tyipcally I do not want the minimal assumptions for which module makes sense (in fact I never want these assumptions)

[Kevin Buzzard]

Of course, others might.

[Kyle Miller]

Maybe we don't want variable! in mathlib code, but it at least shows you everything you need to address on your way to a complete variable line.

[Kyle Miller]

You can use variable! everywhere variable already works.

[Thomas Murrills]

But also R was explicitly given as a commutative ring in the first example but not the second.

[Thomas Murrills]

@Kevin Buzzard maybe you want that sort of abbreviation typeclass mentioned earlier to use in place of Module here (which would add all the assumptions you do want)?

[Kyle Miller]

There could be configuration options to help you deal with specific situations, like a commutative algebra setting where whenever there is a request for something CommRing implies then use CommRing, etc.

[Kevin Buzzard]

I don't really know what I want, I'm just wondering where these ideas are going. For me I always want R to be a commutative ring and M an R-module but I would imagine that the non-commutative guys always want R to be a ring. If semiring people actually exist (something I'm slightly skeptical about) then they'll want something else. I don't have a clear idea about how to support all these competing "canonical" assumptions.

[Kevin Buzzard]

Aah, yeah maybe switch on "commutative algebra mode" and then try it :-)

[Kyle Miller]

it could be variable! (config := commAlg) ... for you

[Kyle Miller]

Another example to show possible scope (introducing Decidable assumptions):

variable! (p : Nat → Prop) (h : ∃ k, p k) (h : 0 < Nat.find h)
/-
p: ℕ → Prop
h✝: ∃ k, p k
inst✝: DecidablePred fun n => p n
h: 0 < Nat.find h✝
-/

[Eric Wieser]

Isn't the answer to Kevin's requrest just to adapt your

-- Imagine this is marked in some way as being an alias for `variables!` purposes
class UniqueFactorizationDomain (R : Type _) [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R]

example above, but for VectorSpace?

[Kevin Buzzard]

Do we actually want to make this class?

[Kevin Buzzard]

I mean, it would be handy for maths undergraduates but would it clog up the system somehow? I remember trying to make vector space just to mean "module over a field" and then this was reverted later because it somehow caused trouble. (I have a poor understanding of these sorts of issues)

[Kyle Miller]

Kevin Buzzard said:

Do we actually want to make this class?

Imagine classes that are used only for variables! and which would otherwise show a warning if you try to use them, and where they don't actually appear after they get expanded.

[Eric Wieser]

I don't think we want to make a class, but I think we could make it a macro of some kind

[Eric Wieser]

I don't think we want to make a class, but I think we could make it a macro of some kind (edit: bad train internet)

[Eric Wieser]

Presumably we can override the parser for theorem in mathlib to handle [[foo X]] or [!foo X] or similar so that we're not limited to variables lines

[Thomas Murrills]

(Off topic, but I do like e.g. ![foo X] or [foo X]! better than [[foo X]]; all those square brackets are a bit busy imo :) )

[Thomas Murrills]

The other option is of course introducing an analogous theorem!

[Eric Wieser]

![foo X] might conflict with vector notation; if not to Lean, then perhaps still to the reader

[Kyle Miller]

Eric Wieser said:

Isn't the answer to Kevin's requrest just to adapt your [...]

That's one answer, but it might be nice to be able to write variable! (σ : R →+* S) and have it introduce CommRings instead of NonAssocSemirings, if things are in commutative algebraist mode. The class alias idea is just for packaging up some common notions, when it's not obvious what you're supposed to introduce.

One reason using class for this is convenient (rather than creating macros) is that you get things like documentation on mouseover for free, and it'd be easier for non-macro-ologists to write their own. You also can see that your alias is type correct, which you don't get with macros. Still, I wonder if there are examples where macros would be more flexible.

[Adam Topaz]

Eric Wieser said:

Presumably we can override the parser for theorem in mathlib to handle [[foo X]] or [!foo X] or similar so that we're not limited to variables lines

Ideally we would find some way to do this under binders as well... What if I want to write forall R S [[Module R S]], ...?

[Kyle Miller]

Maybe more generally forall (! σ : R →+* S), ... and forall R S [! Module R S], ...

[Adam Topaz]

Is that possible? I thought Mario said it was not on some other thread.

[Kyle Miller]

I mean, forall R S [[Module R S]], ... isn't possible either, right?

[Adam Topaz]

right

[Adam Topaz]

that's why I'm asking the expert :)

[Kyle Miller]

I'm just dreaming. Maybe one day Lean 4 devs will create hooks for our own binder types.

[Eric Wieser]

Adam Topaz said:

Ideally we would find some way to do this under binders as well... What if I want to write forall R S [[Module R S]], ...?

That feels like a very niche case where it probably pays to be explicit

[Adam Topaz]

But this is a general idea... somehow [[Module R S]] should expand to [Semiring R] [AddMonoid S] [Module R S] in all places where this can apply.

[Adam Topaz]

And it's not too niche. For example it's certainly reasonable to imagine something like this being used in the definition of some universal property or something.

[Adam Topaz]

I suppose if we had such a general feature, we would end up using a lot more mixins, making it even more common.

[Eric Wieser]

For example it's certainly reasonable to imagine something like this being used in the definition of some universal property or something.

I would claim this probably happens no more than 10 times in mathlib, but maybe I'm not familiar with the parts that do this

[Adam Topaz]

maybe it happens so few times because it's not convenient to do (yet)?

[Adam Topaz]

It certainly was not convenient in lean3 not just because of the topic of this thread, but also because the instances didn't register (without using introsI and friends). But now that's been fixed in lean4, and I can imagine it becoming more commonplace.

[Kyle Miller]

What's the argument here Eric? I'm not sure why it matters if it's a niche use -- if we had the ability to make our own binders that seems like the right way to implement this feature everywhere.

[Eric Wieser]

Mainly just that custom binders in theorem/def/variable is probably possible to do without core changes, and that the benefit of supporting forall on top of that is pretty marginal.

[Eric Rodriguez]

Kyle Miller said:

it could be variable! (config := commAlg) ... for you

i wonder if this should be file-wide

[Kyle Miller]

Ok, I think saying forall is a niche use is completely independent of whether in the short term (i.e., before the hypothetical time when Lean supports custom binders) we might have custom theorem/def/variables for mathlib that support additional binder types. The only reason why it would matter is if someone were to suggest making a custom forall too.

[Kyle Miller]

Here's a v3, now with "Try this" and hopefully more robust binder insertion. Example:

variable!? [Algebra R A]
-- Try this: variable [CommSemiring R] [Semiring A] [Algebra R A]

code v3

import Lean
import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.Algebra.Basic
import Mathlib.Algebra.Module.LinearMap
import Mathlib.RingTheory.UniqueFactorizationDomain

namespace Mathlib.Command
open Lean Lean.Elab Lean.Elab.Command Lean.Parser.Term

private def bracketedBinderType : Syntax → Option (TSyntax `term)
  | `(bracketedBinderF|($_* $[: $ty?]? $(_annot?)?)) => ty?
  | `(bracketedBinderF|{$_* $[: $ty?]?})             => ty?
  | `(bracketedBinderF|[$[$_ :]? $ty])               => some ty
  | `(bracketedBinderF|[$ty])                        => some ty
  | _                                                => none

syntax (name := «variable!») "variable!" "?"? (bracketedBinder)* : command
macro "variable!?" binders:bracketedBinder* : command => `(command| variable! ? $binders*)

/-- Tries elaborating binders, inserting new binders whenever typeclass inference fails.
`i` is the index of the next binder that needs to be checked. -/
partial def completeBinders (gas : Nat)
    (binders : TSyntaxArray `Lean.Parser.Term.bracketedBinder) (i : Nat) :
    CommandElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do
  if 0 < gas && i < binders.size then
    -- Try elaborating the binders so far and see if they create any pending metavariables.
    let info ← getInfoState
    let binders' ← runTermElabM fun _ => do
      withTheReader Term.Context
          (fun ctx => {ctx with ignoreTCFailures := true})
      <| Term.withAutoBoundImplicit
      <| Term.withSynthesize (mayPostpone := true)
      <| Term.elabBinders (binders.extract 0 (i + 1)) fun _ => do
        let mut binders' := #[]
        let pendingSet : MVarIdSet := (← get).pendingMVars.foldl MVarIdSet.insert RBMap.empty
        for mvarId in (← get).pendingMVars.reverse do
          let some decl ← Term.getSyntheticMVarDecl? mvarId | continue
          match decl.kind with
          | .typeClass =>
            let ty ← instantiateMVars (← mvarId.getType)
            -- Only want to consider those that don't have natural metavariables, which helps
            -- prevent infinite regress.
            let nonSynthMVar? := ty.findMVar? fun mvar => not (RBMap.contains pendingSet mvar)
            if nonSynthMVar?.isNone then
              let bi ← `(bracketedBinderF| [$(← PrettyPrinter.delab ty)])
              binders' := binders'.push bi
          | _ => pure ()
        return binders'
    setInfoState info
    if binders'.isEmpty then
      completeBinders gas binders (i + 1)
    else
      let binders := binders.extract 0 i ++ binders' ++ binders.extract i binders.size
      completeBinders (gas - binders'.size) binders i
  else
    if gas == 0 then
      logError "Maximum recursion depth for variables! reached, likely due to a bug."
    -- One last check with the correct configuration.
    runTermElabM fun _ => Term.withAutoBoundImplicit <| Term.elabBinders binders fun _ => pure ()
    return binders

@[command_elab «variable!»] def elabVariables : CommandElab
  | `(variable! $[?%$info]? $binders*) => do
    for binder in binders do
      if (bracketedBinderType binder).isNone then
        throwErrorAt binder "variable! cannot update pre-existing variables"
    let binders' ← completeBinders 50 binders 0
    if info.isSome then
      logInfo m!"Try this: {← `(variable $binders'*)}"
    for binder in binders' do
      let varUIds ← getBracketedBinderIds binder |>.mapM (withFreshMacroScope ∘ MonadQuotation.addMacroScope)
      modifyScope fun scope => { scope with varDecls := scope.varDecls.push binder, varUIds := scope.varUIds ++ varUIds }
  | _ => throwUnsupportedSyntax

@[unused_variables_ignore_fn]
def ignoreVariable! : Lean.Linter.IgnoreFunction :=
  fun _ stack _ => stack.matches [`null, none, `null, `Mathlib.Command.variable!]

end Mathlib.Command

section
variable! (x : Nat) [DecidableEq α] -- works like `variable`
variable! [foo : DecidableEq Nat]
variable! {x} -- fails (intentionally doesn't support updating)
variable! (x) -- fails (same reason)
end

section
variable! [Module R M]
/-
R: Type ?u.18467
M: Type ?u.18470
inst✝²: Semiring R
inst✝¹: AddCommMonoid M
inst✝: Module R M
-/
end

section
variable! [Algebra R A]
/-
R: Type ?u.18767
A: Type ?u.18770
inst✝²: CommSemiring R
inst✝¹: Semiring A
inst✝: Algebra R A
-/
end

section
variable!? [Algebra R A]
-- Try this: variable [CommSemiring R] [Semiring A] [Algebra R A]
end

section
-- Bug: doesn't report error unless you uncomment the `#check`.
variable! [Module R M] [Module S M'] (f : M →ₛₗ[σ] M')
--#check 1

-- This is a bug in variables, too.
-- variable [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S]
--   [AddCommMonoid M'] [Module S M'] (f : M →ₛₗ[σ] M')
end

section
variable! [Module R M] [Module S M'] (σ : R →+* S) (f : M →ₛₗ[σ] M')
/-
R: Type ?u.20902
M: Type ?u.20905
S: Type ?u.20932
M': Type ?u.20935
inst✝⁵: Semiring R
inst✝⁴: AddCommMonoid M
inst✝³: Module R M
inst✝²: Semiring S
inst✝¹: AddCommMonoid M'
inst✝: Module S M'
σ: R →+* S
f: M →ₛₗ[σ] M'
-/
end

section
variable! (σ : R →+* S) [Module R M] [Module S M']
-- Limitation:
/-
R: Type ?u.24671
S: Type ?u.24674
M: Type ?u.24695
M': Type ?u.24727
inst✝⁷: NonAssocSemiring R
inst✝⁶: NonAssocSemiring S
σ: R →+* S
inst✝⁵: Semiring R
inst✝⁴: AddCommMonoid M
inst✝³: Module R M
inst✝²: Semiring S
inst✝¹: AddCommMonoid M'
inst✝: Module S M'
-/
end

section
variable! [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R]
/-
R: Type ?u.23587
inst✝²: CommRing R
inst✝¹: IsDomain R
inst✝: UniqueFactorizationMonoid R
-/
end

section
-- Imagine this is marked in some way as being an alias for `variables!`
class UniqueFactorizationDomain (R : Type _) [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R]

variable! [UniqueFactorizationDomain R]
/-
R: Type ?u.26397
inst✝³: CommRing R
inst✝²: IsDomain R
inst✝¹: UniqueFactorizationMonoid R
inst✝: UniqueFactorizationDomain R -- imagine it doesn't include this
-/
end

section
variable! [CommRing R] [CommRing S] (σ : R →+* S) [Module R M] [Module S M']
/-
R: Type ?u.30154
S: Type ?u.30157
M: Type ?u.30320
M': Type ?u.30490
inst✝⁵: CommRing R
inst✝⁴: CommRing S
σ: R →+* S
inst✝³: AddCommMonoid M
inst✝²: Module R M
inst✝¹: AddCommMonoid M'
inst✝: Module S M'
-/
end

section
variable! (σ : R →+* S)
/-
R: Type ?u.30490
S: Type ?u.30493
inst✝¹: NonAssocSemiring R
inst✝: NonAssocSemiring S
σ: R →+* S
-/
end

section
variable! [AddCommGroup M] [Module R M]
/-
M: Type ?u.31767
R: Type ?u.31770
inst✝²: AddCommGroup M
inst✝¹: Semiring R
inst✝: Module R M
-/
end

section
variable! (p : Nat → Prop) (h : ∃ k, p k) (h : 0 < Nat.find h)
/-
p: ℕ → Prop
h✝: ∃ k, p k
inst✝: DecidablePred fun n => p n
h: 0 < Nat.find h✝
-/
end

[Kyle Miller]

I spent a while trying to track down a bug in what I thought was my own code, but I guess variable has the same bug.

This doesn't report any errors:

variable [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S]
   [AddCommMonoid M'] [Module S M'] (f : M →ₛₗ[σ] M')

This does:

variable [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S]
   [AddCommMonoid M'] [Module S M'] (f : M →ₛₗ[σ] M')
#check 1
/-
Error on f's type:
typeclass instance problem is stuck, it is often due to metavariables
  Module ?m.34167 M'
-/

[Mario Carneiro]

Kyle Miller said:

Ok, I think saying forall is a niche use is completely independent of whether in the short term (i.e., before the hypothetical time when Lean supports custom binders) we might have custom theorem/def/variables for mathlib that support additional binder types. The only reason why it would matter is if someone were to suggest making a custom forall too.

I am generally dubious of approaches that require replacing theorem/def etc. I think there will be a lot of unintended side effects of doing that across mathlib, e.g. some stuff hard coded in the server looking for a certain syntax kind, syntax kinds being referred to in mathport (or choice nodes!)

[Johan Commelin]

@Kyle Miller Is the problem that you didn't specify σ, and Lean is telling you this in a somewhat opaque way?

[Kyle Miller]

Yeah, that's why there's an error (when it decides to actually report it). The autoimplicit feature adds σ : ?R1 ->*+ ?R2 to the context, and then it tries to infer Module ?R1 M and Module ?R2 M', but it can't make any progress on these (and they definitely don't follow from Module R M or Module S M').

[Arthur Paulino]

Can we have this in core? :pray:

[Bryan Gin-ge Chen]

@Kyle Miller What would it take to get something like this over the line? [[]] notation came up again in #PR reviews > #28803 refactor: unbundle algebra from `ENormed*`. I guess we can't use that notation exactly, but it seems to me that what you did with variable! here could help somewhat with the readability issues discussed there.

I also note that Sébastien suggested a variable_alias command in #mathlib4 > Normed modules @ 💬 which could be a next step for this.

[Kyle Miller]

@Bryan Gin-ge Chen Mathlib's variable? has @[variable_alias]. That's what Sébastien's suggestion is equivalent to, right? There's an example in MathlibTest/Variable.lean

All of @Sébastien Gouëzel's examples in that linked thread work exactly expected:

import Mathlib

section
variable? {k E : Type*} [Module k E]
/-
Try this: variable? {k E : Type*} [Module k E] =>
  {k E : Type*} [Semiring k] [AddCommMonoid E] [Module k E]
-/
end

section
variable? {k E : Type*} [NormedAddCommGroup E] [Module k E]
/-
Try this: variable? {k E : Type*} [NormedAddCommGroup E] [Module k E] =>
  {k E : Type*} [NormedAddCommGroup E] [Semiring k] [Module k E]
-/
end

@[variable_alias]
structure HilbertSpace' (k E : Type*)
  [RCLike k] [SeminormedAddCommGroup E] [InnerProductSpace k E] [CompleteSpace E]

section
variable? {k E : Type*} [HilbertSpace' k E]
/-
Try this: variable? {k E : Type*} [HilbertSpace' k E] =>
  {k E : Type*} [RCLike k] [SeminormedAddCommGroup E]
  [InnerProductSpace k E] [CompleteSpace E]
-/
end

Note that the "try this" adds in a hint so that the expanded form appears in the source code, and there's a check that it generates the same thing.

If somehow [[...]] is the ideal syntax for "expand only this", I think that could be worked into variable?.

I saw that Sébastien said that a variable_alias command would ideally support hovers — hovering over HilbertSpace' shows all the typeclass assumptions it depends on, because they appear in its type.

[Bryan Gin-ge Chen]

Ah, it looks like I totally missed the discussion in #mathlib4 > variable! which is why we aren't already using this all over the place... I guess it may be a good time to revisit this.

[Jireh Loreaux]

One issue that isn't addressed with variable? is including this in theorem/def statements.

[Bryan Gin-ge Chen]

We'd need to wait for core changes for that, right? In the meantime it's ugly, but variable? ... in theorem does seem to work.

[Jireh Loreaux]

Potentially we could make lemma actually different from theorem so that it could parse [[HilbertSpace 𝕜 E]] arguments (or maybe ⟦HilbertSpace 𝕜 E⟧ is a better notation? :shrug:)

[Sébastien Gouëzel]

Do I understand correctly that, for now, variable? is not supposed to stay in the code? I.e, we're supposed to replace it with the Try this output, so I don't see how it helps with the verbosity.

[Jireh Loreaux]

1. it may not help with verbosity as-is (but we could potentially make it shut up or introduce a variant to do so).
2. it would at least help with readability because you can just pay attention to what comes before the =>.

[Kyle Miller]

@Sébastien Gouëzel It stays in code. Notice that the "try this" output adds the expanded => clause, but keeps the original input.

Yes, it's verbose, but what came up during review was how for maintainability we'd want to know what the expanded list of instances is. I sort of think it's like a non-terminal simp. The result can be very sensitive to the instance set.

[Kyle Miller]

I do want to see double-bracket instance notation one day, but getting it right looks pretty subtle. There have been a few proposals for how to do it too.

It would be nice if there were a solution that wasn't quite so sensitive, or quite so easy to accidentally get some overlapping instances, or that depends on the (slow) process of adding instances on instance synthesis failure. One direction I've been thinking about is having a way to more formally specify the lattice structure on instances. The double bracket notation could look at existing instances and figure out which instances to include to meet the requirements, while avoiding duplicate data fields, and giving errors if it's impossible. I'd hope that you could look at the double bracket notation and figure out what it expands to in your head, or at least trust that it's not doing anything fishy.

The lattice might also be a way to give more specific errors on instance failure in general.

[Jireh Loreaux]

I think this might be less of a problem if we unbundled more.

[Jireh Loreaux]

Are variable? lines elaborated more than once? I seem to remember that was the case (at least at one point) for variable, but I can't remember if it changed.

[Kyle Miller]

The variable? computation happens once, but all the binders it generates get elaborated multiple times, just like variable.