整数の構成に向けて：構造体とSetoid

これまでMyNatを使って自然数を自前で構成してきましたが、今回からは整数を自前で構成していきます。 この記事では、そのために必要となる構造体と同値関係について学習します。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

構造体

構造体はstructureコマンドで宣言します。 複数のデータをひとつの型としてまとめて扱うためのキーワードです。 構造体が持つデータのことをフィールドと呼びます。 以下の例ではxとyがフィールドです。

structure Point where
  x : Int
  y : Int

構造体の値を作る方法は2通りあります。 ひとつは{ }を使う方法、もうひとつはmkコンストラクタを使う方法です。

#check {x := 1, y := 2 : Point}
#check Point.mk
#check Point.mk 1 2
#eval
  let p := Point.mk 1 2
  p.x

同値関係

同値関係 r : α → α → Prop とは、次の3つの性質を持つ関係のことです。

• 反射律：r x x
• 対称律：r x y ならば r y x
• 推移律：r x y かつ r y z ならば r x z

等号は同値関係の一種であり、同値関係は等号が持つ多くの性質を共有しています。 Leanでは、同値関係であることを示す構造体Equivalenceが以下のように定義されています。

structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where
  /-- 同値関係は反射的である: `r x x` -/
  refl  : ∀ x, r x x
  /-- 同値関係は対称的である: `r x y` ならば `r y x` -/
  symm  : ∀ {x y}, r x y → r y x
  /-- 同値関係は推移的である: `r x y` かつ `r y z` ならば `r x z` -/
  trans : ∀ {x y z}, r x y → r y z → r x z

同値関係が反射的であることを示すには、reflフィールドを使います。

example {α : Type} (r : α → α → Prop) (h: Equivalence r) : ∀ x, r x x := by
  exact h.refl

同値関係を理解するために、任意の型αに対してx = yという関係を定義すると、それが必ず同値関係になることを証明します。 constructorタクティクは、Equivalence構造体を各フィールドの証明義務に分解する役割を果たします。

example {α : Type} : Equivalence (fun x y : α => x = y) := by
  constructor

  case refl =>
    intro x
    rfl

  case symm =>
    intro x y h
    rw [h]

  case trans =>
    intro x y z hxy hyz
    rw [hxy, hyz]

Setoid

Setoid（セットイド）とは、≈と表記される特定の同値関係を備えた型のことです。 同値関係r : α → α → Propそのものを、Setoid αという型クラスで表現します。 Leanでは、Setoidは以下のように定義されています。

class Setoid (α : Sort u) where
  /-- `x ≈ y` は、Setoid における特定の同値関係です。 -/
  r : α → α → Prop
  /-- 関係 `x ≈ y` は同値関係です。 -/
  iseqv : Equivalence r

次回は、この構造体と同値関係を使って、MyNatのペアから整数を構成していきます。

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