feat: MVarId.isIndependentOf (#254)

Std/Lean/Meta/Basic.lean

@@ -274,6 +274,58 @@ where
           modify (·.insert pendingMVarId)
         go pendingMVarId
 
+/-- Check if a goal is of a subsingleton type. -/
+def isSubsingleton (g : MVarId) : MetaM Bool := do
+  try
+    discard <| synthInstance (← mkAppM ``Subsingleton #[← g.getType])
+    return true
+  catch _ =>
+    return false
+
+/--
+Check if a goal is "independent" of a list of other goals.
+We say a goal is independent of other goals if assigning a value to it
+can not change the assignability of the other goals.
+
+Examples:
+* `?m_1 : Type` is not independent of `?m_2 : ?m_1`,
+  because we could assign `true : Bool` to `?m_2`,
+  but if we first assign `Nat` to `?m_1` then that is no longer possible.
+* `?m_1 : Nat` is not independent of `?m_2 : Fin ?m_1`,
+  because we could assign `37 : Fin 42` to `?m_2`,
+  but if we first assign `2` to `?m_1` then that is no longer possible.
+* `?m_1 : ?m_2` is not independent of `?m_2 : Type`, because we could assign `Bool` to ?m_2`,
+  but if we first assign `0 : Nat` to `?m_1` then that is no longer possible.
+* Given `P : Prop` and `f : P → Type`, `?m_1 : P` is independent of `?m_2 : f ?m_1`
+  by proof irrelevance.
+* Similarly given `f : Fin 0 → Type`, `?m_1 : Fin 0` is independent of `?m_2 : f ?m_1`,
+  because `Fin 0` is a subsingleton.
+* Finally `?m_1 : Nat` is independent of `?m_2 : α`,
+  as long as `?m_1` does not appear in `Meta.getMVars α`
+  (note that `Meta.getMVars` follows delayed assignments).
+
+This function only calculates a conservative approximation of this condition.
+That is, it may return `false` when it should return `true`.
+(In particular it returns false whenever the type of `g` contains a metavariable,
+regardless of whether this is related to the metavariables in `L`.)
+-/
+def isIndependentOf (L : List MVarId) (g : MVarId) : MetaM Bool := do
+  let t ← instantiateMVars (← g.getType)
+  if t.hasExprMVar then
+    -- If the goal's type contains other meta-variables,
+    -- we conservatively say that `g` is not independent.
+    -- It would be possible to check if `L` depends on these meta-variables.
+    return false
+  if (← inferType t).isProp then
+    -- If the goal is propositional,
+    -- proof-irrelevance ensures it is independent of any other goals.
+    return true
+  if ← g.isSubsingleton then
+    -- If the goal is a subsingleton, it is independent of any other goals.
+    return true
+  -- Finally, we check if the goal `g` appears in the type of any of the goals `L`.
+  L.allM fun g' => do pure !((← getMVars (← g'.getType)).contains g)
+
 /--
 Replace hypothesis `hyp` in goal `g` with `proof : typeNew`.
 The new hypothesis is given the same user name as the original,