Strange behavior of compute_degree

Stream: mathlib4

[Michael Stoll]

While tinkering with Gelfand-Mazur, I came across the following.

import Mathlib.Tactic.ComputeDegree

variable {R : Type*} [CommRing R]

open Polynomial

variable (R) in
noncomputable
def p : R[X] := X ^ 2 + 2 • X + C 1

variable [Nontrivial R]

theorem xxx : (p R).natDegree = 2 := by
  compute_degree
  -- 2 goals: `¬(p R).coeff 2 ≠ 0` *and* `(p R).natDegree = 2`
  all_goals sorry

I would expect compute_degree to clear the original goal and only leave the side goals necessary for proving it. @Damiano Testa ?

[Michael Stoll]

There is another strange error when I replace p by its definition.

import Mathlib.Tactic.ComputeDegree

variable {R : Type*} [CommRing R]

open Polynomial

theorem yyy : (X ^ 2 + 2 • X + C 1 : R[X]).natDegree = 2 := by
/-  tactic 'apply' failed, could not unify the conclusion of
      'Mathlib.Tactic.ComputeDegree.natDegree_smul_le_of_le'
        (HSMul.hSMul.{?u.3352, ?u.3352, ?u.3352} ?a ?f).natDegree ≤ ?n
    with the goal
      (HSMul.hSMul.{0, u_1, u_1} 2 X).natDegree ≤ ?h_natDeg_le.hp.n
  -/
  compute_degree

This could be related to #lean4 > "@instHAdd ℕ instAddNat : HAdd ℕ ℕ ℕ" out of thin air @ 💬: some strange things seem to be going on when elaborating statements containing polynomials, but I am not sure how closely related it might be.

[Damiano Testa]

I'm not at a computer, but here is what I suspect.

First, compute_degree should not see through defs, so the first behaviour is "almost" what I would expect. I thought it would have left a p.natDegree ≤ 2 goal, though.

Second, I don't think thatcompute_degree is aware of •. It would be really easy to add this feature, but I don't think that I was thinking about that possibility when writing the tactic.

[Michael Stoll]

Damiano Testa said:

I thought it would have left a p.natDegree ≤ 2 goal, though.

Exactly.

[Michael Stoll]

Damiano Testa said:

Second, I don't think thatcompute_degree is aware of •. It would be really easy to add this feature, but I don't think that I was thinking about that possibility when writing the tactic.

I've been trying to manipulate polynomials a fair bit in the last few hours, and I got the impression that simp does not do a good job on them (meaning, so that after simp I can use ring to close equality goals, for example). Probably some thought should go into what a good simp normal form for polynomials may look like. For example, it currently uses map_pow etc., which changes C (a ^2) to (C a) ^ 2, and on this the lemma that says that the nth coefficient of C a is zero (if n is nonzero) doesn't fire.
I assume that you @Damiano Testa have thought about this while writing the tactics like compute_degree. Maybe one can extract a normalize_poly tactic from this?

[Damiano Testa]

I wrote the tactic in Lean3, then ported it to Lean4. The reason this is relevant is that coercions changed quite a bit and in Lean3, basically the only way to multiply constants and polynomials was via C. I think that very little thought has gone into simp-confluence for polynomials in Lean4 and your experiments are probably showing that such a cleanup is overdue.

[Damiano Testa]

Maybe an easy solution would be to have a custom simp set that converts polynomials to something where compute_degree has a chance of working, although going from2 * X to C 2 * X may be tricky with simp.

[Yaël Dillies]

I have a set of simprocs in the works

[Damiano Testa]

Ok, great! Then at least agreeing with an expected simp-normal form for polynomials would help making compute_degree more reliable.

[Michael Stoll]

It's not just compute_degree, one of my problems is that what simp produces is not good for ring. So hopefully Yaël's simprocs will produce a form that is ring-friendly.

[Michael Stoll]

(I need to cook dinner now...)

[Damiano Testa]

How reasonable/feasible would it be to try to ban completely C and only allowing * and •?

[Yaël Dillies]

Why not just make C a plain function?

[Damiano Testa]

(I mean as simp-normal form.)

[Damiano Testa]

A plain function as in refactoring polynomial?

[Damiano Testa]

I personally don't have it in me to embark in such a refactor.

[Damiano Testa]

Also, "fixing" compute_degree to allow • would not be especially hard: likely it is just a matter of adding a lemma about the degree of a smul (which may even already be there) and then making compute_degree use it.

[Michael Stoll]

One problem with • is that ring does not work well with it. To get my goals closed by ring, it seems best to write everything in terms of C.

And regarding compute_degree, the following works in my code:

have : (c ^ 2 • (X ^ 2 - s • (2 * X)) + C (c ^ 2) * C t).natDegree ≤ 2 := by compute_degree

[Yaël Dillies]

Michael Stoll said:

One problem with • is that ring does not work well with it.

Sounds like you want to hear about the module tactic :wink:

[Michael Stoll]

import Mathlib.Tactic

