From 868a217202016cc3ce11adb85615e1e2baaa1e9e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Dec 2019 10:04:37 -0800 Subject: [PATCH] doc: revise design for creating let-expressions of terms containing metavariables TODO: implement :) The goal is to fix accidental zeta-expansions occurring when creating let-declarations where the body of the expression contains syntheticOpaque metavariables. --- src/Init/Lean/MetavarContext.lean | 37 ++++++++++++++++++++++--------- 1 file changed, 26 insertions(+), 11 deletions(-) diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean index 4fcd6bc183..eedd308a16 100644 --- a/src/Init/Lean/MetavarContext.lean +++ b/src/Init/Lean/MetavarContext.lean @@ -123,8 +123,8 @@ 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, `?m` is synthetic. Assume the type of `?m` is -`A`. Then, in both cases we create an auxiliary metavariable `?n` with -type `forall xs => A`, and local context := local context of `?m` - `xs`. +`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 @@ -134,7 +134,8 @@ In both cases, we produce the term `fun xs => t[?n xs]` 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 assign `fun xs => s` to `?n`. + does not contain metavariables, we replace any occurrence + `?n ts` with `s[xs := ts]`. Gruesome details: @@ -143,15 +144,29 @@ Gruesome details: process above is recursive. We claim it terminates because we keep creating new metavariables with smaller local contexts. - - The type of variables `xs` may contain metavariables, and we must - recursively apply the process above. Again, we claim the process - terminates because the metavariables is ocurring in the types of - `xs`, they must have 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` contatins `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]`. - - We can only assign `fun xs => s` to `?n` in case 2, the types of - `xs` must also not contain metavariables. To be precise, it is - sufficient they do not contain metavariables with local contexts - containing any of the `xs`s. + 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