How do I define decidableLE for simple quotient type.

Stream: mathlib4

[Kent Van Vels]

I am implementing my own version of the Integers in lean4 just for the practice. I define the Integers as an quotient of ordered pairs of Naturals numbers with an appropriate equivalence relation. I am following the Zmod37 example set forward in Kevin Buzzard's "Formalizing Mathematics" class.

I have a most of the results I need to claim that my integer class is a linear order. But I am stuck trying to show the DecidableLE (and most likely the DecidableEQ) field in the struct. The relevant code is a follows

import Mathlib.Data.Nat.Basic

def N2 := ℕ × ℕ

--my equivalence relation
def rel (ab cd : N2) : Prop :=
  ab.1 + cd.2 = ab.2 + cd.1

--the "sorry" here is the omitted proof that `rel` is indeed an equivalence relation
instance mysetoid : Setoid N2 := ⟨rel,sorry⟩

attribute [instance] mysetoid
def Z := Quotient mysetoid
attribute [instance] Z

def le_aux (ab cd : N2) : Prop :=
  ∃ (z : ℕ), (ab.fst + cd.snd) + z =  (cd.fst + ab.snd)

--here we lift that aux definition to the Quotient.
def le : Z → Z → Prop := by
  apply Quotient.lift₂ le_aux
  rintro ⟨a10,a11⟩ ⟨b10,b11⟩ ⟨a20,a21⟩ ⟨b20,b21⟩ ha hb
  sorry --I have the proof that goes here

instance : LE Z := ⟨le⟩

instance : LinearOrder Z := {
  --I have most of the proofs needed here
  decidableLE := sorry --what do I do here?
}

It seems that since my le_aux is decidable, (it is equivalent to saying that ab.fst + cd.snd ≤ cd.fst + ab.snd ) it should be straight-forward to claim that le is decidable. I don't know how to do this though.

Please let me know if this is the incorrect board to post this question. I appreciate any pointers.

I am using Lean version 4.0.0-nightly-2023-06-20, commit a44dd71ad62a

[Yury G. Kudryashov]

Why not define le_aux as ab.1 + cd.1 ≤ cd.1 + ab.2?

[Yury G. Kudryashov]

As for the original question, you can do induction on both arguments (or just rintro them).

[Yury G. Kudryashov]

Then your goal will be defeq Decidable (le_aux a b)

[Kent Van Vels]

I originally did, I thought this would be easier/better for some reason.

I just changed it back, and I still need to define decidableLE

[Kent Van Vels]

I didn't see your 2nd and third posts. After rintroing a an b ,I get a goal of Decidable (a ≤ b), where a and b are in Z, not N2. (I don't get a goal of Decidable (le_aux a b) ) I tried using
induction' a using Quotient.inductionOn with aa as I used that incantation for my other proofs but it complains of a type mismatch.

[Yury G. Kudryashov]

You can rintro ⟨a⟩ ⟨b⟩; change Decidable (le_aux a b)

[Yury G. Kudryashov]

You can also use docs#Quotient.lift₂.decidablePred

[Yury G. Kudryashov]

linkifier failed: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Quot.html#Quotient.lift%E2%82%82.decidablePred

[Kent Van Vels]

Thanks for your help and your looking into this. Unfortunately, when I do rintro ⟨a⟩ ⟨b⟩, it complains of an invalid constructor. And if I do intro a b instead, then a and bare Z's not N2's (so I can't change the goal to le_aux a b. I can't find Quotient.lift₂.decidablePred used anywhere in Mathlib, so I don't know how it is supposed to be used. Do you have any ideas?

[Yury G. Kudryashov]

import Mathlib.Data.Nat.Order.Basic

def N2 := ℕ × ℕ

--my equivalence relation
def rel (ab cd : N2) : Prop :=
  ab.1 + cd.2 = ab.2 + cd.1

--the "sorry" here is the omitted proof that `rel` is indeed an equivalence relation
instance mysetoid : Setoid N2 := ⟨rel, fun _ ↦ add_comm _ _,
  fun h ↦ by simpa [rel, add_comm, eq_comm] using h,
  fun {x y z} h₁ h₂ ↦ add_left_cancel (a := y.1 + y.2) <| by
    convert congr_arg₂ (· + ·) h₁ h₂ using 1 <;> simp [add_comm, add_left_comm, add_assoc]⟩

def Z := Quotient mysetoid

def le_aux (ab cd : N2) : Prop := ab.1 + cd.2 ≤ ab.2 + cd.1

instance : DecidableRel le_aux := fun _ _ ↦ inferInstanceAs (Decidable (_ ≤ _))

theorem le_aux_quot (a b c d : N2) (hac : a ≈ c) (hbd : b ≈ d) : le_aux a b = le_aux c d := by
    change _ = _ at hac hbd
    rw [le_aux, ← add_le_add_iff_right (c.2 + d.1), add_add_add_comm, hac, ← hbd]
    simp only [add_assoc, add_le_add_iff_left]
    rw [add_left_comm, add_le_add_iff_left, le_aux]

--here we lift that aux definition to the Quotient.
def le : Z → Z → Prop := Quotient.lift₂ le_aux le_aux_quot

instance : DecidableRel le := Quotient.lift₂.decidablePred _ le_aux_quot

[Kent Van Vels]

Thank you. I am going to sleep now, but I will look at this in the morning. I really appreciate it!

[Kent Van Vels]

I got that part working. I truly do appreciate your help. Now, I am trying to show the following

def myDecEq (a b : Z) : Decidable (a = b) := by sorry

(this is what the field decidableEq requires in LinearOrder) I have tried using the normal tactics of induction' a using Quotient.inductionOn with aa but it complains about that. I appreciate any help.

[Kyle Miller]

There's already an instance for this, but you have to write some instances to unfold the definition for Lean to see it:

instance (ab cd : N2) : Decidable (ab ≈ cd) := inferInstanceAs <| Decidable (_ = _)

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

[Kyle Miller]

The first one says "the setoid relation is decidable because it's defined using natural number equality" and this is fed
implicitly into the second one, which is getting it to see that docs#instDecidableEqQuotient applies

[Kent Van Vels]

Thank you. I appreciate it.