From 91d2f6d4fcbac3dae497d1c665cd66416cc38ca0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Oct 2021 19:54:10 -0700
Subject: [PATCH] feat: add `cleanup` tactic

---
 src/Lean/Meta/Basic.lean          |  6 +--
 src/Lean/Meta/Tactic.lean         |  1 +
 src/Lean/Meta/Tactic/Cleanup.lean | 66 +++++++++++++++++++++++++++++++
 3 files changed, 70 insertions(+), 3 deletions(-)
 create mode 100644 src/Lean/Meta/Tactic/Cleanup.lean

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 00c8bd2271..f520e60c67 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -1076,9 +1076,9 @@ def dependsOn (e : Expr) (fvarId : FVarId) : MetaM Bool :=
 def dependsOnPred (e : Expr) (p : FVarId → Bool) : MetaM Bool :=
   return (← getMCtx).findExprDependsOn e p
 
-/-- Return true iff the local declaration for `fvarId` depends on a free variable `x` s.t. `p x` -/
-def localDeclDependsOnPred (fvarId : FVarId) (p : FVarId → Bool) : MetaM Bool := do
-  return (← getMCtx).findLocalDeclDependsOn (← getLocalDecl fvarId) p
+/-- Return true iff the local declaration `localDecl` depends on a free variable `x` s.t. `p x` -/
+def localDeclDependsOnPred (localDecl : LocalDecl) (p : FVarId → Bool) : MetaM Bool := do
+  return (← getMCtx).findLocalDeclDependsOn localDecl p
 
 def ppExpr (e : Expr) : MetaM Format := do
   let ctxCore  ← readThe Core.Context
diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean
index 0dab0ad686..971b9e085f 100644
--- a/src/Lean/Meta/Tactic.lean
+++ b/src/Lean/Meta/Tactic.lean
@@ -22,3 +22,4 @@ import Lean.Meta.Tactic.Simp
 import Lean.Meta.Tactic.AuxLemma
 import Lean.Meta.Tactic.SplitIf
 import Lean.Meta.Tactic.Split
+import Lean.Meta.Tactic.Cleanup
diff --git a/src/Lean/Meta/Tactic/Cleanup.lean b/src/Lean/Meta/Tactic/Cleanup.lean
new file mode 100644
index 0000000000..a970fb57f3
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Cleanup.lean
@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.CollectFVars
+import Lean.Meta.Tactic.Clear
+
+namespace Lean.Meta
+
+/--
+  Auxiliary tactic for cleaning the local context. It removes local declarations (aka hypotheses) that are *not* relevant.
+  We say a variable `x` is "relevant" if
+  - It occurs in the target type, or
+  - There is a relevant variable `y` that depends on `x`, or
+  - The type of `x` is a proposition and it depends on a relevant variable `y`.
+-/
+partial def cleanup (mvarId : MVarId) : MetaM MVarId := do
+  withMVarContext mvarId do
+    checkNotAssigned mvarId `cleanup
+    let used ← collectUsed |>.run' (false, {})
+    let mut lctx ← getLCtx
+    for localDecl in lctx do
+      unless used.contains localDecl.fvarId do
+        lctx := lctx.erase localDecl.fvarId
+    let localInsts := (← getLocalInstances).filter fun inst => used.contains inst.fvar.fvarId!
+    let mvarNew ← mkFreshExprMVarAt lctx localInsts (← getMVarType' mvarId) MetavarKind.syntheticOpaque (← getMVarTag mvarId)
+    assignExprMVar mvarId mvarNew
+    return mvarNew.mvarId!
+where
+  addUsedFVars (e : Expr) : StateRefT (Bool × FVarIdSet) MetaM Unit := do
+    let (_, s) ← collectUsedFVars (← instantiateMVars e) |>.run {}
+    for fvarId in s.fvarSet do
+      addUsedFVar fvarId
+
+  addDeps (fvarId : FVarId) : StateRefT (Bool × FVarIdSet) MetaM Unit := do
+    let localDecl ← getLocalDecl fvarId
+    addUsedFVars localDecl.type
+    if let some val := localDecl.value? then
+      addUsedFVars val
+
+  addUsedFVar (fvarId : FVarId) : StateRefT (Bool × FVarIdSet) MetaM Unit := do
+    unless (← get).2.contains fvarId do
+      modify fun (modified, s) => (true, s.insert fvarId)
+      addDeps fvarId
+
+  /- We include `p` in the used-set, if `p` is a proposition that contains a `x` that is in the used-set. -/
+  collectPropsStep : StateRefT (Bool × FVarIdSet) MetaM Unit := do
+    let usedSet := (← get).2
+    for localDecl in (← getLCtx) do
+      if (← isProp localDecl.type) then
+        if (← dependsOnPred localDecl.type usedSet.contains) then
+          addUsedFVar localDecl.fvarId
+
+  collectProps : StateRefT (Bool × FVarIdSet) MetaM Unit := do
+    modify fun s => (false, s.2)
+    collectPropsStep
+    if (← get).1 then
+      collectProps
+
+  collectUsed : StateRefT (Bool × FVarIdSet) MetaM FVarIdSet := do
+    addUsedFVars (← getMVarType' mvarId)
+    collectProps
+    return (← get).2
+
+end Lean.Meta