From da8e5150c970d4498d1939024e380c8079a3dc71 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 18 Mar 2021 14:25:50 -0700
Subject: [PATCH] feat: add `getNondepPropHyps`

---
 src/Lean/LocalContext.lean     |  4 ++++
 src/Lean/Meta/Tactic/Util.lean | 31 +++++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+)

diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 152e1f8d59..c931345744 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -69,6 +69,10 @@ def value : LocalDecl → Expr
   | cdecl ..              => panic! "let declaration expected"
   | ldecl (value := v) .. => v
 
+def hasValue : LocalDecl → Bool
+  | cdecl .. => false
+  | ldecl .. => true
+
 def setValue : LocalDecl → Expr → LocalDecl
   | ldecl idx id n t _ nd, v => ldecl idx id n t v nd
   | d, _                     => d
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index 36afffa738..a4f40f2472 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Util.ForEachExpr
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 import Lean.Meta.LevelDefEq
@@ -57,4 +58,34 @@ def admit (mvarId : MVarId) (synthetic := true) : MetaM Unit :=
 def headBetaMVarType (mvarId : MVarId) : MetaM Unit := do
   setMVarType mvarId (← getMVarType mvarId).headBeta
 
+/-- Collect nondependent hypotheses. -/
+def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) :=
+  withMVarContext mvarId do
+    let mut candidates : NameHashSet := {}
+    for localDecl in (← getLCtx) do
+      candidates ← removeDeps localDecl.type candidates
+      match localDecl.value? with
+      | none => pure ()
+      | some value => candidates ← removeDeps value candidates
+      if (← isProp localDecl.type) && !localDecl.hasValue then
+        candidates := candidates.insert localDecl.fvarId
+    candidates ← removeDeps (← getMVarType mvarId) candidates
+    if candidates.isEmpty then
+      return #[]
+    else
+      let mut result := #[]
+      for localDecl in (← getLCtx) do
+        if candidates.contains localDecl.fvarId then
+          result := result.push localDecl.fvarId
+      return result
+where
+  removeDeps (e : Expr) (candidates : NameHashSet) : MetaM NameHashSet := do
+    let e ← instantiateMVars e
+    let visit : StateRefT NameHashSet MetaM NameHashSet := do
+      e.forEach fun
+        | Expr.fvar fvarId _ => modify fun s => s.erase fvarId
+        | _ => pure ()
+      get
+    visit |>.run' candidates
+
 end Lean.Meta