nth_rewrite issue

Stream: general

[Guillaume]

Hi, I was wondering whether there is not a small issue with nth_rewrite. For instance, doing this will give me "goals accomplished" in vscode:

example :
  abs(-1:ℝ) = (-1:ℝ) :=
begin
  nth_rewrite 0 abs_of_pos _,
end

before telling me tactic failed, result contains meta-variables after the proof. Any ideas? Basically, nth_rewrite seems to never add to the goal stack the missing hypotheses

[Alex J. Best]

Looks like an issue similar to #3349. You can check it's not already reported on the GitHub issues page and if not please report it. In the meantime tactic#recover might help you rescue your proof for now. Just run it after the nth rewrite to see the side hypothesis goals generated

[Kevin Buzzard]

recover does indeed recover, although I think there's also a small issue with the mathematics as well ;-)

[Guillaume]

thanks! I tried recover, but the tactic state is not what I would expect: it provides 0 < ?m_3 while I would expect 0 < -1

[Mario Carneiro]

does it work to supply e.g. zero_lt_one?

[Mario Carneiro]

it sounds like the rewrite didn't actually work

[Floris van Doorn]

You reached a situation the current recover didn't invision: you have metavariables that do not occur in the result, but only in the types of other metavariables. Here is one way to get your desired goal 0 < -1:

import data.real.basic

open tactic

meta def metavariables_aux : ℕ → list expr → list expr → tactic (list expr)
| 0     donemvars todo         := return (donemvars ++ todo)
| (n+1) donemvars []           := return donemvars
| (n+1) donemvars (mvar::todo) := do
  tp ← infer_type mvar,
  let newmvars := expr.list_meta_vars tp,
  let newmvars := newmvars.filter (λ mvar, mvar ∉ todo ∧ mvar ∉ donemvars),
  metavariables_aux n (mvar::donemvars) (todo++newmvars)

meta def metavariables' : tactic (list expr) := do
  e ← result,
  metavariables_aux 10 [] e.list_meta_vars

meta def tactic.interactive.recover' : tactic unit :=
metavariables' >>= tactic.set_goals

example :
  abs(-1:ℝ) = (-1:ℝ) :=
begin
  nth_rewrite 0 abs_of_pos _,
  recover',
  exact ℝ,
  apply_instance,
  apply_instance,
  exact -1,
  apply_instance
  -- goal: ⊢ 0 < -1
end

I will PR this.

[Floris van Doorn]

This is not really satisfactory though... It will give metavariables that can have only one possible value, or otherwise result will be type-incorrect. Is there a way to say to Lean "solve this goal in the only way that will make result type-correct"? I tried variations of instantiate_mvars and type_check on result, but I don't see how to do this.