ring/ bound/ simp/ grind

Stream: metaprogramming / tactics

[Alex Kontorovich]

I'm wondering if this is the expected behavior?

import Mathlib

example (n : ℕ) : (-1 : ℝ) ^ (2 * (n + 1) + 2) = 1 := by
  -- `simp` made no progress
  -- `ring` doesn't close it
  -- `bound` fails
  -- `grind` fails
  ring_nf
  bound

Thanks!

[Jovan Gerbscheid]

I think it would be a reasonable feature for ring to cancel minus signs that sit under an even exponent. (cc @Arend Mellendijk, this might give another reason to store the constant factor/offset at the head of the list instead of the end, in the internal ExSum/ExProd types)