left-over metavariables

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

in the code below, I think that the issue is that pX is supposed to have type polynomial.X : polynomial R, but Lean has no way of knowing which R I am talking about. Is there a was to get Lean to unify the Type and semiring metavariables to what they should be and not produce these side goals?

Thanks!

import data.polynomial.degree.lemmas

open tactic

namespace tactic.interactive

meta def extract_deg_one_term (e : expr) : tactic unit :=
do pX ← to_expr ``(polynomial.X),
do bo ← succeeds $ unify e pX,
if bo then trace "0" else trace "1"

example {R : Type*} [semiring R] (h : (polynomial.X ^ 2 : polynomial R) = 1) : true :=
by do nh ← get_local `h >>= infer_type,
  match nh with
  | `(%%tl = %%tr) := do extract_deg_one_term tl,
    trivial
  | _ := skip
  end
/-
## prints "1", so it went through the "else"

tactic failed, there are unsolved goals
state:
2 goals
R : Type ?,
_inst_1 : semiring R,
h : polynomial.X ^ 2 = 1
⊢ Type ?

R : Type ?,
_inst_1 : semiring R,
h : polynomial.X ^ 2 = 1
⊢ semiring ?m_1
-/

[Damiano Testa]

As a check, if I replace polynomial.X ^ 2 with polynomial.X, then the do-block prints 0 and Lean is happy that all goals have been solved.

[Damiano Testa]

Btw, if I add {S : Type*} [semiring S] and use them to close the meta-goals, Lean is happy. This makes me think that the new goals are completely artificial

[Johan Commelin]

@Damiano Testa Do you need something like instantiate_mvars?

[Damiano Testa]

I think that I might, but I was not able to understand how to use it...

[Kyle Miller]

The problem here is that to_expr by default creates new goals for each metavariable after it's done with elaboration. You can use docs#tactic.i_to_expr_no_subgoals instead

[Kyle Miller]

That's equivalent to doing to_expr ``(polynomial.X) tt ff

[Damiano Testa]

Wonderful, Kyle, thanks a lot! In the #mwe it works! I will try it in my context! :thank_you:

[Kyle Miller]

But you might also consider doing something like

meta def extract_deg_one_term (e : expr) : tactic unit :=
match e with
| `(polynomial.X) := trace "0"
| _ := trace "1"
end

[Damiano Testa]

Since the issue was earlier, why does it only create problems in one branch?

[Damiano Testa]

I'll try your second suggestion, but in my actual context I think that it may not work. However, I am very grateful for suggested improvements!

[Kyle Miller]

When the unification is successful, then all the metavariables that were created end up being solved for here (they're in e's polynomial.X), and solved metavariables are automatically removed from the goal list

[Damiano Testa]

Ah, of course! :face_palm:
This is the magic of Lean working in the background!

[Damiano Testa]

Your first suggestion of adding tt ff works perfectly in my use-case and cuts down running time by literally an order of magnitude!

I'll see if I can match more efficiently as well!