Introducing Quotient.mk and ⟦⟧ Notation for MyInt — Numeric Literals and the Minus Sign

Last time we defined the equivalence relation (Setoid) that underlies MyInt. This time we'll use Quotient.mk to actually obtain values of MyInt from terms of PreInt, and make MyInt work with numeric literals and the minus sign. This article follows along with 「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」.

Getting a term with Quotient.mk

Let's try getting a term of PreInt using the Quotient.mk we created.

#check
  let a : PreInt := (1, 3)
  (Quotient.mk PreInt.sr a : MyInt)
  (Quotient.mk _ a)

Defining the ⟦⟧ notation

Writing Quotient.mk every time is tedious, so let's define ⟦⟧. It converts to the underlying Quotient.mk call.

notation:arg "⟦" a "⟧" => Quotient.mk _ a

#check (⟦(1, 3)⟧ : MyInt)

Treating MyInt as a numeric literal

Next, let's make it possible to treat MyInt as a numeric literal.

def MyInt.ofNat (n : Nat) : MyInt := ⟦(MyNat.ofNat n, 0)⟧

instance {n : Nat} : OfNat MyInt n where
  ofNat := MyInt.ofNat n

#check (4 : MyInt)

Supporting the minus sign

Next, let's make it possible to use the minus sign. To do this we need to register a neg instance for MyInt.

instance : Neg MyInt where
  neg := MyInt.neg

Defining PreInt.neg

First, let's define PreInt.neg. The negation of (m, n) is (n, m). Since \( -(m - n) = n - m \), sign flipping (negation) corresponds to the operation of swapping the components, \( (m, n) \mapsto (n, m) \).

def PreInt.neg : PreInt → MyInt
  | (m, n) => ⟦(n, m)⟧

A lemma for unfolding the equivalence relation

As preparation, let's also prove a lemma that unfolds the definition of the equivalence m ≈ n.

@[notation_simp]
theorem MyInt.sr_def (m n : PreInt) : m ≈ n ↔ m.1 + n.2 = m.2 + n.1 := by
  rfl

Defining MyInt.neg

Now let's define MyInt.neg. Quotient.lift PreInt.neg changes the domain of PreInt.neg to MyInt, the quotient of PreInt. To use Quotient.lift, we need to prove that PreInt.neg preserves the equivalence relation — that is, that the negations of two equivalent PreInt terms are themselves equivalent.

def MyInt.neg : MyInt → MyInt := Quotient.lift PreInt.neg <| by
  -- ⊢ ∀ (a b : PreInt), a ≈ b → a.neg = b.neg
  intro (a1, a2) (b1, b2) hab

  suffices (a2, a1) ≈ (b2, b1) from by
    dsimp [PreInt.neg]
    rw [Quotient.sound]
    assumption

  notation_simp at *
  simp_all

This makes it possible to interpret -4 as a MyInt.

#check (-4: MyInt)
#check_failure -4

The full code is available in the GitHub repository.