Dealing with 0 * 0 not defeq 0 in Rat

Stream: general

[Joseph Tooby-Smith]

I'm trying to bump HepLean from 4.12.0 to 4.13.0. But I'm running into a problem.

There are a number of results which are complicated expressions in the rationals that are actually equal to zero.
In 4.12.0 these could be solved with`rfl' but now they can't. I think this boils down to the fact that for 4.12.0

import Mathlib

example : (0 : ℚ) * 0 = 0 := by
  rfl

works but does not work in 4.13.0 (I'm unsure about the releases in-between).

I can't actually seem to find the change which means this no longer works, but in any case, are there any suggestions on how I overcome this? The tactic `norm_num' etc does not work for the expressions that I have.

[Kyle Miller]

The change is that well-founded recursion is irreducible by default now. You can "unseal" such definitions on a case-by-case basis:

unseal Rat.mul in
example : (0 : ℚ) * 0 = 0 := by
  rfl

[Eric Wieser]

I'm guessing this comes up in dimensional analysis?

[Eric Wieser]

Can you give an example of norm_num failing?

[Joseph Tooby-Smith]

@Eric Wieser These sort of things actually came up solving what are called the anomaly cancellation conditions. These are a set of polynomials in the rational parameters (which correspond to physical charges one can assign to the fermions which make up the universe). The polynomials must be zero for a theory to be well defined.

Here is a toy example of norm_num failing:

import Mathlib

def f : Fin 4 → ℚ := ![0, 1, 3, 4]

example :  f 0 + f 0  * f 0 + f 0 = 0 := by
  norm_num

The actual examples I have are of a similar variety but a lot more complicated, meaning it is unfeasible to unfold all of the definitions. Here is an example of one of the theorems which is actually breaking.

I'll try @Kyle Miller suggestion tomorrow. Many thanks

[Eric Wieser]

example :  f 0 + f 0  * f 0 + f 0 = 0 := by
  norm_num [f]

works there

[Yury G. Kudryashov]

Relying on definitional equality is a very fragile design pattern. It can break for reasons out of your control.

[Joseph Tooby-Smith]

@Eric Wieser Ok, the following example is more representative of the problem I'm facing:

import Mathlib


example :  ∑ x : Fin 3,
        (![1, (0 : ℚ), 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((0 : Fin 6), x)) *
        ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((0 : Fin 6), x)) +
      -(2 * (![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((1 : Fin 6), x)) * ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((1 : Fin 6), x)))) +
      ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((2 : Fin 6), x)) * ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((2 : Fin 6), x)) + -(![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((3 : Fin 6), x)) *
      ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((3 : Fin 6), x))) +
      ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((4 : Fin 6), x)) *
      ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((4 : Fin 6), x))) = 0 := by
    norm_num

@Yury G. Kudryashov Indeed - seems like I'm suffering the consequences of this now.

[Daniel Weber]

native_decide gives a very weird error message here

application type mismatch
  Lean.ofReduceBool _example._nativeDecide_1 true (Eq.refl true)
argument has type
  true = true
but function has type
  Lean.reduceBool _example._nativeDecide_1 = true → _example._nativeDecide_1 = true

[Daniel Weber]

It's actually equal to one, not zero, and you can use with_unfolding_all decide to prove it:

import Mathlib

example :  ∑ x : Fin 3,
        (![1, (0 : ℚ), 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((0 : Fin 6), x)) *
        ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((0 : Fin 6), x)) +
      -(2 * (![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((1 : Fin 6), x)) * ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((1 : Fin 6), x)))) +
      ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((2 : Fin 6), x)) * ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((2 : Fin 6), x)) + -(![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((3 : Fin 6), x)) *
      ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((3 : Fin 6), x))) +
      ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((4 : Fin 6), x)) *
      ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] (finProdFinEquiv ((4 : Fin 6), x))) = 1 := by
    with_unfolding_all decide

[Joseph Tooby-Smith]

@Daniel Weber Indeed, that was my fault. This should actually equal 1.
Thanks for the with_unfolding_all decide tactic idea! This seems to work for my general cases.