feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804)

This PR implements first-class support for nondependent let expressions
in the elaborator; recall that a let expression `let x : t := v; b` is
called *nondependent* if `fun x : t => b` typechecks, and the notation
for a nondependent let expression is `have x := v; b`. Previously we
encoded `have` using the `letFun` function, but now we make use of the
`nondep` flag in the `Expr.letE` constructor for the encoding. This has
been given full support throughout the metaprogramming interface and the
elaborator. Key changes to the metaprogramming interface:
- Local context `ldecl`s with `nondep := true` are generally treated as
`cdecl`s. This is because in the body of a `have` expression the
variable is opaque. Functions like `LocalDecl.isLet` by default return
`false` for nondependent `ldecl`s. In the rare case where it is needed,
they take an additional optional `allowNondep : Bool` flag (defaults to
`false`) if the variable is being processed in a context where the value
is relevant.
- Functions such as `mkLetFVars` by default generalize nondependent let
variables and create lambda expressions for them. The
`generalizeNondepLet` flag (default true) can be set to false if `have`
expressions should be produced instead. **Breaking change:** Uses of
`letLambdaTelescope`/`mkLetFVars` need to use `generalizeNondepLet :=
false`. See the next item.
- There are now some mapping functions to make telescoping operations
more convenient. See `mapLetTelescope` and `mapLambdaLetTelescope`.
There is also `mapLetDecl` as a counterpart to `withLetDecl` for
creating `let`/`have` expressions.
- Important note about the `generalizeNondepLet` flag: it should only be
used for variables in a local context that the metaprogram "owns". Since
nondependent let variables are treated as constants in most cases, the
`value` field might refer to variables that do not exist, if for example
those variables were cleared or reverted. Using `mapLetDecl` is always
fine.
- The simplifier will cache its let dependence calculations in the
nondep field of let expressions.
- The `intro` tactic still produces *dependent* local variables. Given
that the simplifier will transform lets into haves, it would be
surprising if that would prevent `intro` from creating a local variable
whose value cannot be used.

Note that nondependence of lets is not checked by the kernel. To
external checker authors: If the elaborator gets the nondep flag wrong,
we consider this to be an elaborator error. Feel free to typecheck `letE
n t v b true` as if it were `app (lam n t b default) v` and please
report issues.

This PR follows up from #8751, which made sure the nondep flag was
preserved in the C++ interface.

Author: kmill

src/Lean/Elab/Binders.lean

@@ -785,54 +785,33 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
       pure (type, val, binders)
   let kind := kindOfBinderName id.getId
   trace[Elab.let.decl] "{id.getId} : {type} := {val}"
-  let elabBody : TermElabM Expr := do
-    let body ← elabTermEnsuringType body expectedType?
-    instantiateMVars body
   let result ←
