fix(tactic/linarith): instantiate metavariables in linarith (#19233)

This probably isn't exhaustive, but catches the really trivial case.

This doesn't appear to need forward-porting.

src/tactic/linarith/datatypes.lean

@@ -369,13 +369,13 @@ Typically `R` and `R'` will be the same, except when `c = 0`, in which case `R'`
 If `c = 1`, `h'` is the same as `h` -- specifically, it does *not* change the type to `1*t R 0`.
 -/
 meta def mk_single_comp_zero_pf (c : ℕ) (h : expr) : tactic (ineq × expr) :=
-do tp ← infer_type h,
+do tp ← infer_type h >>= instantiate_mvars,
   some (iq, e) ← return $ parse_into_comp_and_expr tp,
   if c = 0 then
     do e' ← mk_app ``zero_mul [e], return (ineq.eq, e')
   else if c = 1 then return (iq, h)
   else
-    do tp ← (prod.snd <$> (infer_type h >>= get_rel_sides)) >>= infer_type,
+    do tp ← (prod.snd <$> (infer_type h >>= instantiate_mvars >>= get_rel_sides)) >>= infer_type,
        c ← tp.of_nat c,
        cpos ← to_expr ``(%%c > 0),
        (_, ex) ← solve_aux cpos `[norm_num, done],

src/tactic/linarith/frontend.lean

@@ -151,7 +151,7 @@ newly introduced local constant.
 Otherwise returns `none`.
 -/
 meta def apply_contr_lemma : tactic (option (expr × expr)) :=
-do t ← target,
+do t ← target >>= instantiate_mvars,
    match get_contr_lemma_name_and_type t with
    | some (nm, tp) :=
      do refine ((expr.const nm []) pexpr.mk_placeholder), v ← intro1, return $ some (tp, v)
@@ -207,7 +207,7 @@ to only those that are comparisons over the type `restr_type`.
 -/
 meta def filter_hyps_to_type (restr_type : expr) (hyps : list expr) : tactic (list expr) :=
 hyps.mfilter $ λ h, do
-  ht ← infer_type h,
+  ht ← infer_type h >>= instantiate_mvars,
   match get_contr_lemma_name_and_type ht with
   | some (_, htype) := succeeds $ unify htype restr_type
   | none := return ff
@@ -238,7 +238,7 @@ expressions.
 meta def tactic.linarith (reduce_semi : bool) (only_on : bool) (hyps : list pexpr)
   (cfg : linarith_config := {}) : tactic unit :=
 focus1 $
-do t ← target,
+do t ← target >>= instantiate_mvars,
 -- if the target is an equality, we run `linarith` twice, to prove ≤ and ≥.
 if t.is_eq.is_some then
   linarith_trace "target is an equality: splitting" >>

src/tactic/linarith/parsing.lean

@@ -182,8 +182,8 @@ It also returns the largest variable index that appears in comparisons in `c`.
 -/
 meta def linear_forms_and_max_var (red : transparency) (pfs : list expr) :
   tactic (list comp × ℕ) :=
-do pftps ← pfs.mmap infer_type,
-   (l, _, map) ← to_comp_fold red [] pftps mk_rb_map,
+do pftps ← pfs.mmap (λ e, infer_type e >>= instantiate_mvars),
+   (l, _, map) ← to_comp_fold red []  pftps mk_rb_map,
    return (l, map.size - 1)
 
 

src/tactic/linarith/preprocessing.lean

@@ -70,7 +70,7 @@ private meta def rearr_comp_aux : expr → expr → tactic expr
 and turns it into a proof of a comparison `_ R 0`, where `R ∈ {=, ≤, <}`.
  -/
 meta def rearr_comp (e : expr) : tactic expr :=
-infer_type e >>= rearr_comp_aux e
+infer_type e >>= instantiate_mvars >>= rearr_comp_aux e
 
 /-- If `e` is of the form `((n : ℕ) : ℤ)`, `is_nat_int_coe e` returns `n : ℕ`. -/
 meta def is_nat_int_coe : expr → option expr
@@ -96,7 +96,7 @@ If `pf` is a proof of a strict inequality `(a : ℤ) < b`,
 and similarly if `pf` proves a negated weak inequality.
 -/
 meta def mk_non_strict_int_pf_of_strict_int_pf (pf : expr) : tactic expr :=
-do tp ← infer_type pf,
+do tp ← infer_type pf >>= instantiate_mvars,
 match tp with
 | `(%%a < %%b) := to_expr ``(int.add_one_le_iff.mpr %%pf)
 | `(%%a > %%b) := to_expr ``(int.add_one_le_iff.mpr %%pf)
@@ -139,7 +139,7 @@ Removes any expressions that are not proofs of inequalities, equalities, or nega
 meta def filter_comparisons : preprocessor :=
 { name := "filter terms that are not proofs of comparisons",
   transform := λ h,
-(do tp ← infer_type h,
+(do tp ← infer_type h >>= instantiate_mvars,
    is_prop tp >>= guardb,
    guardb (filter_comparisons_aux tp),
    return [h])
@@ -152,7 +152,7 @@ For example, a proof of `¬ a < b` will become a proof of `a ≥ b`.
 meta def remove_negations : preprocessor :=
 { name := "replace negations of comparisons",
   transform := λ h,
-do tp ← infer_type h,
+do tp ← infer_type h >>= instantiate_mvars,
 match tp with
 | `(¬ %%p) := singleton <$> rem_neg h p
 | _ := return [h]
