congr 1 hangs

Stream: lean4

[Bolton Bailey]

I have the following example

import Mathlib

open MvPolynomial

example
    (map : Nat → ℤ) :
    (eval map) ((X 0 + X 1) * (X 2 + X 3) * (X 4 + X 5)) = (eval map) ((X 1 + X 0) * (X 2 + X 3) * (X 4 + X 5)) := by
  congr 1 -- hangs

Why does this hang here? If I remove (X 4 + X 5), it works as I expect.

[Kyle Miller]

It seems to be that congr is hanging trying to prove the resulting expression is true by rfl.

Two workarounds:

• use with_reducible congr 1
• use congr! (config := {closePost := false}) 1

[Kevin Buzzard]

Is it expected that

import Mathlib

open MvPolynomial

example :
    ((X 0 + X 1) * (X 2 + X 3) * (X 4 + X 5)) =
    ((X 1 + X 0) * (X 2 + X 3) * (X 4 + X 5) : MvPolynomial ℕ ℕ) := by
  rfl -- hangs

hangs then?

[Bolton Bailey]

Nice catch. Minimizing even further, the Xs seem to be unnecessary for the hang to manifest.

import Mathlib

example :
    ((0 + 1) * 2 * 3) =
    ((1 + 0) * 2 * 3 : MvPolynomial ℕ ℕ) := by
  rfl -- hangs

[Kim Morrison]

Now lets work on that import Mathlib line. :-)

[Bolton Bailey]

Yeah I tried changing it to Polynomial ℕ but that no longer hangs.

[Bolton Bailey]

So the type is important somehow.

[Kyle Miller]

I'm not too surprised it takes so long. These expressions are theoretically computable, but MvPolynomial isn't very computationally efficient.

It turns out this doesn't even succeed:

example :
    0 + 1 =
    (1 + 0  : MvPolynomial ℕ ℕ) := by
  rfl

It doesn't time out, it fails.

There's also a DecidableEq instance, but by decide gets stuck here. Here's one part of it that's getting stuck:

example :
    ∀ a ∈ (0 + 1 : MvPolynomial ℕ ℕ).support,
    (0 + 1 : MvPolynomial ℕ ℕ).toFun a = (1 + 0 : MvPolynomial ℕ ℕ).toFun a := by
  decide

It's able to synthesize a decidable instance, but it can't reduce the instance.

[Kevin Buzzard]

Just to say: I don't expect rfl to work, I just didn't expect it to hang :-)

[Bolton Bailey]

Me too. I guess what we are being told is "while this looks like a simple computation, it is actually not simple for weird low-level details of MvPolynomial that make the algorithm that rfl runs unexpectedly but correctly take forever / a long time"?

[Eric Wieser]

It's able to synthesize a decidable instance, but it can't reduce the instance.

The decidability instance uses Classical.choice, so it isn't reducible

[Eric Wieser]

Ah, I think the problem is that docs#Multiset.decidableForallMultiset goes through a quotient type, and so can't be reduced without unfolding until a Quotient.mk appears

[Eric Wieser]

And the Quotient.mk never appears, because there is a classical if hiding in the addition which can't be further reduced

[Floris van Doorn]

Note: I made docs#MonoidAlgebra.mul' irreducible a little while ago. We should make many such operations irreducible.