DecidableEq in Quotient Types

Stream: Is there code for X?

[Brandon Harad]

I am currently redefining the integers as a quotient of pairs of naturals, and am trying to create an instance of DecidableEq for my type. Ideally, I would be able to reduce decidability of equivalence of integers to decidability of some fact about naturals, which would then be easy to prove, but I can't do that without representing an element of my integers as the equivalence class of some pair of naturals. Normally, that would be induction, but I can't do that here since Decidable is a type. #mwe below:

import Mathlib

def R : (ℕ × ℕ) → (ℕ × ℕ) → Prop
  | (a, b), (c, d) => a+d = c+b

instance setoid : Setoid (ℕ×ℕ) := ⟨R, sorry⟩
def Z := Quotient setoid

instance : DecidableEq Z := λ z₁ z₂ ↦
  -- Here I'd like to decompose `z₁` and `z₂` as `⟦(a,b)⟧` and `⟦(c, d)⟧` respectively.
  sorry

[Eric Wieser]

You should prove DecidableRel R instead

[Eric Wieser]

Then you should get this instance for free

[Brandon Harad]

Ah, wonderful.

[Brandon Harad]

Relatedly, how do I prove decidability for things like relations on Z? I have a LE instance as well, that I'd like to prove is decidable, but I run into the same problem.

[Kyle Miller]

By the way, here's how you can go about defining things on a Quotient:

instance : DecidableEq Z := λ z₁ z₂ ↦
  Quotient.recOn z₁ (fun p =>
      Quotient.recOn z₂ (fun q =>
          decidable_of_iff (p.1+q.2 = q.1+p.2) (by rw [Quotient.eq]; rfl))
        sorry)
    sorry

[Brandon Harad]

@Kyle Miller Thank you, but I'm not sure how to resolve the goals you've sorry'd. I'm not even sure what they mean/are asking for.

[Kyle Miller]

They're asking for the functions to be well-defined

[Kyle Miller]

Here's Eric's suggestion also:

instance (p q : ℕ × ℕ) : Decidable (p ≈ q) :=
  match p, q with | (a, b), (c, d) => inferInstanceAs <| Decidable (a+d = c+b)

instance : DecidableEq Z := inferInstanceAs <| DecidableEq (Quotient setoid)

[Eric Wieser]

Ah, my comment "for free" was wrong, as you used def Z not abbrev Z

[Ben]

Had a similar issue. I got my example working by creating a intermediate function that mirrors the relation. There is might be a simpler way, but this worked for me

@[reducible]
def Inner: Type := Nat

def Inner.eq (a b: Inner): Prop := a = b
instance Inner.Setoid : Setoid Inner := ⟨Inner.eq, ⟨Eq.refl, Eq.symm, Eq.trans⟩⟩

@[reducible]
def MyQuotientType : Type := Quotient Inner.Setoid
def MyQuotientType.mk (a: Inner) : MyQuotientType := Quot.mk Inner.eq a

-- Unfold relation into new function
def MyQuotientType.eq (a b: MyQuotientType): Prop := Quotient.liftOn₂ a b Inner.eq (by intro _ _ _ _ h1 h2; rw [h1, h2])

-- Show function is decidable
instance MyQuotientType.eq_decidable (p q : MyQuotientType) : Decidable (p.eq q) :=
  Quotient.recOnSubsingleton₂ p q (fun a b => inferInstanceAs (Decidable (a = b)))

-- Show function is equal to `· = ·`
theorem EqEqToEq (a b: MyQuotientType): a.eq b ↔ a = b := by
  cases a using Quotient.ind
  cases b using Quotient.ind
  constructor
  {
    intro h1
    rw [h1]
  }
  {
    intro h1
    rw [h1]
    rfl
  }

-- `· = ·` is Decidable
instance MyQuotientType_eq_decidable (p q : MyQuotientType) : Decidable (p = q) :=
  decidable_of_iff (MyQuotientType.eq p q) (EqEqToEq p q)

instance : DecidableEq MyQuotientType := MyQuotientType_eq_decidable

instance (n: Nat): OfNat MyQuotientType n := ⟨MyQuotientType.mk n⟩
#eval (7: MyQuotientType) = 7
#eval (7: MyQuotientType) = 6

[Aaron Liu]

You can use the built-in instance (this also has the advantage of avoiding diamonds)

@[reducible]
def Inner: Type := Nat

def Inner.eq (a b : Inner): Prop := a = b
instance Inner.Setoid : Setoid Inner := ⟨Inner.eq, ⟨Eq.refl, Eq.symm, Eq.trans⟩⟩

@[reducible]
def MyQuotientType : Type := Quotient Inner.Setoid
def MyQuotientType.mk (a : Inner) : MyQuotientType := Quot.mk Inner.eq a

instance (a b : Inner) : Decidable (a ≈ b) :=
  inferInstanceAs (Decidable (a = b))

#check Quotient.decidableEq

instance (n : Nat): OfNat MyQuotientType n := ⟨MyQuotientType.mk n⟩
#eval (7 : MyQuotientType) = 7
#eval (7 : MyQuotientType) = 6