@@ -171,9 +171,9 @@ meta def nat_to_int : global_preprocessor :=
 -- we lock the tactic state here because a `simplify` call inside of
 -- `zify_proof` corrupts the tactic state when run under `io.run_tactic`.
 do l ← lock_tactic_state $ l.mmap $ λ h,
-         infer_type h >>= guardb ∘ is_nat_prop >> zify_proof [] h <|> return h,
+      infer_type h >>= instantiate_mvars >>= guardb ∘ is_nat_prop >> zify_proof [] h <|> return h,
    nonnegs ← l.mfoldl (λ (es : expr_set) h, do
-     (a, b) ← infer_type h >>= get_rel_sides,
+     (a, b) ← infer_type h >>= instantiate_mvars >>= get_rel_sides,
      return $ (es.insert_list (get_nat_comps a)).insert_list (get_nat_comps b)) mk_rb_set,
    (++) l <$> nonnegs.to_list.mmap mk_coe_nat_nonneg_prf }
 
@@ -183,7 +183,7 @@ into a proof of `t1 ≤ t2 + 1`. -/
 meta def strengthen_strict_int : preprocessor :=
 { name := "strengthen strict inequalities over int",
   transform := λ h,
-do tp ← infer_type h,
+do tp ← infer_type h >>= instantiate_mvars,
    guardb (is_strict_int_prop tp) >> singleton <$> mk_non_strict_int_pf_of_strict_int_pf h
      <|> return [h] }
 
@@ -213,7 +213,7 @@ it tries to scale `t` to cancel out division by numerals.
 meta def cancel_denoms : preprocessor :=
 { name := "cancel denominators",
   transform := λ pf,
-(do some (_, lhs) ← parse_into_comp_and_expr <$> infer_type pf,
+(do some (_, lhs) ← parse_into_comp_and_expr <$> (infer_type pf >>= instantiate_mvars),
    guardb $ lhs.contains_constant (= `has_div.div),
    singleton <$> normalize_denominators_in_lhs pf lhs)
 <|> return [pf] }
@@ -272,7 +272,7 @@ This produces `2^n` branches when there are `n` such hypotheses in the input.
 -/
 meta def remove_ne_aux : list expr → tactic (list branch) :=
 λ hs,
-(do e ← hs.mfind (λ e : expr, do e ← infer_type e, guard $ e.is_ne.is_some),
+(do e ← hs.mfind (λ e : expr, do e ← infer_type e >>= instantiate_mvars, guard $ e.is_ne.is_some),
     [(_, ng1), (_, ng2)] ← to_expr ``(or.elim (lt_or_gt_of_ne %%e)) >>= apply,
     let do_goal : expr → tactic (list branch) := λ g,
       do set_goals [g],

src/tactic/linarith/verification.lean

@@ -86,11 +86,11 @@ meta def mk_lt_zero_pf : list (expr × ℕ) → tactic expr
 
 /-- If `prf` is a proof of `t R s`, `term_of_ineq_prf prf` returns `t`. -/
 meta def term_of_ineq_prf (prf : expr) : tactic expr :=
-prod.fst <$> (infer_type prf >>= get_rel_sides)
+prod.fst <$> (infer_type prf >>= instantiate_mvars >>= get_rel_sides)
 
 /-- If `prf` is a proof of `t R s`, `ineq_prf_tp prf` returns the type of `t`. -/
 meta def ineq_prf_tp (prf : expr) : tactic expr :=
-term_of_ineq_prf prf >>= infer_type
+term_of_ineq_prf prf >>= infer_type >>= instantiate_mvars
 
 /--
 `mk_neg_one_lt_zero_pf tp` returns a proof of `-1 < 0`,
@@ -120,7 +120,7 @@ proof, it adds a proof of `-t = 0` to the list.
 meta def add_neg_eq_pfs : list expr → tactic (list expr)
 | [] := return []
 | (h::t) :=
-  do some (iq, tp) ← parse_into_comp_and_expr <$> infer_type h,
+  do some (iq, tp) ← parse_into_comp_and_expr <$> (infer_type h >>= instantiate_mvars),
   match iq with
   | ineq.eq := do nep ← mk_neg_eq_zero_pf h, tl ← add_neg_eq_pfs t, return $ h::nep::tl
   | _ := list.cons h <$> add_neg_eq_pfs t

test/linarith.lean

@@ -1,5 +1,14 @@
 import tactic.linarith
 
+example : ∀ (y : ℕ), y ≤ 37 → y < 40 :=
+begin
+  refine λ y hy, _,
+  -- The type of `hy` is a (solved but not instantiated) metavariable
+  do { tactic.get_local `hy >>= tactic.infer_type >>= guardb ∘ expr.is_mvar },
+  -- But linarith should still work
+  linarith
+end
+
 example {α : Type} (_inst : Π (a : Prop), decidable a)
   [linear_ordered_field α]
   {a b c : α}