feat: zetaUnused option (option only) (#6754)

This PR adds the `+zetaUnused` option.

Implementation to follow after the stage0 update.

src/Init/MetaTypes.lean

@@ -109,6 +109,11 @@ structure Config where
   to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
   -/
   index             : Bool := true
+  /--
+  When `true` (default : `true`), then simps will remove unused let-declarations:
+  `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
+  -/
+  zetaUnused : Bool := true
   deriving Inhabited, BEq
 
 end DSimp
@@ -228,6 +233,11 @@ structure Config where
   input and output terms are definitionally equal.
   -/
   implicitDefEqProofs : Bool := true
+  /--
+  When `true` (default : `true`), then simps will remove unused let-declarations:
+  `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
+  -/
+  zetaUnused : Bool := true
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`
@@ -248,6 +258,7 @@ def neutralConfig : Simp.Config := {
   autoUnfold        := false
   ground            := false
   zetaDelta         := false
+  zetaUnused        := false
 }
 
 structure NormCastConfig extends Simp.Config where

src/Lean/Meta/Basic.lean

@@ -175,6 +175,11 @@ structure Config where
   Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
   -/
   zetaDelta : Bool := true
+  /--
+  Zeta reduction for unused let-declarations: `let x := v; e` reduces to `e` when `x` does not occur
+  in `e`.
+  -/
+  zetaUnused : Bool := true
   deriving Inhabited, Repr
 
 /-- Convert `isDefEq` and `WHNF` relevant parts into a key for caching results -/

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -134,6 +134,7 @@ private def mkIndexConfig (c : Config) : MetaM ConfigWithKey := do
     beta         := c.beta
     iota         := c.iota
     zeta         := c.zeta
+    zetaUnused   := c.zetaUnused
     zetaDelta    := c.zetaDelta
     etaStruct    := c.etaStruct
     /-
@@ -153,6 +154,7 @@ private def mkMetaConfig (c : Config) : MetaM ConfigWithKey := do
     beta         := c.beta
     zeta         := c.zeta
     iota         := c.iota
+    zetaUnused   := c.zetaUnused
     zetaDelta    := c.zetaDelta
     etaStruct    := c.etaStruct
     proj         := if c.proj then .yesWithDelta else .no

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0!
+
 namespace lean {
 options get_default_options() {
     options opts;