Zulip Chat Archive

Stream: general

Topic: nth_rewrite issue


Guillaume (Feb 25 2022 at 14:51):

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 (Feb 25 2022 at 15:34):

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 (Feb 25 2022 at 16:31):

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

Guillaume (Feb 25 2022 at 16:50):

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 (Feb 25 2022 at 16:50):

does it work to supply e.g. zero_lt_one?

Mario Carneiro (Feb 25 2022 at 16:51):

it sounds like the rewrite didn't actually work

Floris van Doorn (Feb 25 2022 at 17:25):

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 (Feb 25 2022 at 17:39):

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.


Last updated: Dec 20 2023 at 11:08 UTC