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

@@ -785,54 +785,34 @@ 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
+        let pf ← mkEqRefl x
+        withLetDecl h.getId hTy pf (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, pf]
+          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 pf
           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,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