variable {R : Type*} [CommRing R]

open Polynomial

example : (X (R := R) + 1) ^ 2 = 2 • X + 1 + X ^ 2 := by
  --ring -- works
  /-
  ring failed, ring expressions not equal
  R : Type u_1
  inst✝ : CommRing R
  ⊢ 1 = 0
  -/
  module

[Yaël Dillies]

The idiom is ring_nf; module (but here ring_nf already closes the goal)

[Michael Stoll]

import Mathlib

open Polynomial

theorem foo {R : Type*} [CommRing R] (s t c : R) :
  (X ^ 2 - 2 * s • X + C t) ^ 1 - c ^ 1 • 2 • (X - C s) + C (c ^ (2 * 1)) =
    ((X - C c) ^ 2 - 2 * s • (X - C c) + C t) * 1 := by
  ring_nf
  module -- ring failed, ring expressions not equal
  sorry

This is one of my use cases.

[Damiano Testa]

#25944

[Damiano Testa]

It turns out that compute_degree already supported smul, but only by the coefficients of the polynomial ring. In your case, the smul was coming from a natural number, so technically not from the coefficients. The PR above fixes this issue.

[Damiano Testa]

The PR also contains this test

variable [CommRing R] [Nontrivial R] in
example : (X ^ 2 + 2 • X + C 1 : R[X]).natDegree = 2 := by
  compute_degree!
  guard_target = ((1 + 2 * X.coeff 2 : R) ≠ 0)
  simp [coeff_X]

where ideally compute_degree! should close the goal, not leave a side-goal. However, I have not worked out why X.coeff 2 does not get replaced by 0.

[Michael Stoll]

It seems that docs#Polynomial.coeff_X_of_ne_one and docs#Polynomial.coeff_X are not simp lemmas (and when I just give the first lemma to simp, then simpdoes not discharge the side goal 2 ≠ 1 by itself). I don't know if this is relevant to how compute_degree! works, though.

[Damiano Testa]

Yes, I think that this is indeed relevant: compute_degree! tries to discharge the left-over goals using norm_num <;> assumption. Thus, simp bringing a goal to 2 ≠ 1 should make norm_num close the goal.

[Damiano Testa]

I just checked: adding the simp attribute to coeff_X does indeed simplify the proof:

variable [CommRing R] [Nontrivial R] in
example : (X ^ 2 + 2 • X + C 1 : R[X]).natDegree = 2 := by
  compute_degree!  -- works

[Michael Stoll]

Damiano Testa said:

Thus, simp bringing a goal to 2 ≠ 1 should make norm_num close the goal.

As far as I understand, simp does not fire when it cannot discharge the side goals.

[Damiano Testa]

It seems that inside norm_num, that is ok.

[Damiano Testa]

By the way, this also works:

import Mathlib

open Polynomial

attribute [simp] coeff_X

variable [CommRing R] [Nontrivial R] in
example : (1 + 2 * X.coeff 2 : R) ≠ 0 := by
  simp

So, it seems that simp is already able to close the goal.

[Michael Stoll]

It uses ↓reduceIte and one_ne_zero, so I would assume it's due to simprocs.

[Michael Stoll]

@Damiano Testa Currently this fails:

import Mathlib

open Polynomial

/-
'compute_degree' inapplicable. The goal
  (C 1).natDegree < 1
is expected to be '≤' or '='.
-/
example : (C 1 : Polynomial ℤ).natDegree < 1 := by compute_degree

Would it be possible to extend compute_degree/compute_degree! to also deal with strict inequalities?

[Damiano Testa]

Fixed a bug, found a bug.

[Damiano Testa]

Given that

  apply lt_of_le_of_lt
  · compute_degree
  · norm_num

works, it is probably easy to get something working, at least leaving out of scope the inequality <actual_degree> < given bound, so 0 < 1 in your case.

[Damiano Testa]

I remember thinking about strict inequalities and deciding against doing them in the first place, since the algorithm for ≤ is somewhat easier.

[Damiano Testa]

#26145, where your example is solved by compute_degree!.

[Damiano Testa]

Note that the +37-16 change that github reports consists of

• 2 added lines of code;
• documentation and examples!

[Michael Stoll]

I noticed that (just had a look), but I don't feel competent enough with meta code to maintainer merge.

[Damiano Testa]

Sure, no worries! If it helps anyone, the strategy is to detect if the goal looks like f.natDegree < d and, if so, start the proof with apply lt_of_le_of_lt and then fall back on the earlier behaviour.

[Damiano Testa]

In fact, compute_degree does not "know" what the degree is at the start: it replaces the degree with a metavariable, imposes conditions on the metavariable by traversing the polynomial and then checks whether the constraints are compatible.

[Damiano Testa]

So, the first step of replacing the degree with a metavariable is what it would have done in the weak inequality as well.

[Damiano Testa]

Michael, strict inequalities are now handled by compute_degree also in the online server. Your example above is closed by compute_degree! (while compute_degree leaves a 0 < 1 goal).