文字列変換

特に命題が複雑になってきたときには、(Leanの)変数に格納されている論理式を表示してチェックしたい。そのような機構はMathlib.ModelTheoryにはない。本格的に公理化された集合論のモデルをやり始める前に、これをやっておきたかった。

まず∈と∉の中置書法を定義する。前回もやったのだけれども、優先度を大幅に上げた。論理記号よりも先に処理されてほしいからである。

def ϕelt {α : Type} {n : ℕ} (t1 : LSet.Term (α ⊕ Fin n)) (t2 : LSet.Term (α ⊕ Fin n)) :=
  Relations.boundedFormula₂ is_elt_of₂ t1 t2
infixl : 120 " ∈ " => ϕelt

def ϕnot_elt {α : Type} {n : ℕ} (t1 : LSet.Term (α ⊕ Fin n)) (t2 : LSet.Term (α ⊕ Fin n)) :=
  ∼(Relations.boundedFormula₂ is_elt_of₂ t1 t2)
infixl : 120 " ∉ " => ϕnot_elt

まず項を文字列変換する。関数記号がない前提なので下記でOK。なお、toStringにして多相にできないかと思ったのだけれども、TermとBoundedFormula両方をとれるtoStringを作るというのは型クラスの話になってTermやBoundedFormulaの定義から変えないといけないのでやめておく。将来的にはそれらを付け加えるプルリク？とやらに挑戦してみても良いと思うが。

def TermToString {n : ℕ} (t : LSet.Term (ℕ ⊕ Fin n)) :=
match t with
| Term.var (Sum.inl k) => s!"fv{k}"
| Term.var (Sum.inr k) => s!"bv{k}"
| _ => "error"

