From ba95dbc36be02086d51fed358f5bf2373eaae0cb Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sun, 26 Jan 2025 12:14:12 +0100
Subject: [PATCH] feat: zetaUnused option (implementation) (#6755)

This PR implements the `zetaUnused` simp and reduction option (added in
#6754).

True by default, and implied by `zeta`, this can be turned off to make
simp even more careful about preserving the expression structure,
including unused let and have expressions.

Breaking change: The `split` tactic no longer removes unused let and
have expressions as a side-effect, in rare cases this may break proofs.
`dsimp only` can be used to remove unused have and let expressions.
---
 src/Lean/Meta/ExprDefEq.lean        | 13 +++--
 src/Lean/Meta/Tactic/Simp/Main.lean |  7 +--
 tests/lean/run/zetaUnused.lean      | 80 +++++++++++++++++++++++++++++
 3 files changed, 94 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/zetaUnused.lean

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 6314ee8f08..2a705e7827 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1634,11 +1634,18 @@ private partial def consumeLet : Expr → Expr
     else
       e
 
+private partial def consumeLetIfZeta (e : Expr) : MetaM Expr := do
+  let cfg ← getConfig
+  if cfg.zeta || cfg.zetaUnused then
+    return consumeLet e
+  else
+    return e
+
 mutual
 
-private partial def isDefEqQuick (t s : Expr) : MetaM LBool :=
-  let t := consumeLet t
-  let s := consumeLet s
+private partial def isDefEqQuick (t s : Expr) : MetaM LBool := do
+  let t ← consumeLetIfZeta t
+  let s ← consumeLetIfZeta s
   match t, s with
   | .lit  l₁,      .lit l₂     => return (l₁ == l₂).toLBool
   | .sort u,       .sort v     => toLBoolM <| isLevelDefEqAux u v
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index e1c63556ac..ada06f0576 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -465,7 +465,7 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit
   let post := m.dpost >> dsimpReduce
   withInDSimp do
-  transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
+  transform (usedLetOnly := cfg.zeta || cfg.zetaUnused) e (pre := pre) (post := post)
 
 def visitFn (e : Expr) : SimpM Result := do
   let f := e.getAppFn
@@ -623,6 +623,7 @@ It attempts to minimize the quadratic overhead imposed by
 the locally nameless discipline.
 -/
 partial def simpNonDepLetFun (e : Expr) : SimpM Result := do
+  let cfg ← getConfig
   let rec go (xs : Array Expr) (e : Expr) : SimpM SimpLetFunResult := do
     /-
     Helper function applied when `e` is not a `let_fun` or
@@ -648,9 +649,9 @@ partial def simpNonDepLetFun (e : Expr) : SimpM Result := do
     -/
     if alpha.hasLooseBVars || !betaFun.isLambda || !body.isLambda || betaFun.bindingBody!.hasLooseBVars then
       stop
-    else if !body.bindingBody!.hasLooseBVar 0 then
+    else if (cfg.zeta || cfg.zetaUnused) && !body.bindingBody!.hasLooseBVar 0 then
       /-
-      Redundant `let_fun`. The simplifier will remove it.
+      Redundant `let_fun`. The simplifier will remove it when `zetaUnused := true`.
       Remark: the `hasLooseBVar` check here may introduce a quadratic overhead in the worst case.
       If observe that in practice, we may use a separate step for removing unused variables.
 
diff --git a/tests/lean/run/zetaUnused.lean b/tests/lean/run/zetaUnused.lean
new file mode 100644
index 0000000000..f096fbe76b
--- /dev/null
+++ b/tests/lean/run/zetaUnused.lean
@@ -0,0 +1,80 @@
+
+/--
+info: b : Bool
+⊢ if b = true then
+    let_fun unused := ();
+    True
+  else False
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  trace_state; sorry
+
+/--
+info: b : Bool
+⊢ b = true
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  simp; trace_state; sorry
+
+/--
+info: b : Bool
+⊢ b = true ∧
+    let_fun unused := ();
+    True
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  simp (config := Lean.Meta.Simp.neutralConfig); trace_state; sorry
+
+/-- error: simp made no progress -/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  simp (config := Lean.Meta.Simp.neutralConfig) only; trace_state; sorry
+
+/--
+info: b : Bool
+⊢ if b = true then True else False
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  simp (config := Lean.Meta.Simp.neutralConfig) +zeta only; trace_state; sorry
+
+
+/--
+info: b : Bool
+⊢ if b = true then True else False
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  simp (config := Lean.Meta.Simp.neutralConfig) +zetaUnused only; trace_state; sorry
+
+
+-- Before the introduction of zetaUnused, split would do collateral damage to unused letFuns.
+-- Now they are preserved:
+
+/--
+info: case isTrue
+b : Bool
+h✝ : b = true
+⊢ let_fun unused := ();
+  True
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  split
+  · trace_state; sorry
+  · sorry