feat: optimized simp routine for let telescopes

This PR adds the following features to `simp`:
- A routine for simplifying `let` telescopes, like what #6220 did for `letFun` telescopes. Furthermore, simp converts `letFun`s into `have`s (nondependent lets), and we remove the #6220 routine.
- A `+letToHave` configuration option (enabled by default) that converts lets into haves when possible, when `-zeta` is set. Previosuly Lean would need to do a full typecheck the bodies of `let`s, but the `letToHave` procedure can be faster, and it modifies the `let`s in an entire expression at once.
- A `+zetaHave` configuration option, to turn off zeta reduction of `have`s specifically. The motivation is that dependent `let`s can only be dsimped by let, so zeta reducing just nondependent lets is a reasonable way to make progress.

Author: kmill

src/Init/MetaTypes.lean

@@ -123,7 +123,6 @@ structure Config where
   -/
   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.
@@ -261,14 +260,12 @@ structure Config where
   -/
   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`.
   -/

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

@@ -176,6 +176,8 @@ private def nonPropHaveToLet (e : Expr) : MetaM Expr := do
 def preprocess (e : Expr) : MetaM Simp.Result := do
   unless wf.preprocess.get (← getOptions) do
     return { expr := e }
+  -- Transform `let`s to `have`s to enable `simp` entering let bodies.
+  let e ← letToHave e
   lambdaTelescope e fun xs _ => do
     -- Annotate all xs with `wfParam`
     let xs' ← xs.mapM mkWfParam

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

@@ -3,7 +3,7 @@ def f (x : Nat) := x
 def test : (λ x => f x)
            =
            (λ x : Nat =>
-             let foo := λ y => id (id y)
+             have foo := λ y => id (id y)
              foo x) := by
   conv =>
     pattern (id _)

tests/lean/convPatternAtLetIssue.lean

@@ -8,7 +8,7 @@ example (f : Nat → Nat) : f x = 0 → f x + 1 = y := by
   guard_target =ₛ f x = 0 → 1 = y
   sorry
 
-example (f : Nat → Nat) : let _  : f x = 0 := sorryAx _ false; f x + 1 = y := by
+example (f : Nat → Nat) : have _  : f x = 0 := sorryAx _ false; f x + 1 = y := by
   simp (config := { contextual := true, zeta := false, zetaUnused := false })
   guard_target =ₛ have _  : f x = 0 := sorryAx _ false; 1 = y
   sorry
@@ -45,7 +45,7 @@ example : (if p x then g x else g x + 1) + g x = y := by
   guard_target =ₛ (if p x then x else g x + 1) + g x = y
   sorry
 
-example : (let _  : p x := sorryAx _ false; g x + 1 = y) ↔ g x = y := by
+example : (have _  : p x := sorryAx _ false; g x + 1 = y) ↔ g x = y := by
   simp (config := { zeta := false, zetaUnused := false }) (discharger := assumption)
   guard_target =ₛ (have _  : p x := sorryAx _ false; x + 1 = y) ↔ g x = y
   sorry