-    if config.zeta then
-      let elabZetaCore (x : Expr) : TermElabM Expr := do
-        addLocalVarInfo id x
-        if let some h := config.eq? then
-          let hTy ← mkEq x val
-          withLocalDeclD h.getId hTy fun h' => do
-            addLocalVarInfo h h'
-            let body ← elabBody
-            pure <| (← body.abstractM #[x, h']).instantiateRev #[val, ← mkEqRefl val]
+    withLetDecl id.getId (kind := kind) type val (nondep := config.nondep) fun x => do
+      let elabBody : TermElabM Expr :=
+        elabTermEnsuringType body expectedType? >>= instantiateMVars
+      addLocalVarInfo id x
+      match config.eq? with
+      | none =>
+        let body ← elabBody
+        if config.zeta then
+          pure <| (← body.abstractM #[x]).instantiate1 val
         else
+          mkLetFVars #[x] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
+      | some h =>
+        let hTy ← mkEq x val
+        withLetDecl h.getId hTy (← mkEqRefl x) (nondep := true) fun h' => do
+          addLocalVarInfo h h'
           let body ← elabBody
-          pure <| (← body.abstractM #[x]).instantiate1 val
-      if !config.nondep then
-        withLetDecl id.getId (kind := kind) type val elabZetaCore
-      else
-        withLocalDecl id.getId (kind := kind) .default type elabZetaCore
-    else
-      if !config.nondep then
-        withLetDecl id.getId (kind := kind) type val fun x => do
-          addLocalVarInfo id x
-          if let some h := config.eq? then
-            let hTy ← mkEq x val
-            withLocalDeclD h.getId hTy fun h' => do
-              addLocalVarInfo h h'
-              let body ← elabBody
-              let body := (← body.abstractM #[h']).instantiate1 (← mkEqRefl x)
-              mkLetFVars #[x] body (usedLetOnly := config.usedOnly)
-          else
-            let body ← elabBody
-            mkLetFVars #[x] body (usedLetOnly := config.usedOnly)
-      else
-        withLocalDecl id.getId (kind := kind) .default type fun x => do
-          addLocalVarInfo id x
-          if let some h := config.eq? then
-            -- TODO(kmill): Think about how to encode this case.
-            let hTy ← mkEq x val
-            withLocalDeclD h.getId hTy fun h' => do
-              addLocalVarInfo h h'
-              let body ← elabBody
-              let f ← mkLambdaFVars #[x, h'] body
-              return mkApp2 f val (← mkEqRefl val)
+          if config.zeta then
+            pure <| (← body.abstractM #[x, h']).instantiateRev #[val, ← mkEqRefl val]
+          else if config.nondep then
+            -- TODO(kmill): Think more about how to encode this case.
+            -- Currently we produce `(fun (x : α) (h : x = val) => b) val rfl`.
+            -- N.B. the nondep lets become lambdas here.
+            let f ← mkLambdaFVars #[x, h'] body
+            return mkApp2 f val (← mkEqRefl val)
           else
-            let body ← elabBody
-            mkLetFun x val body
+            mkLetFVars #[x, h'] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
   if config.postponeValue then
     forallBoundedTelescope type binders.size fun xs type => do
       -- the original `fvars` from above are gone, so add back info manually

src/Lean/Elab/Match.lean

@@ -670,7 +670,7 @@ where
     match p with
     | .forallE n d b bi  => withLocalDecl n bi (← go d) fun x => do mkForallFVars #[x] (← go (b.instantiate1 x))
     | .lam n d b bi      => withLocalDecl n bi (← go d) fun x => do mkLambdaFVars #[x] (← go (b.instantiate1 x))
-    | .letE n t v b ..  => withLetDecl n (← go t) (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x))
+    | .letE n t v b nondep => mapLetDecl n (← go t) (← go v) (nondep := nondep) fun x => go (b.instantiate1 x)
     | .app f a          => return mkApp (← go f) (← go a)
     | .proj _ _ b       => return p.updateProj! (← go b)
     | .mdata k b        =>

src/Lean/Elab/MutualDef.lean

@@ -869,10 +869,11 @@ private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT Closu
     | .cdecl _ _ userName type bi k =>
       let toProcess ← pushLocalDecl toProcess fvarId userName type bi k
       mkClosureForAux toProcess
-    | .ldecl _ _ userName type val _ k =>
+    | .ldecl _ _ userName type val nondep k =>
       let zetaDeltaFVarIds ← getZetaDeltaFVarIds
-      if !zetaDeltaFVarIds.contains fvarId then
-        /- Non-dependent let-decl. See comment at src/Lean/Meta/Closure.lean -/
+      -- Note: If `nondep` is true then `zetaDeltaFVarIds.contains fvarId` must be false.
+      if nondep || !zetaDeltaFVarIds.contains fvarId then
+        /- Nondependent let-decl. See comment at src/Lean/Meta/Closure.lean -/
         let toProcess ← pushLocalDecl toProcess fvarId userName type .default k
         mkClosureForAux toProcess
       else

src/Lean/Elab/PreDefinition/Main.lean

@@ -93,7 +93,7 @@ private partial def ensureNoUnassignedLevelMVarsAtPreDef (preDef : PreDefinition
           checkCache { val := e : ExprStructEq } fun _ => do
             match e with
             | .forallE n d b c | .lam n d b c => withExpr e do visit d; withLocalDecl n c d fun x => visit (b.instantiate1 x)
-            | .letE n t v b _ => withExpr e do visit t; visit v; withLetDecl n t v fun x => visit (b.instantiate1 x)
+            | .letE n t v b nondep => withExpr e do visit t; visit v; withLetDecl n t v (nondep := nondep) fun x => visit (b.instantiate1 x)
             | .mdata _ b     => withExpr e do visit b
             | .proj _ _ b    => withExpr e do visit b
             | .sort u        => visitLevel u (← read)

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -133,9 +133,9 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions :
     | Expr.forallE n d b c =>
       withLocalDecl n c (← loop below d) fun x => do
         mkForallFVars #[x] (← loop below (b.instantiate1 x))
-    | Expr.letE n type val body _ =>
-      withLetDecl n (← loop below type) (← loop below val) fun x => do
-        mkLetFVars #[x] (← loop below (body.instantiate1 x)) (usedLetOnly := false)
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n (← loop below type) (← loop below val) (nondep := nondep) (usedLetOnly := false) fun x => do
+        loop below (body.instantiate1 x)
     | Expr.mdata d b =>
       if let some stx := getRecAppSyntax? e then
         withRef stx <| loop below b

src/Lean/Elab/PreDefinition/Structural/IndPred.lean

@@ -50,9 +50,9 @@ private partial def replaceIndPredRecApps (recArgInfo : RecArgInfo) (funType : E
     | Expr.forallE n d b c =>
       withLocalDecl n c (← loop d) fun x => do
         mkForallFVars #[x] (← loop (b.instantiate1 x))
-    | Expr.letE n type val body _ =>
-      withLetDecl n (← loop type) (← loop val) fun x => do
-        mkLetFVars #[x] (← loop (body.instantiate1 x))
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n (← loop type) (← loop val) (nondep := nondep) fun x => do
+        loop (body.instantiate1 x)
     | Expr.mdata d b => do
       if let some stx := getRecAppSyntax? e then
         withRef stx <| loop b

src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean

@@ -32,8 +32,9 @@ where
     match e with
     | Expr.lam ..     => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
     | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
-    | Expr.letE n type val body _ =>
-      withLetDecl n type (← visit val) fun x => do mkLetFVars #[x] (← visit (body.instantiate1 x))
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n type (← visit val) (nondep := nondep) fun x => do
+        visit (body.instantiate1 x)
     | Expr.mdata d b     => return mkMData d (← visit b)
     | Expr.proj n i s    => return mkProj n i (← visit s)
     | Expr.app .. =>

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

@@ -84,9 +84,9 @@ where
     | Expr.forallE n d b c =>
       withLocalDecl n c (← loop F d) fun x => do
         mkForallFVars #[x] (← loop F (b.instantiate1 x))
-    | Expr.letE n type val body _ =>
-      withLetDecl n (← loop F type) (← loop F val) fun x => do
-        mkLetFVars #[x] (← loop F (body.instantiate1 x)) (usedLetOnly := false)
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n (← loop F type) (← loop F val) (nondep := nondep) (usedLetOnly := false) fun x => do
+        loop F (body.instantiate1 x)
     | Expr.mdata d b =>
       if let some stx := getRecAppSyntax? e then
         withRef stx <| loop F b

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

@@ -241,10 +241,10 @@ where
       loop param d
       withLocalDecl n c d fun x => do
         loop param (b.instantiate1 x)
-    | Expr.letE n type val body _ =>
+    | Expr.letE n type val body nondep =>
       loop param type
       loop param val
-      withLetDecl n type val fun x => do
+      withLetDecl n type val (nondep := nondep) fun x => do
         loop param (body.instantiate1 x)
     | Expr.mdata _d b =>
       if let some stx := getRecAppSyntax? e then

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

@@ -110,14 +110,68 @@ builtin_dsimproc paramMatcher (_) := fun e => do
   let matcherApp' := { matcherApp with discrs := discrs', alts := alts' }
   return .continue <| matcherApp'.toExpr
 
-/-- `let x := (wfParam e); body[x] ==> let x := e; body[wfParam y] -/
+private def anyLetValueIsWfParam (e : Expr) : Bool :=
+  match e with
+  | .letE _ _ v b _ => (isWfParam? v).isSome || anyLetValueIsWfParam b
+  | _               => false
+
+private def numLetsWithValueNotIsWfParam (e : Expr) (acc := 0) : Nat :=
+  match e with
+  | .letE _ _ v b _ => if (isWfParam? v).isSome then acc else numLetsWithValueNotIsWfParam b (acc + 1)
+  | _               => acc
+
+private partial def processParamLet (e : Expr) : MetaM Expr := do
+  if let .letE _ t v b _ := e then
+    if let some v' := isWfParam? v then
+      if ← Meta.isProp t then
+        processParamLet <| e.updateLetE! t v' b
+      else
+        let u ← getLevel t
+        let b' := b.instantiate1 <| mkApp2 (.const ``wfParam [u]) t (.bvar 0)
+        processParamLet <| e.updateLetE! t v' b'
+    else
+      let num := numLetsWithValueNotIsWfParam e
+      assert! num > 0
+      letBoundedTelescope e num fun xs b => do
+        let b' ← processParamLet b
+        mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) xs b'
+  else
+    return e
+
+/--
+`let x : T := (wfParam e); body[x] ==> let x : T := e; body[wfParam y]` if `T` is not a proposition,
+otherwise `... ==> let x : T := e; body[x]`. (Applies to `have`s too.)
+
+Note: simprocs are provided the head of a let telescope, but not intermediate lets.
+-/
 builtin_dsimproc paramLet (_) := fun e => do
-  unless e.isLet do return .continue
-  let some v := isWfParam? e.letValue! | return .continue
-  let u ← getLevel e.letType!
-  let body' := e.letBody!.instantiate1 <|
-    mkApp2 (.const ``wfParam [u]) e.letType! (.bvar 0)
-  return .continue <| e.updateLetE! e.letType! v body'
+  unless e.isLet || anyLetValueIsWfParam e do return .continue
+  return .continue (← processParamLet e)
+
+/--
+Transforms non-Prop `have`s to `let`s, so that the values can be used in GuessLex and decreasing-by proofs.
+These `have`s may have been introdued by `simp`, which converts `let`s to `have`s.
+-/
+private def nonPropHaveToLet (e : Expr) : MetaM Expr := do
+  Meta.transform e (pre := fun e => do
+    if (← Meta.isProof e) then
+      return .done e
+    else if e.isLet then
+      -- Recall that `Meta.transform` processes entire let telescopes,
+      -- so we need to handle the telescope all at once.
+      let lctx ← getLCtx
+      let e' ← letTelescope e fun xs b => do
+        let lctx' ← xs.foldlM (init := lctx) fun lctx' x => do
+          let decl ← x.fvarId!.getDecl
+          -- Clear the flag if it's not a prop.
+          let decl' := decl.setNondep <| ← pure decl.isNondep <&&> Meta.isProp decl.type
+          pure <| lctx'.addDecl decl'
+        withLCtx' lctx' do
+          mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) xs b
+      return .continue e'
+    else
+      return .continue
+  )
 
 def preprocess (e : Expr) : MetaM Simp.Result := do
   unless wf.preprocess.get (← getOptions) do
@@ -141,9 +195,13 @@ def preprocess (e : Expr) : MetaM Simp.Result := do
           if h : as.size ≥ 2 then
             return .continue (mkAppN as[1] as[2:])
         return .continue
+
+    -- Transform `have`s to `let`s for non-propositions.
+    let e'' ← nonPropHaveToLet e''
+
     let result := { result with expr := e'' }
 
-    trace[Elab.definition.wf] "Attach-introduction:{indentExpr e'}\nto{indentExpr result.expr}\ncleaned up as{indentExpr e''}"
+    trace[Elab.definition.wf] "Attach-introduction:{indentExpr e'}\nto{indentExpr result.expr}"
     result.addLambdas xs
 
 end Lean.Elab.WF