feat: add zetaHave/letToHave simp options (#8788)

This PR adds the `zetaHave` and `letToHave` options to `simp`.
Implementations will appear in future PRs.

Author: kmill

src/Init/MetaTypes.lean

@@ -57,8 +57,9 @@ It is immediately converted to `Lean.Meta.Simp.Config` by `Lean.Elab.Tactic.elab
 -/
 structure Config where
   /--
-  When `true` (default: `true`), performs zeta reduction of let expressions.
+  When `true` (default: `true`), performs zeta reduction of `let` and `have` expressions.
   That is, `let x := v; e[x]` reduces to `e[v]`.
+  If `zetaHave` is `false` then `have` expressions are not zeta reduced.
   See also `zetaDelta`.
   -/
   zeta              : Bool := true
@@ -107,7 +108,8 @@ structure Config where
   unfoldPartialApp  : Bool := false
   /--
   When `true` (default: `false`), local definitions are unfolded.
-  That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
+  That is, given a local context containing `x : t := e`, then the free variable `x` reduces to `e`.
+  Otherwise, `x` must be provided as a `simp` argument.
   -/
   zetaDelta         : Bool := false
   /--
@@ -116,10 +118,17 @@ structure Config where
   -/
   index             : Bool := true
   /--
-  When `true` (default : `true`), then simps will remove unused let-declarations:
+  When `true` (default : `true`), then `simp` will remove unused `let` and `have` expressions:
   `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
   -/
   zetaUnused : Bool := true
+  /--
+  (Unimplemented)
+  When `false` (default: `true`), then disables zeta reduction of `have` expressions.
+  If `zeta` is `false`, then this option has no effect.
+  Unused `have`s are still removed if `zeta` or `zetaUnused` are true.
+  -/
+  zetaHave : Bool := true
   deriving Inhabited, BEq
 
 end DSimp
@@ -161,8 +170,9 @@ structure Config where
   -/
   singlePass        : Bool := false
   /--
-  When `true` (default: `true`), performs zeta reduction of let expressions.
+  When `true` (default: `true`), performs zeta reduction of `let` and `have` expressions.
   That is, `let x := v; e[x]` reduces to `e[v]`.
+  If `zetaHave` is `false` then `have` expressions are not zeta reduced.
   See also `zetaDelta`.
   -/
   zeta              : Bool := true
@@ -226,7 +236,8 @@ structure Config where
   unfoldPartialApp  : Bool := false
   /--
   When `true` (default: `false`), local definitions are unfolded.
-  That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
+  That is, given a local context containing `x : t := e`, then the free variable `x` reduces to `e`.
+  Otherwise, `x` must be provided as a `simp` argument.
   -/
   zetaDelta         : Bool := false
   /--
@@ -240,7 +251,7 @@ structure Config where
   -/
   implicitDefEqProofs : Bool := true
   /--
-  When `true` (default : `true`), then simps will remove unused let-declarations:
+  When `true` (default : `true`), then `simp` will remove unused `let` and `have` expressions:
   `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
   -/
   zetaUnused : Bool := true
@@ -249,6 +260,19 @@ structure Config where
   convert them into `simp` exceptions.
   -/
   catchRuntime : Bool := true
+  /--
+  (Unimplemented)
+  When `false` (default: `true`), then disables zeta reduction of `have` expressions.
+  If `zeta` is `false`, then this option has no effect.
+  Unused `have`s are still removed if `zeta` or `zetaUnused` are true.
+  -/
+  zetaHave : Bool := true
+  /--
+  (Unimplemented)
+  When `true` (default : `true`), then `simp` will attempt to transform `let`s into `have`s
+  if they are non-dependent. This only applies when `zeta := false`.
+  -/
+  letToHave : Bool := true
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`
@@ -270,6 +294,7 @@ def neutralConfig : Simp.Config := {
   ground            := false
   zetaDelta         := false
   zetaUnused        := false
+  letToHave         := false
 }
 
 structure NormCastConfig extends Simp.Config where