整数MyIntを前順序Preorderとして登録する

今回は、MyIntを順序集合として扱えるようにしていきます。まず前順序（preorder）を導入し、MyNatからMyIntへの型キャストを整備したうえで、広義順序と狭義順序を定義し、MathlibのPreorder型クラスに登録してorderタクティクを使えるようにします。本記事は「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」を参考に進めています。

前順序とは

集合Xの上の二項関係が以下の2つの性質を満たすとき、その関係は前順序であると呼ばれます。

反射律: \( \forall x \in X,\ x \le x \)
推移律: \( \forall x, y, z \in X,\ x \le y \land y \le z \to x \le z \)

MyIntはこの2つの性質を満たすため、前順序として扱うことができます。Mathlibが用意しているPreorder型クラスのインスタンスとして登録していきます。

MyNatをMyIntとして扱う

順序を定義する前に、自然数も整数として扱えるようにしておきます。現状では、MyIntを引数にとる関数にMyNatをそのまま渡すとエラーになります。

private def MyInt.const (z : MyInt) : MyInt → MyInt := fun _ => z

#check_failure MyInt.const (0 : MyNat)

MyIntの引数として渡す前に、以下のように変換する必要があります。

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

#check MyInt.const (.ofMyNat 0)

Lean4の型強制（coercion）という仕組みを使うと、MyNatをMyIntへ強制的に変換することができます。

instance : Coe MyNat MyInt where
  coe := MyInt.ofMyNat

-- (MyInt.ofMyNat 0).const : MyInt → MyInt
#check MyInt.const (0 : MyNat)

ただし、この指定方法では単なるキャストではなく、常に強制的に型変換が行われてしまいます。

example : ((0 : MyNat): MyInt) = (0 : MyInt) := by
  guard_target =ₛ MyInt.ofMyNat 0 = 0
  sorry

MyNatとMyIntのように部分集合の関係にある型は、型変換として扱えたほうが便利です。型キャストはcoe属性にMyInt.ofMyNatを登録することで実現できます。

attribute [coe] MyInt.ofMyNat

先ほどのexampleを見ると、↑(0 : MyNat)のようにMyNatが型キャストとして扱われていることが分かります。↑は型キャストであることを示す記号です。

@[simp]
theorem MyInt.ofMyNat_zero_eq_zero : MyInt.ofMyNat 0 = (0: MyInt) := by
  dsimp [MyInt.ofMyNat]
  rfl

example : ((0 : MyNat): MyInt) = (0 : MyInt) := by
  guard_target =ₛ ↑(0 : MyNat) = (0 : MyInt)
  simp

型キャストが単射であることを証明する

この型キャストが単射であることを証明します。norm_castは型キャストを扱うタクティクに登録するための属性です。

@[norm_cast]
theorem MyInt.ofMyNat_inj {m n : MyNat}
  : (m : MyInt) = (n : MyInt) ↔ m = n := by
    constructor <;> intro h
    case mp =>
      have : (m, 0) ≈ (n, 0) := by
        exact Quotient.exact h
      notation_simp at this
      simp_all
    case mpr =>
      rw [h]

norm_castタクティクは以下のように使用できます。

@[simp]
theorem MyInt.ofMyNat_eq_zero {n : MyNat} : (n : MyInt) = 0 ↔ n = 0 := by
  constructor <;> intro h
  · rw [show (0 : MyInt) = ↑ (0 : MyNat) from rfl] at h
    norm_cast at h
  · simp_all

push_cast属性を登録しておくと、ringのようなタクティクを実行する前に型キャストを展開してくれます。型キャストは括弧の内側に展開されます。

@[push_cast]
theorem MyInt.ofNat_add (m n : MyNat)
  : ↑ (m + n) = (m : MyInt) + (n : MyInt) := by
    rfl

MyIntの広義順序と狭義順序を定義する

MyIntの広義順序（≤）と狭義順序（<）を定義します。

def MyInt.le (m n : MyInt) : Prop :=
  ∃ k : MyNat, m + ↑ k = n

instance : LE MyInt where
  le := MyInt.le

@[notation_simp]
theorem MyInt.le_def (m n : MyInt) : m ≤ n ↔ ∃ k : MyNat, m + ↑ k = n := by
  rfl

def MyInt.lt (m n : MyInt) : Prop :=
  m ≤ n ∧ ¬ n ≤ m

instance : LT MyInt where
  lt := MyInt.lt

@[notation_simp]
theorem MyInt.lt_def (a b : MyInt) : a < b ↔ a ≤ b ∧ ¬ (b ≤ a) := by
  rfl

反射律を証明する

@[refl]
theorem MyInt.le_refl (m : MyInt) : m ≤ m := by
  exists 0
  simp

推移律を証明する

続いて推移律を証明します。notation_simpで和の形に変形し、use a + bでゴールを⊢ n + ↑(a + b) = kに、push_castで⊢ n + (↑a + ↑b) = kに変形するのがポイントです。あとは仮定とac_rflでゴールへ変形できます。

theorem MyInt.le_trans {m n k : MyInt} (hnm: n ≤ m) (hmk: m ≤ k) : n ≤ k := by
  notation_simp at *
  obtain ⟨a, ha⟩ := hnm
  obtain ⟨b, hb⟩ := hmk
  -- a : MyNat
  -- ha : n + ↑a = m
  -- b : MyNat
  -- hb : m + ↑b = k
  -- ⊢ ∃ k_1, n + ↑k_1 = k
  use a + b -- ⊢ n + ↑(a + b) = k
  push_cast -- ⊢ n + (↑a + ↑b) = k

  have : n + (↑ a + ↑ b) = k := calc
    _ = (n + ↑ a) + ↑ b := by ac_rfl
    _ = m + ↑ b := by rw [ha]
    _ = k := by rw [hb]
  assumption

calcタクティクで使用できるように、推移律をTransクラスへ登録します。

instance : Trans (· ≤ · : MyInt → MyInt → Prop) (· ≤ ·) (· ≤ ·) where
  trans := MyInt.le_trans

Preorderへの登録

最後に前順序へ登録し、orderタクティクを使えるようにします。

instance : Preorder MyInt where
  le_refl := MyInt.le_refl
  le_trans := by
    intro a b c hab hbc
    apply MyInt.le_trans hab hbc

example (a b c : MyInt) (h1: a ≤ b) (h2 : b ≤ c) : a ≤ c := by
  order

Preorderインスタンスとして登録したことで、orderタクティクが反射律と推移律を自動的に扱ってくれるようになりました。

コードはGitHubリポジトリにて公開しています。