From 5d35e9496ef895339131f00017f2013c10f8edfe Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 6 Dec 2023 09:15:45 +0100 Subject: [PATCH] doc: fix MetavarContext markdown (#3026) I found the documentation page hard to parse, so I figured I should fix this. It's mostly indentation (e.g. in lists), some line breaks and making URLs clickable. --- src/Lean/MetavarContext.lean | 257 ++++++++++++++++++----------------- 1 file changed, 135 insertions(+), 122 deletions(-) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index db4374cf3e07..c9fc80579601 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -15,76 +15,79 @@ assignments. It is used in the elaborator, tactic framework, unifier the requirements imposed by these modules. - We may invoke TC while executing `isDefEq`. We need this feature to -be able to solve unification problems such as: -``` -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`. + WellFoundedRelationbe able to solve unification problems such as: + ``` + 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`. - TC uses `isDefEq`, and `isDefEq` may create TC problems as shown -above. Thus, we may have nested TC problems. + above. Thus, we may have nested TC problems. - `isDefEq` extends the local context when going inside binders. Thus, -the local context for nested TC may be an extension of the local -context for outer TC. + the local context for nested TC may be an extension of the local + context for outer TC. - TC should not assign metavariables created by the elaborator, simp, -tactic framework, and outer TC problems. Reason: TC commits to the -first solution it finds. Consider the TC problem `Coe Nat ?x`, -where `?x` is a metavariable created by the caller. There are many -solutions to this problem (e.g., `?x := Int`, `?x := Real`, ...), -and it doesn’t make sense to commit to the first one since TC does -not know the constraints the caller may impose on `?x` after the -TC problem is solved. -Remark: we claim it is not feasible to make the whole system backtrackable, -and allow the caller to backtrack back to TC and ask it for another solution -if the first one found did not work. We claim it would be too inefficient. + tactic framework, and outer TC problems. Reason: TC commits to the + first solution it finds. Consider the TC problem `Coe Nat ?x`, + where `?x` is a metavariable created by the caller. There are many + solutions to this problem (e.g., `?x := Int`, `?x := Real`, ...), + and it doesn’t make sense to commit to the first one since TC does + not know the constraints the caller may impose on `?x` after the + TC problem is solved. + + Remark: we claim it is not feasible to make the whole system backtrackable, + and allow the caller to backtrack back to TC and ask it for another solution + if the first one found did not work. We claim it would be too inefficient. - TC metavariables should not leak outside of TC. Reason: we want to -get rid of them after we synthesize the instance. + get rid of them after we synthesize the instance. - `simp` invokes `isDefEq` for matching the left-hand-side of -equations to terms in our goal. Thus, it may invoke TC indirectly. + equations to terms in our goal. Thus, it may invoke TC indirectly. - In Lean3, we didn’t have to create a fresh pattern for trying to -match the left-hand-side of equations when executing `simp`. We had a -mechanism called "tmp" metavariables. It avoided this overhead, but it -created many problems since `simp` may indirectly call TC which may -recursively call TC. Moreover, we may want to allow TC to invoke -tactics in the future. Thus, when `simp` invokes `isDefEq`, it may indirectly invoke -a tactic and `simp` itself. The Lean3 approach assumed that -metavariables were short-lived, this is not true in Lean4, and to some -extent was also not true in Lean3 since `simp`, in principle, could -trigger an arbitrary number of nested TC problems. + match the left-hand-side of equations when executing `simp`. We had a + mechanism called "tmp" metavariables. It avoided this overhead, but it + created many problems since `simp` may indirectly call TC which may + recursively call TC. Moreover, we may want to allow TC to invoke + tactics in the future. Thus, when `simp` invokes `isDefEq`, it may indirectly invoke + a tactic and `simp` itself. The Lean3 approach assumed that + metavariables were short-lived, this is not true in Lean4, and to some + extent was also not true in Lean3 since `simp`, in principle, could + trigger an arbitrary number of nested TC problems. - Here are some possible call stack traces we could have in Lean3 (and Lean4). -``` -Elaborator (-> TC -> isDefEq)+ -Elaborator -> isDefEq (-> TC -> isDefEq)* -Elaborator -> simp -> isDefEq (-> TC -> isDefEq)* -``` -In Lean4, TC may also invoke tactics in the future. + ``` + Elaborator (-> TC -> isDefEq)+ + Elaborator -> isDefEq (-> TC -> isDefEq)* + Elaborator -> simp -> isDefEq (-> TC -> isDefEq)* + ``` + In Lean4, TC may also invoke tactics in the future. - In Lean3 and Lean4, TC metavariables are not really short-lived. We -solve an arbitrary number of unification problems, and we may have -nested TC invocations. + solve an arbitrary number of unification problems, and we may have + nested TC invocations. - TC metavariables do not share the same local context even in the -same invocation. In the C++ and Lean implementations we use a trick to -ensure they do: -https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L3583-L3594 + same invocation. In the C++ and Lean implementations we use a trick to + ensure they do: + - Metavariables may be natural, synthetic or syntheticOpaque. - a) Natural metavariables may be assigned by unification (i.e., `isDefEq`). - b) Synthetic metavariables may still be assigned by unification, + 1. Natural metavariables may be assigned by unification (i.e., `isDefEq`). + + 2. Synthetic metavariables may still be assigned by unification, but whenever possible `isDefEq` will avoid the assignment. For example, if we have the unification constraint `?m =?= ?n`, where `?m` is synthetic, but `?n` is not, `isDefEq` solves it by using the assignment `?n := ?m`. @@ -94,7 +97,7 @@ https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379 them, and check whether the synthesized result is compatible with the one assigned by `isDefEq`. - c) SyntheticOpaque metavariables are never assigned by `isDefEq`. + 3. SyntheticOpaque metavariables are never assigned by `isDefEq`. That is, the constraint `?n =?= Nat.succ Nat.zero` always fail if `?n` is a syntheticOpaque metavariable. This kind of metavariable is created by tactics such as `intro`. Reason: in the tactic framework, @@ -104,78 +107,80 @@ https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379 This distinction was not precise in Lean3 and produced counterintuitive behavior. For example, the following hack was added in Lean3 to work around one of these issues: - https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L2751 + - When creating lambda/forall expressions, we need to convert/abstract -free variables and convert them to bound variables. Now, suppose we are -trying to create a lambda/forall expression by abstracting free -variable `xs` and a term `t[?m]` which contains a metavariable `?m`, -and the local context of `?m` contains `xs`. The term -``` -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: + free variables and convert them to bound variables. Now, suppose we are + trying to create a lambda/forall expression by abstracting free + variable `xs` and a term `t[?m]` which contains a metavariable `?m`, + and the local context of `?m` contains `xs`. The term + ``` + 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: - When we create the type `forall xs => A` for `?n`, we may - encounter the same issue if `A` contains metavariables. So, the - process above is recursive. We claim it terminates because we keep - creating new metavariables with smaller local contexts. + encounter the same issue if `A` contains metavariables. So, the + process above is recursive. We claim it terminates because we keep + creating new metavariables with smaller local contexts. - Suppose, we have `t[?m]` and we want to create a let-expression by - abstracting a let-decl free variable `x`, and the local context of - `?m` contains `x`. Similarly to the previous case - ``` - 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. + abstracting a let-decl free variable `x`, and the local context of + `?m` contains `x`. Similarly to the previous case + ``` + 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. - We use TC for implementing coercions. Both Joe Hendrix and Reid Barton -reported a nasty limitation. In Lean3, TC will not be used if there are -metavariables in the TC problem. For example, the elaborator will not try -to synthesize `Coe Nat ?x`. This is good, but this constraint is too -strict for problems such as `Coe (Vector Bool ?n) (BV ?n)`. The coercion -exists independently of `?n`. Thus, during TC, we want `isDefEq` to throw -an exception instead of return `false` whenever it tries to assign -a metavariable owned by its caller. The idea is to sign to the caller that -it cannot solve the TC problem at this point, and more information is needed. -That is, the caller must make progress an assign its metavariables before -trying to invoke TC again. - -In Lean4, we are using a simpler design for the `MetavarContext`. + reported a nasty limitation. In Lean3, TC will not be used if there are + metavariables in the TC problem. For example, the elaborator will not try + to synthesize `Coe Nat ?x`. This is good, but this constraint is too + strict for problems such as `Coe (Vector Bool ?n) (BV ?n)`. The coercion + exists independently of `?n`. Thus, during TC, we want `isDefEq` to throw + an exception instead of return `false` whenever it tries to assign + a metavariable owned by its caller. The idea is to sign to the caller that + it cannot solve the TC problem at this point, and more information is needed. + That is, the caller must make progress an assign its metavariables before + trying to invoke TC again. + + In Lean4, we are using a simpler design for the `MetavarContext`. - No distinction between temporary and regular metavariables. @@ -184,6 +189,7 @@ In Lean4, we are using a simpler design for the `MetavarContext`. - MetavarContext also has a `depth` field. - We bump the `MetavarContext` depth when we create a nested problem. + Example: Elaborator (depth = 0) -> Simplifier matcher (depth = 1) -> TC (level = 2) -> TC (level = 3) -> ... - When `MetavarContext` is at depth N, `isDefEq` does not assign variables from `depth < N`. @@ -192,11 +198,12 @@ In Lean4, we are using a simpler design for the `MetavarContext`. - New design even allows us to invoke tactics from TC. -* Main concern -We don't have tmp metavariables anymore in Lean4. Thus, before trying to match -the left-hand-side of an equation in `simp`. We first must bump the level of the `MetavarContext`, -create fresh metavariables, then create a new pattern by replacing the free variable on the left-hand-side with -these metavariables. We are hoping to minimize this overhead by +- Main concern + + We don't have tmp metavariables anymore in Lean4. Thus, before trying to match + the left-hand-side of an equation in `simp`. We first must bump the level of the `MetavarContext`, + create fresh metavariables, then create a new pattern by replacing the free variable on the left-hand-side with + these metavariables. We are hoping to minimize this overhead by - Using better indexing data structures in `simp`. They should reduce the number of time `simp` must invoke `isDefEq`. @@ -480,7 +487,8 @@ def assignDelayedMVar [MonadMCtx m] (mvarId : MVarId) (fvars : Array Expr) (mvar modifyMCtx fun m => { m with dAssignment := m.dAssignment.insert mvarId { fvars, mvarIdPending } } /-! -Notes on artificial eta-expanded terms due to metavariables. +## 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 @@ -491,9 +499,11 @@ all free variables that may be used to "fill" the hole. Suppose, we create a met 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 : Nat → Nat` 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`. -/ @@ -923,7 +933,8 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) 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. + introduced in Lean3 to address issue . + In Lean4, this solution is not satisfactory because all definitions/theorems are potentially recursive. So, even a simple (incomplete) definition such as ``` @@ -939,11 +950,13 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) 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 + Note that is not an issue in Lean4 because we have changed how we compile recursive definitions. -/ def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) : M (Array Expr) := do