fix(tactic/linarith): use refine instead of apply to avoid apply bug (#…

…3199)

closes #3142




Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/tactic/linarith/frontend.lean

@@ -149,7 +149,7 @@ Otherwise returns `none`.
 meta def apply_contr_lemma : tactic (option (expr × expr)) :=
 do t ← target,
    match get_contr_lemma_name_and_type t with
-   | some (nm, tp) := do applyc nm, v ← intro1, return $ some (tp, v)
+   | some (nm, tp) := do refine ((expr.const nm []) pexpr.mk_placeholder), v ← intro1, return $ some (tp, v)
    | none := return none
    end
 

test/linarith.lean

@@ -332,3 +332,14 @@ by nlinarith
 variables {E : Type*} [add_group E]
 example (f : ℤ → E) (h : 0 = f 0) : 1 ≤ 2 := by nlinarith
 example (a : E) (h : a = a) : 1 ≤ 2  := by nlinarith
+
+-- test that the apply bug doesn't affect linarith preprocessing
+
+constant α : Type
+def leα : α → α → Prop := λ a b, ∀ c : α, true
+
+noncomputable instance : discrete_linear_ordered_field α :=
+by refine_struct { le := leα }; admit
+
+example (a : α) (ha : a < 2) : a ≤ a :=
+by linarith