From 457d33d660c349505824ff70443329ef981dc9c6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Feb 2024 12:13:20 -0800 Subject: [PATCH] feat: configuration options `zeta` and `zetaDelta` TODO: bootstrapping issues, set `zetaDelta := false` in the simplifier. --- src/Lean/Elab/MutualDef.lean | 8 ++-- src/Lean/Elab/Structure.lean | 2 +- src/Lean/Elab/Tactic/ElabTerm.lean | 2 +- src/Lean/Meta/AbstractNestedProofs.lean | 6 +-- src/Lean/Meta/Basic.lean | 40 ++++++++-------- src/Lean/Meta/Closure.lean | 52 ++++++++++----------- src/Lean/Meta/Match/Match.lean | 2 +- src/Lean/Meta/Tactic/Simp/Main.lean | 2 +- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 2 +- src/Lean/Meta/Tactic/Simp/Types.lean | 4 +- src/Lean/Meta/Transform.lean | 1 + src/Lean/Meta/WHNF.lean | 6 +-- 12 files changed, 65 insertions(+), 62 deletions(-) diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 041414a97e..e14c4eb993 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -531,8 +531,8 @@ private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT Closu let toProcess ← pushLocalDecl toProcess fvarId userName type bi k mkClosureForAux toProcess | .ldecl _ _ userName type val _ k => - let zetaFVarIds ← getZetaFVarIds - if !zetaFVarIds.contains fvarId then + let zetaDeltaFVarIds ← getZetaDeltaFVarIds + if !zetaDeltaFVarIds.contains fvarId then /- Non-dependent let-decl. See comment at src/Lean/Meta/Closure.lean -/ let toProcess ← pushLocalDecl toProcess fvarId userName type .default k mkClosureForAux toProcess @@ -696,8 +696,8 @@ def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mai let letRecsToLift := letRecsToLift.toArray let mainFVarIds := mainFVars.map Expr.fvarId! let recFVarIds := (letRecsToLift.map fun toLift => toLift.fvarId) ++ mainFVarIds - resetZetaFVarIds - withTrackingZeta do + resetZetaDeltaFVarIds + withTrackingZetaDelta do -- By checking `toLift.type` and `toLift.val` we populate `zetaFVarIds`. See comments at `src/Lean/Meta/Closure.lean`. let letRecsToLift ← letRecsToLift.mapM fun toLift => withLCtx toLift.lctx toLift.localInstances do Meta.check toLift.type diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 2406b49bad..a46742b8fa 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -739,7 +739,7 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name × throwError "invalid default value for field, it contains metavariables{indentExpr value}" /- The identity function is used as "marker". -/ let value ← mkId value - discard <| mkAuxDefinition declName type value (zeta := true) + discard <| mkAuxDefinition declName type value (zetaDelta := true) setReducibleAttribute declName /-- diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 6c633f18ec..3ce0864fbb 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -356,7 +356,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId /-- Make sure `expectedType` does not contain free and metavariables. - It applies zeta-reduction to eliminate let-free-vars. + It applies zeta and zetaDelta-reduction to eliminate let-free-vars. -/ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do let mut expectedType ← instantiateMVars expectedType diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean index de29d93ca6..3779a2679c 100644 --- a/src/Lean/Meta/AbstractNestedProofs.lean +++ b/src/Lean/Meta/AbstractNestedProofs.lean @@ -35,10 +35,10 @@ private def mkAuxLemma (e : Expr) : M Expr := do let s ← get let lemmaName ← mkAuxName (ctx.baseName ++ `proof) s.nextIdx modify fun s => { s with nextIdx := s.nextIdx + 1 } - /- We turn on zeta-expansion to make sure we don't need to perform an expensive `check` step to - identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zeta expansion step. + /- We turn on zetaDelta-expansion to make sure we don't need to perform an expensive `check` step to + identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zetaDelta expansion step. It a benchmark created by @selsam, The extra `check` step was a bottleneck. -/ - mkAuxTheoremFor lemmaName e (zeta := true) + mkAuxTheoremFor lemmaName e (zetaDelta := true) partial def visit (e : Expr) : M Expr := do if e.isAtomic then diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index a7c4336fd0..48abfe834e 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -96,17 +96,17 @@ structure Config where -/ transparency : TransparencyMode := TransparencyMode.default /-- - When `trackZeta = true`, we track all free variables that have been zeta-expanded. + When `trackZetaDelta = true`, we track all free variables that have been zetaDelta-expanded. That is, suppose the local context contains - the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaFVarIds`. - We use `trackZeta` to discover which let-declarations `let x := v; e` can be represented as `(fun x => e) v`. + the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaDeltaFVarIds`. + We use `trackZetaDelta` to discover which let-declarations `let x := v; e` can be represented as `(fun x => e) v`. When we find these declarations we set their `nonDep` flag with `true`. To find these let-declarations in a given term `s`, we - 1- Reset `State.zetaFVarIds` - 2- Set `trackZeta := true` + 1- Reset `State.zetaDeltaFVarIds` + 2- Set `trackZetaDelta := true` 3- Type-check `s`. -/ - trackZeta : Bool := false + trackZetaDelta : Bool := false /-- Eta for structures configuration mode. -/ etaStruct : EtaStructMode := .all @@ -261,12 +261,12 @@ structure PostponedEntry where `MetaM` monad state. -/ structure State where - mctx : MetavarContext := {} - cache : Cache := {} - /-- When `trackZeta == true`, then any let-decl free variable that is zeta expansion performed by `MetaM` is stored in `zetaFVarIds`. -/ - zetaFVarIds : FVarIdSet := {} + mctx : MetavarContext := {} + cache : Cache := {} + /-- When `trackZetaDelta == true`, then any let-decl free variable that is zetaDelta expansion performed by `MetaM` is stored in `zetaDeltaFVarIds`. -/ + zetaDeltaFVarIds : FVarIdSet := {} /-- Array of postponed universe level constraints -/ - postponed : PersistentArray PostponedEntry := {} + postponed : PersistentArray PostponedEntry := {} deriving Inhabited /-- @@ -330,7 +330,7 @@ protected def saveState : MetaM SavedState := /-- Restore backtrackable parts of the state. -/ def SavedState.restore (b : SavedState) : MetaM Unit := do Core.restore b.core - modify fun s => { s with mctx := b.meta.mctx, zetaFVarIds := b.meta.zetaFVarIds, postponed := b.meta.postponed } + modify fun s => { s with mctx := b.meta.mctx, zetaDeltaFVarIds := b.meta.zetaDeltaFVarIds, postponed := b.meta.postponed } instance : MonadBacktrack SavedState MetaM where saveState := Meta.saveState @@ -374,7 +374,7 @@ section Methods variable [MonadControlT MetaM n] [Monad n] @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit := - modify fun { mctx, cache, zetaFVarIds, postponed } => { mctx, cache := f cache, zetaFVarIds, postponed } + modify fun { mctx, cache, zetaDeltaFVarIds, postponed } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed } @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit := modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩ @@ -394,11 +394,11 @@ def getLocalInstances : MetaM LocalInstances := def getConfig : MetaM Config := return (← read).config -def resetZetaFVarIds : MetaM Unit := - modify fun s => { s with zetaFVarIds := {} } +def resetZetaDeltaFVarIds : MetaM Unit := + modify fun s => { s with zetaDeltaFVarIds := {} } -def getZetaFVarIds : MetaM FVarIdSet := - return (← get).zetaFVarIds +def getZetaDeltaFVarIds : MetaM FVarIdSet := + return (← get).zetaDeltaFVarIds /-- Return the array of postponed universe level constraints. -/ def getPostponed : MetaM (PersistentArray PostponedEntry) := @@ -790,10 +790,10 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : mapMetaM <| withReader (fun ctx => { ctx with config := f ctx.config }) /-- -Executes `x` tracking zeta reductions `Config.trackZeta := true` +Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true` -/ -@[inline] def withTrackingZeta (x : n α) : n α := - withConfig (fun cfg => { cfg with trackZeta := true }) x +@[inline] def withTrackingZetaDelta (x : n α) : n α := + withConfig (fun cfg => { cfg with trackZetaDelta := true }) x @[inline] def withoutProofIrrelevance (x : n α) : n α := withConfig (fun cfg => { cfg with proofIrrelevance := false }) x diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index 7ac2972f4a..6729197b2f 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -56,14 +56,14 @@ def aux := fun (y : Nat) => h (g y) Note that in this particular case, it is safe to lambda abstract the let-varible `y`. This module uses the following approach to decide whether it is safe or not to lambda abstract a let-variable. -1) We enable zeta-expansion tracking in `MetaM`. That is, whenever we perform type checking - if a let-variable needs to zeta expanded, we store it in the set `zetaFVarIds`. - We say a let-variable is zeta expanded when we replace it with its value. +1) We enable zetaDelta-expansion tracking in `MetaM`. That is, whenever we perform type checking + if a let-variable needs to zetaDelta expanded, we store it in the set `zetaDeltaFVarIds`. + We say a let-variable is zetaDelta expanded when we replace it with its value. 2) We use the `MetaM` type checker `check` to type check the expression we want to close, and the type of the binders. -3) If a let-variable is not in `zetaFVarIds`, we lambda abstract it. +3) If a let-variable is not in `zetaDeltaFVarIds`, we lambda abstract it. -Remark: We still use let-expressions for let-variables in `zetaFVarIds`, but we move the +Remark: We still use let-expressions for let-variables in `zetaDeltaFVarIds`, but we move the `let` inside the lambdas. The idea is to make sure the auxiliary definition does not have an interleaving of `lambda` and `let` expressions. Thus, if the let-variable occurs in the type of one of the lambdas, we simply zeta-expand it there. @@ -89,7 +89,7 @@ let n : Nat := 20; (let y : {v // v=n} := {val := 20, property := ex._proof_1}; y.val+n+f x, z+10) ``` -BTW, this module also provides the `zeta : Bool` flag. When set to true, it +BTW, this module also provides the `zetaDelta : Bool` flag. When set to true, it expands all let-variables occurring in the target expression. -/ @@ -102,7 +102,7 @@ structure ToProcessElement where deriving Inhabited structure Context where - zeta : Bool + zetaDelta : Bool structure State where visitedLevel : LevelMap Level := {} @@ -165,9 +165,9 @@ def collectLevel (u : Level) : ClosureM Level := do def preprocess (e : Expr) : ClosureM Expr := do let e ← instantiateMVars e let ctx ← read - -- If we are not zeta-expanding let-decls, then we use `check` to find + -- If we are not zetaDelta-expanding let-decls, then we use `check` to find -- which let-decls are dependent. We say a let-decl is dependent if its lambda abstraction is type incorrect. - if !ctx.zeta then + if !ctx.zetaDelta then check e pure e @@ -207,7 +207,7 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do } return mkFVar newFVarId | Expr.fvar fvarId => - match (← read).zeta, (← fvarId.getValue?) with + match (← read).zetaDelta, (← fvarId.getValue?) with | true, some value => collect (← preprocess value) | _, _ => let newFVarId ← mkFreshFVarId @@ -259,14 +259,14 @@ partial def process : ClosureM Unit := do pushFVarArg (mkFVar fvarId) process | .ldecl _ _ userName type val _ _ => - let zetaFVarIds ← getZetaFVarIds - if !zetaFVarIds.contains fvarId then + let zetaDeltaFVarIds ← getZetaDeltaFVarIds + if !zetaDeltaFVarIds.contains fvarId then /- Non-dependent let-decl - Recall that if `fvarId` is in `zetaFVarIds`, then we zeta-expanded it + Recall that if `fvarId` is in `zetaDeltaFVarIds`, then we zetaDelta-expanded it during type checking (see `check` at `collectExpr`). - Our type checker may zeta-expand declarations that are not needed, but this + Our type checker may zetaDelta-expand declarations that are not needed, but this check is conservative, and seems to work well in practice. -/ pushLocalDecl newFVarId userName type pushFVarArg (mkFVar fvarId) @@ -315,15 +315,15 @@ structure MkValueTypeClosureResult where exprArgs : Array Expr def mkValueTypeClosureAux (type : Expr) (value : Expr) : ClosureM (Expr × Expr) := do - resetZetaFVarIds - withTrackingZeta do + resetZetaDeltaFVarIds + withTrackingZetaDelta do let type ← collectExpr type let value ← collectExpr value process pure (type, value) -def mkValueTypeClosure (type : Expr) (value : Expr) (zeta : Bool) : MetaM MkValueTypeClosureResult := do - let ((type, value), s) ← ((mkValueTypeClosureAux type value).run { zeta := zeta }).run {} +def mkValueTypeClosure (type : Expr) (value : Expr) (zetaDelta : Bool) : MetaM MkValueTypeClosureResult := do + let ((type, value), s) ← ((mkValueTypeClosureAux type value).run { zetaDelta }).run {} let newLocalDecls := s.newLocalDecls.reverse ++ s.newLocalDeclsForMVars let newLetDecls := s.newLetDecls.reverse let type := mkForall newLocalDecls (mkForall newLetDecls type) @@ -344,8 +344,8 @@ end Closure A "closure" is computed, and a term of the form `name.{u_1 ... u_n} t_1 ... t_m` is returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on, and `t_j`s are free and meta variables `type` and `value` depend on. -/ -def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) (compile : Bool := true) : MetaM Expr := do - let result ← Closure.mkValueTypeClosure type value zeta +def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false) (compile : Bool := true) : MetaM Expr := do + let result ← Closure.mkValueTypeClosure type value zetaDelta let env ← getEnv let decl := Declaration.defnDecl { name := name @@ -361,16 +361,16 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := f return mkAppN (mkConst name result.levelArgs.toList) result.exprArgs /-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/ -def mkAuxDefinitionFor (name : Name) (value : Expr) (zeta : Bool := false) : MetaM Expr := do +def mkAuxDefinitionFor (name : Name) (value : Expr) (zetaDelta : Bool := false) : MetaM Expr := do let type ← inferType value let type := type.headBeta - mkAuxDefinition name type value (zeta := zeta) + mkAuxDefinition name type value (zetaDelta := zetaDelta) /-- Create an auxiliary theorem with the given name, type and value. It is similar to `mkAuxDefinition`. -/ -def mkAuxTheorem (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : MetaM Expr := do - let result ← Closure.mkValueTypeClosure type value zeta +def mkAuxTheorem (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false) : MetaM Expr := do + let result ← Closure.mkValueTypeClosure type value zetaDelta let env ← getEnv let decl := if env.hasUnsafe result.type || env.hasUnsafe result.value then @@ -396,9 +396,9 @@ def mkAuxTheorem (name : Name) (type : Expr) (value : Expr) (zeta : Bool := fals /-- Similar to `mkAuxTheorem`, but infers the type of `value`. -/ -def mkAuxTheoremFor (name : Name) (value : Expr) (zeta : Bool := false) : MetaM Expr := do +def mkAuxTheoremFor (name : Name) (value : Expr) (zetaDelta : Bool := false) : MetaM Expr := do let type ← inferType value let type := type.headBeta - mkAuxTheorem name type value zeta + mkAuxTheorem name type value zetaDelta end Lean.Meta diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 62e8f1bf6d..3834316cf6 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -682,7 +682,7 @@ builtin_initialize matcherExt : EnvExtension (PHashMap (Expr × Bool) Name) ← def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (Expr × Option (MatcherInfo → MetaM Unit)) := do trace[Meta.Match.debug] "{name} : {type} := {value}" let compile := bootstrap.genMatcherCode.get (← getOptions) - let result ← Closure.mkValueTypeClosure type value (zeta := false) + let result ← Closure.mkValueTypeClosure type value (zetaDelta := false) let env ← getEnv let mkMatcherConst name := mkAppN (mkConst name result.levelArgs.toList) result.exprArgs diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 7732ee5447..4a35305b15 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -76,7 +76,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do reduceProjCont? (← unfoldDefinition? e) private def reduceFVar (cfg : Config) (thms : SimpTheoremsArray) (e : Expr) : MetaM Expr := do - if cfg.zeta || thms.isLetDeclToUnfold e.fvarId! then + if cfg.zetaDelta || thms.isLetDeclToUnfold e.fvarId! then match (← getFVarLocalDecl e).value? with | some v => return v | none => return e diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index 170877bdf0..412005da93 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -165,7 +165,7 @@ structure SimpTheorems where lemmaNames : PHashSet Origin := {} /-- Constants (and let-declaration `FVarId`) to unfold. - When `zeta := false`, the simplifier will expand a let-declaration if it is in this set. + When `zetaDelta := false`, the simplifier will expand a let-declaration if it is in this set. -/ toUnfold : PHashSet Name := {} erased : PHashSet Origin := {} diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 7d3da91d0f..948104a0ea 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -14,7 +14,7 @@ namespace Simp /-- The result of simplifying some expression `e`. -/ structure Result where - /-- The simplified version of `e` -/ + /-- The simplified version of `e` -/ expr : Expr /-- A proof that `$e = $expr`, where the simplified expression is on the RHS. If `none`, the proof is assumed to be `refl`. -/ @@ -483,6 +483,8 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do Return a WHNF configuration for retrieving `[simp]` from the discrimination tree. If user has disabled `zeta` and/or `beta` reduction in the simplifier, we must also disable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281 + +-- TODO: zetaDelta -/ def getDtConfig (cfg : Config) : WhnfCoreConfig := match cfg.beta, cfg.zeta with diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index 1b22604300..4db24ed58c 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -134,6 +134,7 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] | _ => visitPost e visit input |>.run +-- TODO: add options to distinguish zeta and zetaDelta reduction def zetaReduce (e : Expr) : MetaM Expr := do let pre (e : Expr) : MetaM TransformStep := do match e with diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index b2ad977af3..0df12e501f 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -371,9 +371,9 @@ structure WhnfCoreConfig where match decl with | .cdecl .. => return e | .ldecl (value := v) .. => - unless config.zeta do return e - if (← getConfig).trackZeta then - modify fun s => { s with zetaFVarIds := s.zetaFVarIds.insert fvarId } + unless config.zetaDelta do return e + if (← getConfig).trackZetaDelta then + modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId } whnfEasyCases v k config | .mvar mvarId => match (← getExprMVarAssignment? mvarId) with