Documentation

Lean.MetavarContext

The metavariable context stores metavariable declarations and their assignments. It is used in the elaborator, tactic framework, unifier (aka isDefEq), and type class resolution (TC). First, we list all the requirements imposed by these modules.

f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m

where (?a : Type) (?s : Ring ?a) (?x ?y : ?a) During isDefEq (i.e., unification), it will need to solve the constrain

ringAdd ?s =?= intAdd

We say ringAdd ?s is stuck because it cannot be reduced until we synthesize the term ?s : Ring ?a using TC. This can be done since we have assigned ?a := Int when solving ?a =?= Int.

Elaborator (-> TC -> isDefEq)+
Elaborator -> isDefEq (-> TC -> isDefEq)*
Elaborator -> simp -> isDefEq (-> TC -> isDefEq)*

In Lean4, TC may also invoke tactics in the future.

fun xs => t[?m]

will be ill-formed if we later assign a term s to ?m, and s contains free variables in xs. We address this issue by changing the free variable abstraction procedure. We consider two cases: ?m is natural or synthetic, or ?m is syntheticOpaque. Assume the type of ?m is A[xs]. Then, in both cases we create an auxiliary metavariable ?n with type forall xs => A[xs], and local context := local context of ?m - xs. In both cases, we produce the term fun xs => t[?n xs]

1- If ?m is natural or synthetic, then we assign ?m := ?n xs, and we produce the term fun xs => t[?n xs]

2- If ?m is syntheticOpaque, then we mark ?n as a syntheticOpaque variable. However, ?n is managed by the metavariable context itself. We say we have a "delayed assignment" ?n xs := ?m. That is, after a term s is assigned to ?m, and s does not contain metavariables, we replace any occurrence ?n ts with s[xs := ts].

Gruesome details:

let x : T := v; t[?m]

will be ill-formed if we later assign a term s to ?m, and s contains free variable x. Again, assume the type of ?m is A[x].

1- If `?m` is natural or synthetic, then we create `?n : (let x : T := v; A[x])` with
and local context := local context of `?m` - `x`, we assign `?m := ?n`,
and produce the term `let x : T := v; t[?n]`. That is, we are just making
sure `?n` must never be assigned to a term containing `x`.

2- If `?m` is syntheticOpaque, we create a fresh syntheticOpaque `?n`
with type `?n : T -> (let x : T := v; A[x])` and local context := local context of `?m` - `x`,
create the delayed assignment `?n #[x] := ?m`, and produce the term `let x : T := v; t[?n x]`.
Now suppose we assign `s` to `?m`. We do not assign the term `fun (x : T) => s` to `?n`, since
`fun (x : T) => s` may not even be type correct. Instead, we just replace applications `?n r`
with `s[x/r]`. The term `r` may not necessarily be a bound variable. For example, a tactic
may have reduced `let x : T := v; t[?n x]` into `t[?n v]`.
We are essentially using the pair "delayed assignment + application" to implement a delayed
substitution.

In Lean4, we are using a simpler design for the MetavarContext.

The temporary metavariables were also used in the "app builder" module used in Lean3. The app builder uses isDefEq. So, it could, in principle, invoke an arbitrary number of nested TC problems. However, in Lean3, all app builder uses are controlled. That is, it is mainly used to synthesize implicit arguments using very simple unification and/or non-nested TC. So, if the "app builder" becomes a bottleneck without tmp metavars, we may solve the issue by implementing isDefEqCheap that never invokes TC and uses tmp metavars.

LocalInstance represents a local typeclass instance registered by and for the elaborator. It stores the name of the typeclass in className, and the concrete typeclass instance in fvar. Note that the kernel does not care about this information, since typeclasses are entirely eliminated during elaboration.

