Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The tactic decide seems to be looking inside definitions marked @[irreducible]. False statements involving @[irreducible] definitions fail slowly (presumably because decide is unfolding the definitions), and true statements involving @[irreducible] definitions can be proved.

Steps to Reproduce

structure Foo where num : Nat deriving DecidableEq

namespace Foo

instance : OfNat Foo n := ⟨⟨n⟩⟩

/-! # Example 1 -/

@[irreducible] def mul (a b : Foo) : Foo :=
  let d := Nat.gcd a.num 1
  ⟨(a.num.div d) * (b.num.div d)⟩

example : ((Foo.mul 4 1).mul 1).mul 1 = 4 := by decide

/-! # Example 2 -/

@[irreducible] def add (a b : Foo) : Foo := ⟨a.num * b.num⟩

example : ((Foo.add 4 1).add 1).add 1 = 4 := by decide

Expected behavior: Expect both examples to fail quickly.

Actual behavior: Example 1 fails slowly (16s for me), and Example 2 succeeds.

Reproduces how often: 100%

Versions

nightly-2023-03-15

Additional Information

@digama0 and I encountered this while investigating the following slow example in Std:

import Std.Data.Rat.Basic

example : (4:Rat) * 1 * 1 + 4 = 0 := by decide -- fails, takes 3.17s