def TermTupleToString {n : ℕ} {m : ℕ} (ts : Fin m → LSet.Term (ℕ ⊕ Fin n)) (k : ℕ): String := 
  match m with 
  | 0 => "error"
  | m' + 1 => TermToString (ts (Fin.ofNat' (m' + 1) k))

s!は最近の言語にはよくある{}内を展開してくれるやつ。

TermTupleToStringは関数で表現された項タプルtsとkを受け取ってts kを文字列化して返す。Fin 0は空なのでmが0でないという証明(NeZero mの元)が必要になる。これをどうしたらよいかわからなかったのだけれども、match mでm=0とそれ以外のケースに分ければよいことがわかった。

これができればFormulaToStringも簡単にできる。

def FormulaToString {n : ℕ} (ϕ : LSet.BoundedFormula ℕ n) : String :=
match ϕ with
| BoundedFormula.falsum => "⊥"
| BoundedFormula.equal t1 t2 => s!"{TermToString t1} = {TermToString t2}"
| BoundedFormula.rel is_elt_of₂ ts =>
    s!"{TermTupleToString ts 0} ∈ {TermTupleToString ts 1}"
| BoundedFormula.imp ϕ1 ϕ2 => s!"{FormulaToString ϕ1} ⟹ {FormulaToString ϕ2}"
| BoundedFormula.all ϕ1 => s!"∀'bv{n}({FormulaToString ϕ1})"

いろいろ表示させてみる。いや、これだとほぼそのまま返ってくるだけなんだけど。

#eval FormulaToString ϕbot
#eval FormulaToString ((fv 0 0)='(fv 0 1))
#eval FormulaToString ((fv 0 0)∈(fv 0 1))
#eval FormulaToString (ϕbot ⟹ ϕbot)
#eval FormulaToString (∀'((bv 1 0)∈(fv 1 0)))
#eval FormulaToString (∃' ∀'((bv 2 1)∈(bv 2 0)))
#eval FormulaToString ((fv 0 0)='(fv 0 1) ⊔ (fv 0 0)='(fv 0 2))
#eval FormulaToString ((fv 0 0)='(fv 0 1) ⊓ (fv 0 0)='(fv 0 2))

最後の3つは不満だと思う。BoundedFormulaの定義に則っているだけなので、ネイティブに表現されるわけではない存在量化子やandとorは解釈してくれない。

これをなんとかする。まず⊔や⊓というどこで定義されているかすらわからない記号をやめて、自前で作る。

@[match_pattern]
def FormulaOr {α : Type} {n : ℕ} (ϕ1 ϕ2 : LSet.BoundedFormula α n) : LSet.BoundedFormula α n := (∼ϕ1)⟹ϕ2
infix : 70 "∨" => FormulaOr

@[match_pattern]
def FormulaAnd {α : Type} {n : ℕ} (ϕ1 ϕ2 : LSet.BoundedFormula α n) : LSet.BoundedFormula α n :=  ∼(ϕ1⟹∼ϕ2)
infix : 80 "∧" => FormulaAnd

@[match_pattern]はこれらをパターンマッチで使えるようにするもの。

そして、→を単純に記述するよりもこれらを優先的にマッチングさせる。

def FormulaToString' {n : ℕ} (ϕ : LSet.BoundedFormula ℕ n) : String :=
match ϕ with
| BoundedFormula.falsum => "⊥"
| BoundedFormula.ex ϕ1 => s!"∃'bv{n}({FormulaToString' ϕ1})"
| BoundedFormula.all ϕ1 => s!"∀'bv{n}({FormulaToString' ϕ1})"
| FormulaOr ϕ1 ϕ2 => s!"{FormulaToString' ϕ1} ∨ {FormulaToString' ϕ2}"
| FormulaAnd ϕ1 ϕ2 => s!"{FormulaToString' ϕ1} ∧ {FormulaToString' ϕ2}"
| ∼ϕ1 => s!"∼{FormulaToString' ϕ1}"
| BoundedFormula.equal t1 t2 => s!"{TermToString t1} = {TermToString t2}"
| BoundedFormula.rel is_elt_of₂ ts  =>
    s!"{TermTupleToString ts 0} ∈ {TermTupleToString ts 1}"
| BoundedFormula.imp ϕ1 ϕ2 => s!"{FormulaToString' ϕ1} ⟹ {FormulaToString' ϕ2}"

いろいろ表示させてみる。

#eval FormulaToString' ϕbot
#eval FormulaToString' (∼ϕbot)
#eval FormulaToString' ((fv 0 0)='(fv 0 1))
#eval FormulaToString' ((fv 0 0)∈(fv 0 1))
#eval FormulaToString' (ϕbot ⟹ ((fv 0 0)∈(fv 0 1)))
#eval FormulaToString' (ϕbot ⟹ (fv 0 0)∈(fv 0 1))
#eval FormulaToString' (∀'((bv 1 0)∈(fv 1 0)))
#eval FormulaToString' ((fv 0 0)='(fv 0 1) ⊔ (fv 0 0)='(fv 0 2))
#eval FormulaToString' ((fv 0 0)='(fv 0 1) ⊓ (fv 0 0)='(fv 0 2))
#eval FormulaToString' (∃' ∀'((bv 2 1)∈(bv 2 0)))
#eval FormulaToString' (∀' ∃'((bv 2 1)∈(bv 2 0)))

とりあえず私は大満足である。前回定義したis_emptysetで作られた論理式も全展開して表示できる。

#eval FormulaToString' (∀'(is_emptyset (bv 1 0) ⟹ (bv 1 0)='(fv 1 0)))
-- Output: "∀'bv0(∀'bv1(∼bv1 ∈ bv0) ⟹ bv0 = fv0)"

次回予告

集合論のモデルを考えるのに、これまで例にしてきたVのようなものをinstanceで定義するのは現実的でない。そもそも無矛盾であるかさえ不明なものを扱うわけで。というわけで、型クラスを使って何らかの公理を満たす型というのを表現する。正直、型クラスはよく理解できていないのでここからちょっとペースが落ちるかもしれない。がんばる。