feat: zeta-expand auxiliary let-declarations and mark to_default as reducible

src/Lean/Elab/Structure.lean

@@ -467,7 +467,9 @@ private def addDefaults (ref : Syntax) (mctx : MetavarContext) (lctx : LocalCont
 liftTermElabM none $ Term.withLocalContext lctx localInsts do
   Term.setMCtx mctx;
   defaultAuxDecls.forM fun ⟨declName, type, value⟩ => do
-    _ ← Term.mkAuxDefinition ref declName type value;
+    let zeta := true; -- expand `let-declarations`
+    _ ← Term.mkAuxDefinition ref declName type value zeta;
+    Term.modifyEnv fun env => setReducibilityStatus env declName ReducibilityStatus.reducible;
     pure ()
 
 /-

src/Lean/Elab/Term.lean

@@ -132,6 +132,7 @@ def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
 
 def setEnv (env : Environment) : TermElabM Unit := modify $ fun s => { s with env := env }
 def setMCtx (mctx : MetavarContext) : TermElabM Unit := modify $ fun s => { s with mctx := mctx }
+@[inline] def modifyEnv (f : Environment → Environment) : TermElabM Unit := modify $ fun s => { s with env := f s.env }
 
 def addContext (msg : MessageData) : TermElabM MessageData := do
 env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
@@ -989,12 +990,12 @@ match env.compileDecl opts decl with
 | Except.ok env    => setEnv env
 | Except.error kex => throwError ref (kex.toMessageData opts)
 
-def mkAuxDefinition (ref : Syntax) (declName : Name) (type : Expr) (value : Expr) : TermElabM Expr := do
+def mkAuxDefinition (ref : Syntax) (declName : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : TermElabM Expr := do
 env ← getEnv;
 opts ← getOptions;
 mctx ← getMCtx;
 lctx ← getLCtx;
-match Lean.mkAuxDefinition env opts mctx lctx declName type value with
+match Lean.mkAuxDefinition env opts mctx lctx declName type value zeta with
 | Except.error ex    => throwError ref (ex.toMessageData opts)
 | Except.ok (r, env) => do
   setEnv env;

src/Lean/Util/Closure.lean

@@ -14,6 +14,7 @@ namespace Closure
 structure Context :=
 (mctx      : MetavarContext)
 (lctxInput : LocalContext)
+(zeta      : Bool) -- if `true` let-variables are expanded
 
 structure State :=
 (lctxOutput    : LocalContext := {})
@@ -138,11 +139,14 @@ partial def collectExprAux : Expr → ClosureM Expr
       x    ← mkLocalDecl userName type;
       modify $ fun s => { s with exprClosure := s.exprClosure.push e };
       pure x
-    | some (LocalDecl.ldecl _ _ userName type value) => do
-      type  ← collect type;
-      value ← collect value;
-      -- Note that let-declarations do not need to be provided to the closure being constructed.
-      mkLetDecl userName type value
+    | some (LocalDecl.ldecl _ _ userName type value) =>
+      if ctx.zeta then
+        collect value
+      else do
+        type  ← collect type;
+        value ← collect value;
+        -- Note that let-declarations do not need to be provided to the closure being constructed.
+        mkLetDecl userName type value
   | e => pure e
 
 def collectExpr (e : Expr) : ClosureM Expr :=
@@ -155,7 +159,7 @@ structure MkClosureResult :=
 (levelClosure : Array Level)
 (exprClosure  : Array Expr)
 
-def mkClosure (mctx : MetavarContext) (lctx : LocalContext) (type : Expr) (value : Expr) : Except String MkClosureResult :=
+def mkClosure (mctx : MetavarContext) (lctx : LocalContext) (type : Expr) (value : Expr) (zeta : Bool := false) : Except String MkClosureResult :=
 let shareCommonTypeValue : Std.ShareCommonM (Expr × Expr) := do {
   type  ← Std.withShareCommon type;
   value ← Std.withShareCommon value;
@@ -167,7 +171,7 @@ let mkTypeValue : ClosureM (Expr × Expr) := do {
   value ← collectExpr value;
   pure (type, value)
 };
-match (mkTypeValue { mctx := mctx, lctxInput := lctx }).run {} with
+match (mkTypeValue { mctx := mctx, lctxInput := lctx, zeta := zeta }).run {} with
 | EStateM.Result.ok (type, value) s =>
   let fvars := s.lctxOutput.getFVars;
   let type  := s.lctxOutput.mkForall fvars type;
@@ -183,8 +187,8 @@ match (mkTypeValue { mctx := mctx, lctxInput := lctx }).run {} with
 end Closure
 
 def mkAuxDefinition (env : Environment) (opts : Options) (mctx : MetavarContext) (lctx : LocalContext) (name : Name) (type : Expr) (value : Expr)
-    : Except KernelException (Expr × Environment) :=
-match Closure.mkClosure mctx lctx type value with
+    (zeta : Bool := false) : Except KernelException (Expr × Environment) :=
+match Closure.mkClosure mctx lctx type value zeta with
 | Except.error ex  => throw $ KernelException.other ex
 | Except.ok result => do
   let decl := Declaration.defnDecl {