panic while testing ring tactic

Stream: mathlib4

[Scott Morrison]

I was thinking about benchmarking the new ring tactic, available now in mathlib4, but encountered a panic:

import Mathlib.Tactic.Ring

-- Causes `PANIC at Lean.Expr.getRevArg! Lean.Expr:508:22: invalid index`:
example (A B C D E F G H I J : ℕ) : ((((((1 : ℕ) ^ 2) + (((((((J ^ 1) + F) * (1 : ℕ)) ^ 0) * (1 : ℕ)) * (((B ^ 1) ^ 0) * (D + (C + (0 : ℕ))))) * ((J * ((1 : ℕ) + (((1 : ℕ) + ((2 : ℕ) + ((I * (H ^ 1)) * (1 : ℕ)))) ^ 0))) ^ 1))) + (((A * (((1 : ℕ) ^ 1) ^ 0)) + ((A + (((1 : ℕ) ^ 1) + (1 : ℕ))) ^ 0)) + (((1 : ℕ) ^ 1) + D))) ^ 2) ^ 2) = ((((((1 : ℕ) ^ 2) + (((((((J ^ 1) + F) * (1 : ℕ)) ^ 0) * (1 : ℕ)) * (((B ^ 1) ^ 0) * (D + (C + (0 : ℕ))))) * ((J * ((1 : ℕ) + (((1 : ℕ) + ((2 : ℕ) + ((I * (H ^ 1)) * (1 : ℕ)))) ^ 0))) ^ 1))) + (((A * (((1 : ℕ) ^ 1) ^ 0)) + ((A + (((1 : ℕ) ^ 1) + (1 : ℕ))) ^ 0)) + (((1 : ℕ) ^ 1) + D))) ^ 2) ^ 2) := by ring

[Scott Morrison]

I've minimised this to:

import Mathlib.Tactic.Ring

-- Causes `PANIC at Lean.Expr.getRevArg! Lean.Expr:508:22: invalid index`:
example (A : ℕ) : (2 * A) ^ 2 = (2 * A) ^ 2 := by ring

I also added this as a (failing) test as Mathlib/Test/Ring.lean.

@Aurélien Saue, do you have a guess what is happening here? I can break out the debugger otherwise.

[Notification Bot]

This topic was moved here from #lean4 > panic while testing ring tactic by Scott Morrison

[Daniel Selsam]

Scott Morrison said:

I was thinking about benchmarking the new ring tactic, available now in mathlib4,

It would be great to compare against Coq's ring tactic as well. Last I checked on (x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8)^15 it was much faster than either of the Lean3 implementations.

[Scott Morrison]

The same panic error prevents us testing Mathlib4's ring on this example.

[Scott Morrison]

I think a good thing to test is (x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8)^15 = (x8 + x7 + x6 + x5 + x4 + x3 + x2 + x1)^15. Asking for proofs of equations is more interesting that finding normal forms.

Coq takes about 5s on my laptop to do this.

[Daniel Selsam]

Scott Morrison said:

I think a good thing to test is (x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8)^15 = (x8 + x7 + x6 + x5 + x4 + x3 + x2 + x1)^15. Asking for proofs of equations is more interesting that finding normal forms.

Coq takes about 5s on my laptop to do this.

Agreed, just beware the gotcha: some ring tactics are clever enough to avoid normalizing when proving certain equalities. For example, IIR at least one of Mario's lean3 ring tactics would solve this instantly:

(x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8)^15 = (x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + 0)^15

[Scott Morrison]

Coq is indeed way faster than either ring or ring_exp in Lean3. Even replacing ^15 with ^5, both Lean tactics are slower than Coq (still at ^15).

[Daniel Selsam]

FYI Coq's ringtactic is reflexive (like Lean3's ring2 tactic) but the Coq kernel has special support for trusted (and pretty-fast) computation. It is not clear to me yet how competitive a proof-producing procedure can be on benchmarks like that.

[Mario Carneiro]

Fixed (it was a bug in normNum, not ring, when you try to normalize a raw nat literal).

[Mario Carneiro]

Although it calls into question why ring is calling normNum with raw literals

[Aurélien Saue]

@Scott Morrison @Mario Carneiro There was a bug in ring too I will pull request in a minute :)