zmod decidability

Stream: mathlib4

[Heather Macbeth]

I'm very confused by a decidability failure involving ZMod, see below. The failure is very fragile - - reversing argument order makes it go away, as does removing an intro/revert pair, changing ZMod to Fin, or changing the associativity in P. I was also not able to make it smaller by removing clauses of P (I'm not sure I tried each clause, but I tried several).

Any ideas what the issue is here?

import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.DeriveFintype

structure Foo :=
  (x : ZMod 3)
  (i : ZMod 2)
deriving Fintype, DecidableEq

abbrev f (e : Foo) : Finset Foo := {e}

abbrev P (j k : ZMod 2) (x : ZMod 3) : Prop :=
  let a := Foo.mk 0 0
  ¬ ((Foo.mk x 0 ≠ ⟨0, 0⟩ ∧ Foo.mk 0 0 ≠ ⟨0, k⟩ ∧ ⟨x, 0⟩ ∈ f (Foo.mk 0 0))
  ∧ (Foo.mk 0 0 ≠ ⟨0, 0⟩ ∧ Foo.mk 0 k ≠ ⟨0, j⟩ ∧ ⟨0, 0⟩ ∈ f (Foo.mk 0 k) ∧ ⟨0, 0⟩ ∈ f (Foo.mk 0 j))
  ∧ (Foo.mk 0 0 ≠ ⟨x, 0⟩ ∧ Foo.mk 0 j ≠ a ∧ ⟨0, 0⟩ ∈ f (Foo.mk 0 j) ∧ ⟨0, 0⟩ ∈ f a))

example {j k : ZMod 2} {x : ZMod 3} : P j k x := by
  dsimp only [P]
  intro h
  revert x j k
  decide -- fails

-- bug disappears after reversing argument order
example {x : ZMod 3} {j k : ZMod 2} : P j k x := by
  dsimp only [P]
  intro h
  revert x j k
  decide -- works

-- bug disappears after pattern-matching part of the goal
example {j k : ZMod 2} {x : ZMod 3} : P j k x := by
  dsimp only [P]
  intro ⟨h1, h2⟩
  revert x j k
  decide -- works

-- bug disappears without spurious introduction/reversion of negation in goal
example {j k : ZMod 2} {x : ZMod 3} : P j k x := by
  dsimp only [P]
  revert x j k
  decide -- works

-- bug disappears if use `Fin` rather than `ZMod`
example {j k : Fin 2} {x : Fin 3} : P j k x := by
  dsimp only [P]
  intro h
  revert x j k
  decide -- works

[Eric Wieser]

This is a lot less painful to debug as

abbrev nP (j k : ZMod 2) (x : ZMod 3) : Prop :=
  let a := Foo.mk 0 0
  ((Foo.mk x 0 ≠ ⟨0, 0⟩ ∧ Foo.mk 0 0 ≠ ⟨0, k⟩ ∧ ⟨x, 0⟩ ∈ f (Foo.mk 0 0))
  ∧ (Foo.mk 0 0 ≠ ⟨0, 0⟩ ∧ Foo.mk 0 k ≠ ⟨0, j⟩ ∧ ⟨0, 0⟩ ∈ f (Foo.mk 0 k) ∧ ⟨0, 0⟩ ∈ f (Foo.mk 0 j))
  ∧ (Foo.mk 0 0 ≠ ⟨x, 0⟩ ∧ Foo.mk 0 j ≠ a ∧ ⟨0, 0⟩ ∈ f (Foo.mk 0 j) ∧ ⟨0, 0⟩ ∈ f a))

abbrev P (j k : ZMod 2) (x : ZMod 3) : Prop :=
  ¬ nP j k x

[Heather Macbeth]

Sorry Eric, I didn't understand this comment ... what is the issue? (Thanks for looking)

[Eric Wieser]

Oh I have no idea what the issue is, but that makes the goal view at the failure a lot shorter!

[Heather Macbeth]

Ah! :)

[Mario Carneiro]

It appears to be an issue with the instance size limit. set_option synthInstance.maxSize 200 in decide fixes the issue