Lean4における自作整数の数値リテラルとマイナス記号への対応

前回はMyIntの元となる同値関係（Setoid）を定義しました。今回はQuotient.mkを使ってPreIntの項から実際にMyIntの値を取得し、数値リテラルやマイナス記号を扱えるようにしていきます。本記事は「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」を参考にしています。

Quotient.mkで項を取得する

作成したQuotient.mkを使ってPreIntの項を取得してみます。

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

⟦⟧記法の定義

毎回、Quotient.mkを書くのは面倒なので、⟦⟧を定義します。⟦⟧で変換できます。

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

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

数値リテラルとして扱う

さらに数値リテラルとしてMyIntを扱えるようにします。

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

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

#check (4 : MyInt)

マイナス記号に対応する

さらにマイナス記号を扱えるようにします。そのためには、MyIntのnegを登録する必要があります。

instance : Neg MyInt where
  neg := MyInt.neg

PreInt.negの定義

まずは、PreInt.negを定義します。(m, n)のマイナス値は(n, m)です。\( -(m - n) = n - m \) なので、符号反転（マイナス）は成分を入れ替える操作 \( (m, n) \mapsto (n, m) \) に対応します。

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

同値関係を展開する補題

さらに、準備として同値（m ≈ n）であることの定義式を展開するための補題を証明します。

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

MyInt.negの定義

そして、MyInt.negを定義します。Quotient.lift PreInt.negでPreInt.negの定義域をPreIntの商であるMyIntに変更します。Quotient.liftを使用するにはPreInt.negが同値関係を保つことを証明する必要があります。つまり、同値なPreIntのnegもまた同値であることを示します。

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

これにより-4をMyIntとして解釈できるようになりました。

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

コードの全体はGitHubリポジトリで公開しています。