feat: fix bug in MVarId.independent? and handling of symm in solve_by…

…_elim (#6862) Fixes the `exact?` bug reported at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/exact.3F.20recent.20regression.3F/near/387691588. Diagnosing this problem also revealed leanprover/lean4#2483, which we work around here (thanks @kmill) rather than wait for. Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Aug 30, 2023 · 20d0162 · 20d0162
1 parent 2d4a7e0
commit 20d0162
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 12 deletions.
diff --git a/Mathlib/Lean/Meta.lean b/Mathlib/Lean/Meta.lean
@@ -103,7 +103,7 @@ 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 solvability of the other goals.
 
-This function only calculates an approximation of this condition
+This function only calculates a conservative approximation of this condition.
 -/
 def independent? (L : List MVarId) (g : MVarId) : MetaM Bool := do
   let t ← instantiateMVars (← g.getType)
@@ -120,8 +120,8 @@ def independent? (L : List MVarId) (g : MVarId) : MetaM Bool := do
     return true
   -- Finally, we check if the goal `g` appears in the type of any of the goals `L`.
   L.allM fun g' => do
-    let t' ← instantiateMVars (← g'.getType)
-    pure <| !(← exprDependsOn' t' (.mvar g))
+    let mvars ← Meta.getMVars (← g'.getType)
+    pure <| !(mvars.contains g)
 
 end Lean.MVarId
 

diff --git a/Mathlib/Tactic/SolveByElim.lean b/Mathlib/Tactic/SolveByElim.lean
@@ -188,12 +188,18 @@ def elabContextLemmas (g : MVarId) (lemmas : List (TermElabM Expr)) (ctx : TermE
 /-- Returns the list of tactics corresponding to applying the available lemmas to the goal. -/
 def applyLemmas (cfg : Config) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr))
     (g : MVarId) : MetaM (List (MetaM (List MVarId))) := do
+-- We handle `cfg.symm` by saturating hypotheses of all goals using `symm`.
+-- This has better performance that the mathlib3 approach.
+let g ← if cfg.symm then g.symmSaturate else pure g
 let es ← elabContextLemmas g lemmas ctx
 applyTactics cfg.toApplyConfig cfg.transparency es g
 
 /-- Applies the first possible lemma to the goal. -/
 def applyFirstLemma (cfg : Config) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr))
     (g : MVarId) : MetaM (List MVarId) := do
+-- We handle `cfg.symm` by saturating hypotheses of all goals using `symm`.
+-- This has better performance that the mathlib3 approach.
+let g ← if cfg.symm then g.symmSaturate else pure g
 let es ← elabContextLemmas g lemmas ctx
 applyFirst cfg.toApplyConfig cfg.transparency es g
 
@@ -215,15 +221,6 @@ Custom wrappers (e.g. `apply_assumption` and `apply_rules`) may modify this beha
 -/
 def solveByElim (cfg : Config) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr))
     (goals : List MVarId) : MetaM (List MVarId) := do
-  -- We handle `cfg.symm` by saturating hypotheses of all goals using `symm`.
-  -- Implementation note:
-  -- (We used to apply `symm` all throughout the `solve_by_elim` stage.)
-  -- I initially reproduced the mathlib3 approach, but it had bad performance so switched to this.
-  let goals ← if cfg.symm then
-    goals.mapM fun g => g.symmSaturate
-  else
-    pure goals
-
   try
     run goals
   catch e => do

diff --git a/test/LibrarySearch/basic.lean b/test/LibrarySearch/basic.lean
@@ -217,3 +217,7 @@ example {r : α → α → Prop} : Function.Surjective (Quot.mk r) := by exact?
 #guard_msgs in
 lemma prime_of_prime (n : ℕ) : Prime n ↔ Nat.Prime n := by
   exact?
+
+-- Example from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/exact.3F.20recent.20regression.3F/near/387691588
+lemma ex' (x : ℕ) (_h₁ : x = 0) (h : 2 * 2 ∣ x) : 2 ∣ x := by
+  exact? says exact dvd_of_mul_left_dvd h