feat: rw? can discharge side conditions using local hypotheses (#7770)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib/Tactic/Rewrites.lean

@@ -12,6 +12,7 @@ import Mathlib.Tactic.Cache
 import Mathlib.Lean.Meta
 import Mathlib.Tactic.TryThis
 import Mathlib.Control.Basic
+import Mathlib.Tactic.SolveByElim
 
 /-!
 # The `rewrites` tactic.
@@ -30,6 +31,20 @@ We could try discharging side goals via `assumption` or `solve_by_elim`.
 
 set_option autoImplicit true
 
+namespace Lean.Meta
+
+/-- Extract the lemma, with arguments, that was used to produce a `RewriteResult`. -/
+-- This assumes that `r.eqProof` was constructed as:
+-- `mkAppN (mkConst ``Eq.ndrec [u1, u2]) #[α, a, motive, h₁, b, h₂]`
+-- and we want `h₂`.
+def RewriteResult.by? (r : RewriteResult) : Option Expr :=
+  if r.eqProof.isAppOfArity ``Eq.ndrec 6 then
+    r.eqProof.getArg! 5
+  else
+    none
+
+end Lean.Meta
+
 namespace Mathlib.Tactic.Rewrites
 
 open Lean Meta Std.Tactic.TryThis
@@ -157,6 +172,15 @@ def RewriteResult.computeRfl (r : RewriteResult) : MetaM RewriteResult := do
   catch _ =>
     pure { r with rfl? := some false }
 
+/-- Shortcut for calling `solveByElim`. -/
+def solveByElim (goals : List MVarId) (depth : Nat := 6) : MetaM PUnit := do
+  -- There is only a marginal decrease in performance for using the `symm` option for `solveByElim`.
+  -- (measured via `lake build && time lake env lean test/librarySearch.lean`).
+  let cfg : SolveByElim.Config :=
+    { maxDepth := depth, exfalso := false, symm := true }
+  let [] ← SolveByElim.solveByElim.processSyntax cfg false false [] [] #[] goals
+    | failure
+
 /--
 Find lemmas which can rewrite the goal.
 
@@ -206,12 +230,19 @@ def rewritesCore (hyps : Array (Expr × Bool × Nat))
     trace[Tactic.rewrites] m!"considering {if symm then "←" else ""}{expr}"
     let some result ← try? do goal.rewrite target expr symm
       | return none
-    return if result.mvarIds.isEmpty then
-      some ⟨expr, symm, weight, result, none, ← getMCtx⟩
+    if result.mvarIds.isEmpty then
+      return some ⟨expr, symm, weight, result, none, ← getMCtx⟩
     else
-      -- TODO Perhaps allow new goals? Try closing them with solveByElim?
-      -- A challenge is knowing what suggestions to print if we do so!
-      none
+      -- There are side conditions, which we try to discharge using local hypotheses.
+      let some _ ← try? do solveByElim result.mvarIds | return none
+      -- If we succeed, we need to reconstruct the expression to report that we rewrote by.
+      let some expr := result.by? | return none
+      let expr ← instantiateMVars expr
+      let (expr, symm) := if expr.isAppOfArity ``Eq.symm 4 then
+          (expr.getArg! 3, true)
+        else
+          (expr, false)
+      return some ⟨expr, symm, weight, result, none, ← getMCtx⟩
 
 /-- Find lemmas which can rewrite the goal. -/
 def rewrites (hyps : Array (Expr × Bool × Nat))

test/rewrites.lean

@@ -125,3 +125,22 @@ def zero : Nat := 0
 example : zero = 0 := by
   rw?
   exact test_sorry
+
+-- Discharge side conditions from local hypotheses.
+/--
+info: Try this: rw [h p]
+-- "no goals"
+-/
+#guard_msgs in
+example {P : Prop} (p : P) (h : P → 1 = 2) : 2 = 1 := by
+  rw?
+
+-- Rewrite in reverse, discharging side conditions from local hypotheses.
+/--
+info: Try this: rw [← h₁ p]
+-- Q a
+-/
+#guard_msgs in
+example {P : Prop} (p : P) (Q : α → Prop) (a b : α) (h₁ : P → a = b) (w : Q a) : Q b := by
+  rw?
+  exact w