debugging `compute_degree_le`

Stream: general

[Damiano Testa]

Dear All,

now that compute_degree_le is in mathlib, I have taken back looking at compute_degree. I have found a bug though that I am not able to remove. In the code below, if you add and then remove a zero, compute_degree_le works, but fails otherwise.

Does anyone have any idea of what might be going on?

import tactic.compute_degree

open polynomial
open_locale polynomial

variables {R : Type*} [ring R]

lemma repl {p q : R[X]} (hp : p.nat_degree ≤ 0) :
  (p * q).nat_degree = 0 :=
sorry

example : nat_degree (- 1 * 1 : R[X]) = 0 :=
begin
  apply repl _,
  rw [← zero_add 0, zero_add],  -- if you remove this line, then next one fails.
  compute_degree_le,
end

As far as I can see, without adding and removing the zero, Lean does not realize that -1 is a negative. But this is where I can make no further progress.

Any help is greatly appreciated!

Thanks!

[Damiano Testa]

In order to "fix" compute_degree_le, you can also use apply repl <no_underscore> or use refine repl _. This does not help me much in understanding how to make compute_degree_le oblivious to the issue, though.

[Floris van Doorn]

Without looking into it much, maybe compute_degree_le is not instantiating metavariables properly?

[Damiano Testa]

It is possible: where can I learn about what I should instantiate? I feel that I am running into this issue more and more as I get myself stuck deeper in meta-programs and never really understand how the instantiation works.

[Damiano Testa]

to give some context: I narrowed it down to here:

do `(nat_degree %%tl ≤ %%tr) ← target | fail!("Goal is not of the form `f.nat_degree ≤ d`"),
match tl with
| `(%%tl1 + %%tl2) := refine ``((nat_degree_add_le_iff_left _ _ _).mpr _)
| `(%%tl1 - %%tl2) := refine ``((nat_degree_sub_le_iff_left _ _ _).mpr _)
| `(%%tl1 * %%tl2) := do [d1, d2] ← [tl1, tl2].mmap guess_degree,
    refine ``(nat_degree_mul_le.trans $ (add_le_add _ _).trans (_ : %%d1 + %%d2 ≤ %%tr))
| `(- %%f)         := refine ``((nat_degree_neg _).le.trans _)
--  more similar lines

and Lean just ignores the last neg match.

[Damiano Testa]

Floris, your suggestion is spot on! What is below fixes this issue:

do `(nat_degree %%tl1 ≤ %%tr) ← target | fail!("Goal is not of the form `f.nat_degree ≤ d`"),
tl ← instantiate_mvars tl1,
-- continue as before

[Damiano Testa]

How can I know if I should instantiate mvars or not?

[Floris van Doorn]

If you have an unknown expression (like target), and you want to check whether it has a particular shape, you want to instantiate the metavariables first. You might also want to call whnf in case you need to do some beta-reductions (but without unfolding the ≤). Something like

do
  t ← target >>= instantiate_mvars,
  do `(nat_degree %%tl ≤ %%tr) ← whnf t reducible | fail!("Goal is not of the form `f.nat_degree ≤ d`"),

[Floris van Doorn]

In your example you can also double check that instantiating meta-variables is the problem, since this also succeeds:

example : nat_degree (- 1 * 1 : R[X]) = 0 :=
begin
  apply repl _,
  instantiate_mvars_in_target,
  compute_degree_le,
end

[Damiano Testa]

So, whenever I do a match, Lean will infer nothing more than the bare minimum, unless I explicitly tell it to. Is this a good first approximation?

[Floris van Doorn]

Yeah basically. Lean is very lazy with instantiating metavariables (which is crucial for performance reasons), so it is possible your goal is something like nat_degree ?m ≤ 0 and Lean already knows exactly what ?m is, but hasn't assigned ?m yet in your goal.

[Damiano Testa]

I see. Is it reasonable to file this as "like the difference between apply and refine, except at a more fundamental level"?

[Floris van Doorn]

I don't understand your analogy, so maybe not :-)

[Damiano Testa]

This refers to simply matching (giving something like apply) or doing the mvars and whnf stuff (something like refine).

[Damiano Testa]

I'm saying this because I often find that apply leaves goals that can be solved by apply_instance whereas using refine never seems to.

[Damiano Testa]

So, in my head, this is some unification that has not happened yet, but could have.

[Damiano Testa]

Anyway, this is more philosophical now: I will keep in mind that, whenever I match, I may want to give hints to Lean that it instantiate something.

Thanks a lot!

[Floris van Doorn]

I see what you mean. apply indeed fails to do some post-processing (which it probably really should do), like doing some apply_instance at the end and instantiating metavariables in the new goals.

[Damiano Testa]

Ok, I am happy that there is some analogy, even if vague. It helps to classify what is going on, by relating to something that I already know!

[Damiano Testa]

PR #15649 implements instantiate_mvars/whnf, as well as using focus1 to avoid spillage of the tactic to neighboring goals.