Instances For
    Equations
    @[inline, reducible]
    Equations
    Instances For
      Equations

      Remove local instance with the given fvarId. Do nothing if localInsts does not contain any free variable with id fvarId.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        A kind for the metavariable that determines its unification behaviour. For more information see the large comment at the beginning of this file.

        Instances For
          Equations
          Instances For
            Equations
            Instances For
              • userName : Lake.Name

                A user-friendly name for the metavariable. If anonymous then there is no such name.

              • The local context containing the free variables that the mvar is permitted to depend upon.

              • type : Lean.Expr

                The type of the metavarible, in the given lctx.

              • depth : Nat

                The nesting depth of this metavariable. We do not want unification subproblems to influence the results of parent problems. The depth keeps track of this information and ensures that unification subproblems cannot leak information out, by unifying based on depth.

              • localInstances : Lean.LocalInstances
              • numScopeArgs : Nat

                See comment at CheckAssignment Meta/ExprDefEq.lean

              • index : Nat

                We use this field to track how old a metavariable is. It is set using a counter at MetavarContext

              Information about a metavariable.

              Instances For
                Equations
                • One or more equations did not get rendered due to their size.

                A delayed assignment for a metavariable ?m. It represents an assignment of the form ?m := (fun fvars => (mkMVar mvarIdPending)). mvarIdPending is a syntheticOpaque metavariable that has not been synthesized yet. The delayed assignment becomes a real one as soon as mvarIdPending has been fully synthesized. fvars are variables in the mvarIdPending local context.

                See the comment below assignDelayedMVar for the rationale of delayed assignments.

                Recall that we use a locally nameless approach when dealing with binders. Suppose we are trying to synthesize ?n in the expression e, in the context of (fun x => e). The metavariable ?n might depend on the bound variable x. However, since we are locally nameless, the bound variable x is in fact represented by some free variable fvar_x. Thus, when we exit the scope, we must rebind the value of fvar_x in ?n to the de-bruijn index of the bound variable x.

                Instances For

                  The metavariable context is a set of metavariable declarations and their assignments.

                  For more information on specifics see the comment in the file that MetavarContext is defined in.

                  Instances For
                    class Lean.MonadMCtx (m : TypeType) :

                    A monad with a stateful metavariable context, defining getMCtx and modifyMCtx.

                    Instances
                      @[always_inline]
                      instance Lean.instMonadMCtx (m : TypeType) (n : TypeType) [MonadLift m n] [Lean.MonadMCtx m] :
                      Equations
                      @[inline, reducible]
                      abbrev Lean.setMCtx {m : TypeType} [Lean.MonadMCtx m] (mctx : Lean.MetavarContext) :
                      Equations
                      Instances For
                        @[inline, reducible]
                        Equations
                        Instances For
                          Equations
                          Instances For
                            Equations
                            Instances For
                              partial def Lean.getDelayedMVarRoot {m : TypeType} [Monad m] [Lean.MonadMCtx m] (mvarId : Lean.MVarId) :

                              Given a sequence of delayed assignments

                              mvarId₁ := mvarId₂ ...;
                              ...
                              mvarIdₙ := mvarId_root ...  -- where `mvarId_root` is not delayed assigned
                              

                              in mctx, getDelayedRoot mctx mvarId₁ return mvarId_root. If mvarId₁ is not delayed assigned then return mvarId₁

                              Equations
                              Instances For

                                Return true if the give metavariable is already assigned.

                                Equations
                                Instances For
                                  @[deprecated Lean.MVarId.isAssigned]
                                  Equations
                                  Instances For
                                    Equations
                                    Instances For
                                      @[deprecated Lean.MVarId.isDelayedAssigned]
                                      Equations
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            Instances For
                                              @[deprecated Lean.MVarId.isAssignable]
                                              Equations
                                              Instances For

                                                Return true iff the given level contains an assigned metavariable.

                                                Equations
                                                Instances For

                                                  Return true iff the given level contains a metavariable that can be assigned.

                                                  Equations
                                                  Instances For
                                                    def Lean.assignLevelMVar {m : TypeType} [Lean.MonadMCtx m] (mvarId : Lean.LMVarId) (val : Lean.Level) :

                                                    Add mvarId := u to the universe metavariable assignment. This method does not check whether mvarId is already assigned, nor it checks whether a cycle is being introduced. This is a low-level API, and it is safer to use isLevelDefEq (mkLevelMVar mvarId) u.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      def Lean.MVarId.assign {m : TypeType} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (val : Lean.Expr) :

                                                      Add mvarId := x to the metavariable assignment. This method does not check whether mvarId is already assigned, nor it checks whether a cycle is being introduced, or whether the expression has the right type. This is a low-level API, and it is safer to use isDefEq (mkMVar mvarId) x.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[deprecated Lean.MVarId.assign]
                                                        def Lean.assignExprMVar {m : TypeType} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (val : Lean.Expr) :
                                                        Equations
                                                        Instances For
                                                          def Lean.assignDelayedMVar {m : TypeType} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (mvarIdPending : Lean.MVarId) :
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For

                                                            Notes on artificial eta-expanded terms due to metavariables. We try avoid synthetic terms such as ((fun x y => t) a b) in the output produced by the elaborator. This kind of term may be generated when instantiating metavariable assignments. This module tries to avoid their generation because they often introduce unnecessary dependencies and may affect automation.

                                                            When elaborating terms, we use metavariables to represent "holes". Each hole has a context which includes all free variables that may be used to "fill" the hole. Suppose, we create a metavariable (hole) ?m : Nat in a context containing (x : Nat) (y : Nat) (b : Bool), then we can assign terms such as x + y to ?m since x and y are in the context used to create ?m. Now, suppose we have the term ?m + 1 and we want to create the lambda expression fun x => ?m + 1. This term is not correct since we may assign to ?m a term containing x. We address this issue by create a synthetic metavariable ?n : NatNat and adding the delayed assignment ?n #[x] := ?m, and the term fun x => ?n x + 1. When we later assign a term t[x] to ?m, fun x => t[x] is assigned to ?n, and if we substitute it at fun x => ?n x + 1, we produce fun x => ((fun x => t[x]) x) + 1. To avoid this term eta-expanded term, we apply beta-reduction when instantiating metavariable assignments in this module. This operation is performed at instantiateExprMVars, elimMVarDeps, and levelMVarToParam.

                                                            instantiateExprMVars main function

                                                            Equations
                                                            • Lean.instMonadMCtxStateRefT'MetavarContextST = { getMCtx := get, modifyMCtx := modify }
                                                            Equations
                                                            Instances For
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      Instances For
                                                                        Equations
                                                                        @[inline]
                                                                        Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          def Lean.findExprDependsOn {m : TypeType} [Monad m] [Lean.MonadMCtx m] (e : Lean.Expr) (pf : optParam (Lean.FVarIdBool) fun x => false) (pm : optParam (Lean.MVarIdBool) fun x => false) :

                                                                          Return true iff e depends on a free variable x s.t. pf x is true, or an unassigned metavariable ?m s.t. pm ?m is true. For each metavariable ?m (that does not satisfy pm occurring in x 1- If ?m := t, then we visit t looking for x 2- If ?m is unassigned, then we consider the worst case and check whether x is in the local context of ?m. This case is a "may dependency". That is, we may assign a term t to ?m s.t. t contains x.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            @[inline]
                                                                            def Lean.findLocalDeclDependsOn {m : TypeType} [Monad m] [Lean.MonadMCtx m] (localDecl : Lean.LocalDecl) (pf : optParam (Lean.FVarIdBool) fun x => false) (pm : optParam (Lean.MVarIdBool) fun x => false) :

                                                                            Similar to findExprDependsOn, but checks the expressions in the given local declaration depends on a free variable x s.t. pf x is true or an unassigned metavariable ?m s.t. pm ?m is true.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              def Lean.exprDependsOn {m : TypeType} [Monad m] [Lean.MonadMCtx m] (e : Lean.Expr) (fvarId : Lean.FVarId) :
                                                                              Equations
                                                                              Instances For
                                                                                def Lean.dependsOn {m : TypeType} [Monad m] [Lean.MonadMCtx m] (e : Lean.Expr) (fvarId : Lean.FVarId) :

                                                                                Return true iff e depends on the free variable fvarId

                                                                                Equations
                                                                                Instances For
                                                                                  def Lean.localDeclDependsOn {m : TypeType} [Monad m] [Lean.MonadMCtx m] (localDecl : Lean.LocalDecl) (fvarId : Lean.FVarId) :

                                                                                  Return true iff localDecl depends on the free variable fvarId

                                                                                  Equations
                                                                                  Instances For

                                                                                    Similar to exprDependsOn, but x can be a free variable or an unassigned metavariable.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      def Lean.localDeclDependsOn' {m : TypeType} [Monad m] [Lean.MonadMCtx m] (localDecl : Lean.LocalDecl) (x : Lean.Expr) :

                                                                                      Similar to localDeclDependsOn, but x can be a free variable or an unassigned metavariable.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        def Lean.dependsOnPred {m : TypeType} [Monad m] [Lean.MonadMCtx m] (e : Lean.Expr) (pf : optParam (Lean.FVarIdBool) fun x => false) (pm : optParam (Lean.MVarIdBool) fun x => false) :

                                                                                        Return true iff e depends on a free variable x s.t. pf x, or an unassigned metavariable ?m s.t. pm ?m is true.

                                                                                        Equations
                                                                                        Instances For
                                                                                          def Lean.localDeclDependsOnPred {m : TypeType} [Monad m] [Lean.MonadMCtx m] (localDecl : Lean.LocalDecl) (pf : optParam (Lean.FVarIdBool) fun x => false) (pm : optParam (Lean.MVarIdBool) fun x => false) :

                                                                                          Return true iff the local declaration localDecl depends on a free variable x s.t. pf x, an unassigned metavariable ?m s.t. pm ?m is true.

                                                                                          Equations
                                                                                          Instances For
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            @[export lean_mk_metavar_ctx]
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For

                                                                                              Low level API for adding/declaring metavariable declarations. It is used to implement actions in the monads MetaM, ElabM and TacticM. It should not be used directly since the argument (mvarId : MVarId) is assumed to be "unique".

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                Equations
                                                                                                Instances For

                                                                                                  Low level API for adding/declaring universe level metavariable declarations. It is used to implement actions in the monads MetaM, ElabM and TacticM. It should not be used directly since the argument (mvarId : MVarId) is assumed to be "unique".

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For

                                                                                                      Set the metavariable user facing name.

                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For

                                                                                                        Low-level version of setMVarUserName. It does not update the table userNames. Thus, findUserName? cannot see the modification. It is meant for mkForallFVars' where we temporarily set the user facing name of metavariables to get more meaningful binder names.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For

                                                                                                          Update the type of the given metavariable. This function assumes the new type is definitionally equal to the current one

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                  • Lean.MetavarContext.instMonadMCtxStateRefT'MetavarContextST = { getMCtx := get, modifyMCtx := modify }
                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.

                                                                                                                  MkBinding and elimMVarDepsAux are mutually recursive, but cache is only used at elimMVarDepsAux. We use a single state object for convenience.

                                                                                                                  We have a NameGenerator because we need to generate fresh auxiliary metavariables.

                                                                                                                  Instances For
                                                                                                                    • mainModule : Lake.Name
                                                                                                                    • preserveOrder : Bool
                                                                                                                    • binderInfoForMVars : Lean.BinderInfo

                                                                                                                      When creating binders for abstracted metavariables, we use the following BinderInfo.

                                                                                                                    • mvarIdsToAbstract : Lean.MVarIdSet

                                                                                                                      Set of unassigned metavariables being abstracted.

                                                                                                                    Instances For
                                                                                                                      Equations
                                                                                                                      • One or more equations did not get rendered due to their size.

                                                                                                                      Given toRevert an array of free variables s.t. lctx contains their declarations, return a new array of free variables that contains toRevert and all variables in lctx that may depend on toRevert.

                                                                                                                      Remark: the result is sorted by LocalDecl indices.

                                                                                                                      Remark: We used to throw an Exception.revertFailure exception when an auxiliary declaration had to be reversed. Recall that auxiliary declarations are created when compiling (mutually) recursive definitions. The revertFailure due to auxiliary declaration dependency was originally introduced in Lean3 to address issue https://github.com/leanprover/lean/issues/1258. In Lean4, this solution is not satisfactory because all definitions/theorems are potentially recursive. So, even a simple (incomplete) definition such as

                                                                                                                      variables {α : Type} in
                                                                                                                      def f (a : α) : List α :=
                                                                                                                      _
                                                                                                                      

                                                                                                                      would trigger the Exception.revertFailure exception. In the definition above, the elaborator creates the auxiliary definition f : {α : Type} → List α. The _ is elaborated as a new fresh variable ?m that contains α : Type, a : α, and f : α → List α in its context, When we try to create the lambda fun {α : Type} (a : α) => ?m, we first need to create an auxiliary ?n which does not contain α and a in its context. That is, we create the metavariable ?n : {α : Type} → (a : α) → (f : α → List α) → List α, add the delayed assignment ?n #[α, a, f] := ?m, and create the lambda fun {α : Type} (a : α) => ?n α a f. See elimMVarDeps for more information. If we kept using the Lean3 approach, we would get the Exception.revertFailure exception because we are reverting the auxiliary definition f.

                                                                                                                      Note that https://github.com/leanprover/lean/issues/1258 is not an issue in Lean4 because we have changed how we compile recursive definitions.

                                                                                                                      Equations
                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                      Instances For

                                                                                                                        Create a new LocalContext by removing the free variables in toRevert from lctx. We use this function when we create auxiliary metavariables at elimMVarDepsAux.

                                                                                                                        Equations
                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                        Instances For

                                                                                                                          Revert the variables xs from the local context of mvarId, returning an expression representing the (new) reverted metavariable and the list of variables that were actually reverted (this list will include any forward dependencies).

                                                                                                                          See details in the comment at the top of the file.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[inline]

                                                                                                                            Similar to Expr.abstractRange, but handles metavariables correctly. It uses elimMVarDeps to ensure e and the type of the free variables xs do not contain a metavariable ?m s.t. local context of ?m contains a free variable in xs.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[specialize #[]]

                                                                                                                              Similar to LocalContext.mkBinding, but handles metavariables correctly. If usedOnly == true then forall and lambda expressions are created only for used variables. If usedLetOnly == true then let expressions are created only for used (let-) variables.

                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For
                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      @[inline]
                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        @[inline]
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[inline]
                                                                                                                                          Equations
                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                          Instances For
                                                                                                                                            @[inline]
                                                                                                                                            Equations
                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                            Instances For

                                                                                                                                              isWellFormed lctx e returns true iff

                                                                                                                                              • All locals in e are declared in lctx
                                                                                                                                              • All metavariables ?m in e have a local context which is a subprefix of lctx or are assigned, and the assignment is well-formed.
                                                                                                                                              Instances For
                                                                                                                                                Equations
                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                Instances For
                                                                                                                                                  def Lean.MetavarContext.levelMVarToParam (mctx : Lean.MetavarContext) (alreadyUsedPred : Lake.NameBool) (except : Lean.LMVarIdBool) (e : Lean.Expr) (paramNamePrefix : optParam Lake.Name `u) (nextParamIdx : optParam Nat 1) :
                                                                                                                                                  Equations
                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                  Instances For