You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
structureFoowherenum : Nat deriving DecidableEq
namespace Foo
instance : OfNat Foo n := ⟨⟨n⟩⟩
/-! # Example 1 -/@[irreducible]defmul (a b : Foo) : Foo :=
let d := Nat.gcd a.num 1
⟨(a.num.div d) * (b.num.div d)⟩
example : ((Foo.mul 41).mul 1).mul 1 = 4 := by decide
/-! # Example 2 -/@[irreducible]defadd (a b : Foo) : Foo := ⟨a.num * b.num⟩
example : ((Foo.add 41).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
The text was updated successfully, but these errors were encountered:
Prerequisites
Description
The tactic
decide
seems to be looking inside definitions marked@[irreducible]
. False statements involving@[irreducible]
definitions fail slowly (presumably becausedecide
is unfolding the definitions), and true statements involving@[irreducible]
definitions can be proved.Steps to Reproduce
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:
The text was updated successfully, but these errors were encountered: