feat: use nondep flag in Expr.letE and LocalContext.ldecl

This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x := v; b` is called *nondependent* if `fun x => 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 fully supported throughout the metaprogramming interface and the elaborator.

Note that nondependence of lets is not checked by the kernel.

Follows up from leanprover#8751, which made sure the nondep flag was preserved in the C++ interface.

Author: kmill

src/Lean/Elab/Binders.lean

@@ -741,18 +741,12 @@ 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 result ← if useLetExpr then
-    withLetDecl id.getId (kind := kind) type val fun x => do
+  let result ←
+    withLetDecl id.getId (kind := kind) type val (nondep := !useLetExpr) fun x => do
       addLocalVarInfo id x
       let body ← elabTermEnsuringType body expectedType?
       let body ← instantiateMVars body
-      mkLetFVars #[x] body (usedLetOnly := usedLetOnly)
-  else
-    withLocalDecl id.getId (kind := kind) .default type fun x => do
-      addLocalVarInfo id x
-      let body ← elabTermEnsuringType body expectedType?
-      let body ← instantiateMVars body
-      mkLetFun x val body
+      mkLetFVars #[x] body (usedLetOnly := usedLetOnly) (generalizeNondepLet := false)
   if elabBodyFirst 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

@@ -824,10 +824,10 @@ 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 -/
+      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,11 @@ 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 =>
+      -- Turn `have`s into `let`s if they are not propositions.
+      let nondep ← pure nondep <&&> not <$> Meta.isProp type
+      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,12 @@ 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 =>
+      -- Convert `have`s to `let`s if they aren't propositions so that the values
+      -- of local declarations can be used within decreasing-by proofs.
+      let nondep ← pure nondep <&&> Meta.isProp type
+      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,12 @@ 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
+      -- Convert `have`s to `let`s if they aren't propositions so that the values of local declarations can be used.
+      let nondep ← pure nondep <&&> Meta.isProp type
+      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,16 @@ 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] -/
+/-- `let x := (wfParam e); body[x] ==> let x := e; body[wfParam y]`
+Also accepts non-Prop `have`s as well. -/
 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'
+  let .letE _ t v b _ := e | return .continue
+  let some v := isWfParam? v | return .continue
+  if ← Meta.isProp t then return .continue <| e.updateLetE! t v b
+  let u ← getLevel t
+  let body' := b.instantiate1 <|
+    mkApp2 (.const ``wfParam [u]) t (.bvar 0)
+  return .continue <| e.updateLetE! t v body'
 
 def preprocess (e : Expr) : MetaM Simp.Result := do
   unless wf.preprocess.get (← getOptions) do