feat: add support for expanding let-declarations to simp

Given a local context containing `x : t := e`,
`simp (config := { zeta := false }) [x]` will expand `x` even
if `zeta := false`.

src/Lean/Elab/Tactic/Simp.lean

@@ -101,6 +101,17 @@ private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (id : Origin) (e
         return thms.addDeclToUnfoldCore declName
       else
         thms.addDeclToUnfold declName
+  else if e.isFVar then
+    let fvarId := e.fvarId!
+    let decl ← fvarId.getDecl
+    if (← isProp decl.type) then
+      thms.add id #[] e (post := post) (inv := inv)
+    else if !decl.isLet then
+      throwError "invalid argument, variable is not a proposition or let-declaration"
+    else if inv then
+      throwError "invalid '←' modifier, '{e}' is a let-declaration name to be unfolded"
+    else
+      return thms.addLetDeclToUnfold fvarId
   else
     thms.add id #[] e (post := post) (inv := inv)
 
@@ -237,6 +248,10 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
   else
     let ctx := r.ctx
     let mut simpTheorems := ctx.simpTheorems
+    /-
+    When using `zeta := false`, we do not expand let-declarations when using `[*]`.
+    Users must explicitly include it in the list.
+    -/
     let hs ← getPropHyps
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do

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

@@ -119,8 +119,8 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
         -- `structure` projections
         reduceProjCont? (← unfoldDefinition? e)
 
-private def reduceFVar (cfg : Config) (e : Expr) : MetaM Expr := do
-  if cfg.zeta then
+private def reduceFVar (cfg : Config) (thms : SimpTheoremsArray) (e : Expr) : MetaM Expr := do
+  if cfg.zeta || thms.isLetDeclToUnfold e.fvarId! then
     match (← getFVarLocalDecl e).value? with
     | some v => return v
     | none   => return e
@@ -254,8 +254,8 @@ private partial def dsimp (e : Expr) : M Expr := do
       if r.expr != e then
         return .visit r.expr
     let mut eNew ← reduce e
-    if cfg.zeta && eNew.isFVar then
-      eNew ← reduceFVar cfg eNew
+    if eNew.isFVar then
+      eNew ← reduceFVar cfg (← getSimpTheorems) eNew
     if eNew != e then return .visit eNew else return .done e
   transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
@@ -363,7 +363,7 @@ where
     | Expr.sort ..     => return { expr := e }
     | Expr.lit ..      => simpLit e
     | Expr.mvar ..     => return { expr := (← instantiateMVars e) }
-    | Expr.fvar ..     => return { expr := (← reduceFVar (← getConfig) e) }
+    | Expr.fvar ..     => return { expr := (← reduceFVar (← getConfig) (← getSimpTheorems) e) }
 
   simpLit (e : Expr) : M Result := do
     match e.natLit? with

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

@@ -157,6 +157,10 @@ structure SimpTheorems where
   pre          : SimpTheoremTree := DiscrTree.empty
   post         : SimpTheoremTree := DiscrTree.empty
   lemmaNames   : PHashSet Origin := {}
+  /--
+  Constants (and let-declaration `FVarId`) to unfold.
+  When `zeta := false`, the simplifier will expand a let-declaration if it is in this set.
+  -/
   toUnfold     : PHashSet Name := {}
   erased       : PHashSet Origin := {}
   toUnfoldThms : PHashMap Name (Array Name) := {}
@@ -177,10 +181,17 @@ where
 def SimpTheorems.addDeclToUnfoldCore (d : SimpTheorems) (declName : Name) : SimpTheorems :=
   { d with toUnfold := d.toUnfold.insert declName }
 
+def SimpTheorems.addLetDeclToUnfold (d : SimpTheorems) (fvarId : FVarId) : SimpTheorems :=
+  -- A small hack that relies on the fact that constants and `FVarId` names should be disjoint.
+  { d with toUnfold := d.toUnfold.insert fvarId.name }
+
 /-- Return `true` if `declName` is tagged to be unfolded using `unfoldDefinition?` (i.e., without using equational theorems). -/
 def SimpTheorems.isDeclToUnfold (d : SimpTheorems) (declName : Name) : Bool :=
   d.toUnfold.contains declName
 
+def SimpTheorems.isLetDeclToUnfold (d : SimpTheorems) (fvarId : FVarId) : Bool :=
+  d.toUnfold.contains fvarId.name -- See comment at `addLetDeclToUnfold`
+
 def SimpTheorems.isLemma (d : SimpTheorems) (thmId : Origin) : Bool :=
   d.lemmaNames.contains thmId
 
@@ -470,6 +481,9 @@ def SimpTheoremsArray.isErased (thmsArray : SimpTheoremsArray) (thmId : Origin)
 def SimpTheoremsArray.isDeclToUnfold (thmsArray : SimpTheoremsArray) (declName : Name) : Bool :=
   thmsArray.any fun thms => thms.isDeclToUnfold declName
 
+def SimpTheoremsArray.isLetDeclToUnfold (thmsArray : SimpTheoremsArray) (fvarId : FVarId) : Bool :=
+thmsArray.any fun thms => thms.isLetDeclToUnfold fvarId
+
 macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc:(docComment)?
   "register_simp_attr" id:ident : command => do
   let str := id.getId.toString