linarith bug with metavariable

Stream: mathlib4

[Floris van Doorn]

If you write linarith [h] where h is a term that is not type-correct, but has a metavariable, then linarith will still use the conclusion of h to solve the goal, but then produces a proof with sorry.

import Mathlib.Data.Real.Basic

example (q : Prop) (p : ∀ (x : ℤ), q → 1 = 2) : 1 = 2 := by
  linarith [p _ garbage] -- no error, proof accepted with sorry
-- expected: unknown identifier `garbage`

[Eric Wieser]

Does this still happen with autoImplicit false?

[Thomas Murrills]

Hmm, maybe withoutErrToSorry belongs somewhere when elaborating the [] arguments?

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

open Lean Meta Elab Term Tactic

elab "without_err_to_sorry " tac:tactic : tactic => withoutErrToSorry <| evalTactic tac

example (q : Prop) (p : ∀ (x : ℤ), q → 1 = 2) : 1 = 2 := by
  without_err_to_sorry linarith [p _ garbage]
                                   --^^^^^^^ error: unknown identifier 'garbage'

[Thomas Murrills]

Eric Wieser said:

Does this still happen with autoImplicit false?

Just checked now—it still does

[Thomas Murrills]

Note that even if there's no metavariable, the error message is wrong: it says linarith failed to find a contradiction, not that garbage is garbage

[Kyle Miller]

#8561 seems to fix it, but it'd be good to wait for CI to see if it turns up any productive uses of metavariables

[Kyle Miller]

I also made it check for new metavariables, since these are likely not anything linarith should be solving for. Old metavariables might be ok, since the context might incidentally have some (but maybe linarith should use withNewMctxDepth to make sure it doesn't assign them, if it doesn't already)

[Kevin Buzzard]

#8561 is failing on KreinMilman

[Kevin Buzzard]

diff --git a/Mathlib/Analysis/Convex/KreinMilman.lean b/Mathlib/Analysis/Convex/KreinMilman.lean
index e8bb27ccdc..8c2d834d0e 100644
--- a/Mathlib/Analysis/Convex/KreinMilman.lean
+++ b/Mathlib/Analysis/Convex/KreinMilman.lean
@@ -102,6 +102,9 @@ theorem closure_convexHull_extremePoints (hscomp : IsCompact s) (hAconv : Convex
   have h : IsExposed ℝ s ({ y ∈ s | ∀ z ∈ s, l z ≤ l y }) := fun _ => ⟨l, rfl⟩
   obtain ⟨z, hzA, hz⟩ := hscomp.exists_forall_ge ⟨x, hxA⟩ l.continuous.continuousOn
   obtain ⟨y, hy⟩ := (h.isCompact hscomp).has_extreme_point ⟨z, hzA, hz⟩
-  linarith [hlr _ (subset_closure <| subset_convexHull _ _ <|
-    h.isExtreme.extremePoints_subset_extremePoints hy), hy.1.2 x hxA]
+  -- note : `linarith` struggles if `this` is used directly because there are
+  -- too many metavariables?
+  have := hlr _ (subset_closure <| subset_convexHull _ _ <|
+    h.isExtreme.extremePoints_subset_extremePoints hy)
+  linarith [this, hy.1.2 x hxA]
 #align closure_convex_hull_extreme_points closure_convexHull_extremePoints

That fixes it -- is that some kind of regression though?

[Kevin Buzzard]

I got bored waiting for count_heartbeats to terminate.

[Kyle Miller]

Thanks for investigating. I had set a flag that changes how _'s are elaborated, since it seemed to make a test work better, but I've switched that flag off.