feat: optimized simp routine for let telescopes (#8968)

This PR adds the following features to `simp`:
- A routine for simplifying `have` telescopes in a way that avoids
quadratic complexity arising from locally nameless expression
representations, like what #6220 did for `letFun` telescopes.
Furthermore, simp converts `letFun`s into `have`s (nondependent lets),
and we remove the #6220 routine since we are moving away from `letFun`
encodings of nondependent lets.
- A `+letToHave` configuration option (enabled by default) that converts
lets into haves when possible, when `-zeta` is set. Previously Lean
would need to do a full typecheck of the bodies of `let`s, but the
`letToHave` procedure can skip checking some subexpressions, and it
modifies the `let`s in an entire expression at once rather than one at a
time.
- 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 the dependent lets is a
reasonable way to make progress. The `+zetaHave` option is also added to
the meta configuration.
- When `simp` is zeta reducing, it now uses an algorithm that avoids
complexity quadratic in the depth of the let telescope.
- Additionally, the zeta reduction routines in `simp`, `whnf`, and
`isDefEq` now all are consistent with how they apply the `zeta`,
`zetaHave`, and `zetaUnused` configurations.

The `letToFun` option is addressing a TODO in `getSimpLetCase` ("handle
a block of nested let decls in a single pass if this becomes a
performance problem").

Performance should be compared to before #8804, which temporarily
disabled the #6220 optimizations for `letFun` telescopes.

Good kernel performance depends on carefully handling the `have`
encoding. Due to the way the kernel instantiates bvars (it does *not*
beta reduce when instantiating), we cannot use congruence theorems of
the form `(have x := v; f x) = (have x ;= v'; f' x)`, since the bodies
of the `have`s will not be syntactically equal, which triggers zeta
reduction in the kernel in `is_def_eq`. Instead, we work with `f v = f'
v'`, where `f` and `f'` are lambda expressions. There is still zeta
reduction, but only when converting between these two forms at the
outset of the generated proof.

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.
@@ -253,6 +252,7 @@ structure Config where
   /--
   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`.
+  This option takes precedence over `zeta` and `zetaHave`.
   -/
   zetaUnused : Bool := true
   /--
@@ -261,14 +261,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/Init/SimpLemmas.lean

@@ -74,6 +74,22 @@ theorem let_body_congr {α : Sort u} {β : α → Sort v} {b b' : (a : α) → 
     (a : α) (h : ∀ x, b x = b' x) : (let x := a; b x) = (let x := a; b' x) :=
   (funext h : b = b') ▸ rfl
 
+/-!
+Congruence lemmas for `have` have kernel performance issues when stated using `have` directly.
+Illustration of the problem: the kernel infers that the type of
+`have_congr (fun x => b) (fun x => b') h₁ h₂`
+is
+`(have x := a; (fun x => b) x) = (have x := a'; (fun x => b') x)`
+rather than
+`(have x := a; b x) = (have x := a'; b' x)`
+That means the kernel will do `whnf_core` at every step of checking a sequence of these lemmas.
+Thus, we get quadratically many zeta reductions.
+
+For reference, we have the `have` versions of the theorems in the following comment,
+and then after that we have the versions that `simpHaveTelescope` actually uses,
+which avoid this issue.
+-/
+/-
 theorem have_unused {α : Sort u} {β : Sort v} (a : α) {b b' : β}
     (h : b = b') : (have _ := a; b) = b' := h
 
@@ -95,6 +111,29 @@ theorem have_body_congr_dep {α : Sort u} {β : α → Sort v} (a : α) {f f' :
 theorem have_body_congr {α : Sort u} {β : Sort v} (a : α) {f f' : α → β}
     (h : ∀ x, f x = f' x) : (have x := a; f x) = (have x := a; f' x) :=
   h a
+-/
+
+theorem have_unused' {α : Sort u} {β : Sort v} (a : α) {b b' : β}
+    (h : b = b') : (fun _ => b) a = b' := h
+
+theorem have_unused_dep' {α : Sort u} {β : Sort v} (a : α) {b : α → β} {b' : β}
+    (h : ∀ x, b x = b') : b a = b' := h a
+
+theorem have_congr' {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β}
+    (h₁ : a = a') (h₂ : ∀ x, f x = f' x) : f a = f' a' :=
+  @congr α β f f' a a' (funext h₂) h₁
+
+theorem have_val_congr' {α : Sort u} {β : Sort v} {a a' : α} {f : α → β}
+    (h : a = a') : f a = f a' :=
+  @congrArg α β a a' f h
+
+theorem have_body_congr_dep' {α : Sort u} {β : α → Sort v} (a : α) {f f' : (x : α) → β x}
+    (h : ∀ x, f x = f' x) : f a = f' a :=
+  h a
+
+theorem have_body_congr' {α : Sort u} {β : Sort v} (a : α) {f f' : α → β}
+    (h : ∀ x, f x = f' x) : f a = f' a :=
+  h a
 
 theorem letFun_unused {α : Sort u} {β : Sort v} (a : α) {b b' : β} (h : b = b') : @letFun α (fun _ => β) a (fun _ => b) = b' :=
   h

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/Basic.lean

@@ -158,8 +158,8 @@ structure Config where
   /-- Control projection reduction at `whnfCore`. -/
   proj : ProjReductionKind := .yesWithDelta
   /--
-  Zeta reduction: `let x := v; e[x]` reduces to `e[v]`.
-  We say a let-declaration `let x := v; e` is non dependent if it is equivalent to `(fun x => e) v`.
+  Zeta reduction: `let x := v; e[x]` and `have x := v; e[x]` reduce to `e[v]`.
+  We say a let-declaration `let x := v; e` is nondependent if it is equivalent to `(fun x => e) v`.
   Recall that
   ```
   fun x : BitVec 5 => let n := 5; fun y : BitVec n => x = y
@@ -169,6 +169,7 @@ structure Config where
   fun x : BitVec 5 => (fun n => fun y : BitVec n => x = y) 5
   ```
   is not.
+  See also `zetaHave`, for disabling the reduction nondependent lets (`have` expressions).
   -/
   zeta : Bool := true
   /--
@@ -178,8 +179,13 @@ structure Config where
   /--
   Zeta reduction for unused let-declarations: `let x := v; e` reduces to `e` when `x` does not occur
   in `e`.
+  This option takes precedence over `zeta` and `zetaHave`.
   -/
   zetaUnused : Bool := true
+  /--
+  When `zeta := true`, then `zetaHave := false` disables zeta reduction of `have` expressions.
+  -/
+  zetaHave : Bool := true
   deriving Inhabited, Repr
 
 /-- Convert `isDefEq` and `WHNF` relevant parts into a key for caching results -/
@@ -200,7 +206,8 @@ private def Config.toKey (c : Config) : UInt64 :=
   (c.zetaDelta.toUInt64 <<< 14) |||
   (c.univApprox.toUInt64 <<< 15) |||
   (c.etaStruct.toUInt64 <<< 16) |||
-  (c.proj.toUInt64 <<< 18)
+  (c.proj.toUInt64 <<< 18) |||
+  (c.zetaHave.toUInt64 <<< 20)
 
 /-- Configuration with key produced by `Config.toKey`. -/
 structure ConfigWithKey where

src/Lean/Meta/ExprDefEq.lean

@@ -1641,20 +1641,14 @@ private def isDefEqMVarSelf (mvar : Expr) (args₁ args₂ : Array Expr) : MetaM
       pure false
 
 /--
-Removes unnecessary let-decls (both true `let`s and `let_fun`s).
+Consumes unused lets/haves, depending on the current configuration.
+- When `zetaUnused`, all unused lets may be consumed.
+- Otherwise, when `zeta` is true, then unused lets can be consumed, unless they are nondependent and `cfg.zetaHave` is false.
 -/
-private partial def consumeLet : Expr → Expr
-  | e@(.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b
-  | e =>
-    if let some (_, _, _, b) := e.letFun? then
-      if b.hasLooseBVars then e else consumeLet b
-    else
-      e
-
 private partial def consumeLetIfZeta (e : Expr) : MetaM Expr := do
   let cfg ← getConfig
   if cfg.zeta || cfg.zetaUnused then
-    return consumeLet e
+    return consumeUnusedLet e (consumeNondep := cfg.zetaUnused || cfg.zetaHave)
   else
     return e
 

src/Lean/Meta/InferType.lean

@@ -189,10 +189,10 @@ because it overrides unrelated configurations.
 @[inline] def withInferTypeConfig (x : MetaM α) : MetaM α :=
   withAtLeastTransparency .default do
     let cfg ← getConfig
-    if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj == .yesWithDelta then
+    if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaHave && cfg.zetaDelta && cfg.proj == .yesWithDelta then
       x
     else
-      withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaDelta := true, proj := .yesWithDelta }) x
+      withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaHave := true, zetaDelta := true, proj := .yesWithDelta }) x
 
 @[export lean_infer_type]
 def inferTypeImp (e : Expr) : MetaM Expr :=