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