📝
ProofDataで中間的な定義や証明を整理する

2024/12/05に公開
定理証明支援系
English version is available.
この記事では、型クラス (type class) を用いることで中間的な定義やそれに対する証明を効率的に再利用する手法を紹介します。この手法自体は新しいものではないかもしれませんが、パターン共有することで、アプリケーションの検証がより実用的になることを願っています。

 動機現在、私はlean-regexという正規表現エンジンの開発および検証に取り組んでいます。このエンジンはLean 4で実装されており、正規表現を非決定性有限オートマトン(NFA)にコンパイルすることで文字列検索を行います。現時点では、検索関数が入力文字列にマッチがある場合にのみ.someを返すことを証明できています。しかし、検索関数がマッチ位置を正しく報告していることの証明はできていません。なぜなら、マッチ位置の報告はキャプチャグループ昨日に依存しており、キャプチャグループの形式化はまだできていないからです。
したがって、次のステップはキャプチャグループの意味論を形式化し、実装がその意味論に対して正しいことを証明することです。一方で、現状の証明の設計ではこういった複雑な性質に対応しきれないのではないかという懸念から、キャプチャグループの形式化に取り組むことをためらっていました。
本題に入る前に、まずlean-regexの実装について簡単に説明します。このライブラリは正規表現をNFAにコンパイルします。NFAを利用することで、正規表現を用いた検索を線型時間で実現できます。コンパイルはpushRegexという関数を通じて段階的に行われます。具体的には、pushRegex nfa next eは与えられたNFA nfaを拡張した新しいNFAを生成します。生成されたNFAにおいて、初期状態からnext状態への遷移と入力文字列の正規表現eへのマッチが同値となります。
例えば、e₁ | e₂ (和) の形の正規表現をコンパイルする場合を考えます。まず、doneと呼ばれる単一状態のNFAを用意します。このNFAの唯一の状態が受理状態を表しており、この状態に到達することが正規表現のマッチに対応します。
e₁ | e₂をコンパイルするには、pushRegex done 0 (e₁ | e₂)を呼び出します。この処理は再帰的に展開されます:
最初に、doneにe₁の状態を追加したNFAを得ます: nfa₁ := pushRegex done 0 e₁
次に、e₂の状態を追加して新しいNFAを作ります: nfa₂ := pushRegex nfa₁ 0 e₂
最後に、ε遷移(空入力での遷移)によってe₁とe₂の開始状態にジャンプするsplitノードを追加し、最終的な NFA を構築します: nfa' := pushNode nfa₂ (.split nfa₁.start nfa₂.start)
このように、e₁ | e₂のNFAを構築するには、nfa₁やnfa₂などの中間的なステップがいくつか必要になります。これらの中間NFAの遷移の動作や、コンパイル済みNFAとの関係性を分析・証明することが、正しさの証明において重要です。
しかし、nfa₁やnfa₂のような中間データはpushRegex内でローカル変数として定義されているため、関数外からはアクセスできません。このため、様々な証明でこれらを再利用することができず、同じ性質を繰り返し証明しなければならない状況が頻発していました。これは非常に非効率で手間のかかる作業です。

 ProofData パターン実際のところ、これらの中間データ構造を型クラスを用いてトップレベルの定義に引き上げることが可能です。このアプローチのもと、基本的な定義や性質を再利用可能なフレームワーク内にまとめることで、証明の冗長性を排除することができます。このアイデアは、Floris のZulipメッセージで初めて見かけたので、そこから「ProofData」という名前を借りました。
今回のケースでは、pushRegex関数への入力をまとめたProofData型クラスを作成します。この型クラスに初期NFA、ターゲット状態、正規表現といった入力をまとめることで、これらを証明内でより便利に参照および再利用できるようになります。例えば、ProofData インスタンスがスコープ内にある場合、コンパイル結果nfa'を次のように定義できます。
class ProofData where
  nfa : NFA
  next : Nat
  e : Expr
  
def ProofData.nfa' [ProofData] : NFA := pushRegex nfa next e
ただし、ProofDataクラスは、正規表現のそれぞれのバリアント固有の情報を欠いています。この問題を解決するため、私は正規表現ごとにサブクラスを作成しました。これらのサブクラスはProofDataを拡張し、追加のデータと、元の式に追加データを結び付けるプロパティexpr_eqを含んでいます。例えば、正規表現の和を扱うAlternateクラスは次のようになります。
class Alternate extends ProofData where
  e₁ : Expr
  e₂ : Expr
  expr_eq : e = .alternate e₁ e₂
Alternateインスタンスを使えば、nfa₁やnfa₂といった中間データをトップレベルの定義として表現できます。この方法は、中間データの定義をきれいに整理できるだけでなく、性質を証明してまとめることを可能にします。さらに、中間データに対して証明された性質は正当性の検証全体で再利用できます。以下はその例です：
namespace Alternate

variable [Alternate]

-- 中間データの定義
def nfa1 : NFA := nfa.pushRegex next e₁
def nfa2 : NFA := nfa1.pushRegex next e₂

-- 中間データの性質
theorem size_lt₂ : nfa₂.nodes.size < nfa'.nodes.size := ...
theorem size_lt₁ : nfa₁.nodes.size < nfa'.nodes.size := ...
theorem get_start : nfa'[nfa'.start] = .split nfa₁.start nfa₂.start := ...

end
これらの性質を正当性の検証で使用する際には、型クラスのインスタンスをローカル変数として導入します。すると、LeanがAlternate名前空間内の名前を解決する際に自動的にこのインスタンスを利用します。
-- eq : nfa.pushRegex next e = result
induction e with
| ...
| alternate e₁ e₂ ih₁ ih₂ =>
  -- Alternate インスタンスを導入するユーティリティ関数
  let pd := ProofData.Alternate.intro eq

  -- この時点で、バリアント固有の定義や性質が利用可能になる
  -- 例：
  -- - `pd.nfa1`は`e₁`をコンパイルされたNFAを表す
  -- - `pd.get_start`はsplitノードに関する性質を提供する

 結果このProofData手法への移行は、このプルリクエストで確認できます。ボイラープレートの追加により全体の行数は増加しましたが、中間データに関する性質の再利用により、個々の証明は大幅に短縮されました。特に複雑な証明において、行数が30～40%減少したことを確認しました。
さらに、ProofDataは中間データとそれに関連する性質を整理するための体系的な構造を提供してくれます。この変更により、新しい機能を追加する際にもライブラリを拡張しやすくなったと思います。このリファクタリングはやる価値があったと思っており、今後もこの手法を継続して使用する予定です。

 課題ProofDataは証明を構造化するための有用なパターンですが、いくつかの課題も見つかりました。
1つ目の課題は、帰納法による証明とProofDataがバリアントごとに定義されることのミスマッチです。帰納法では、仮定として一般的な正規表現eが与えられますが、ProofDataは正規表現の各バリアントに対して定義されています。そのため、結果をProofDataのバリアントごとの名前空間に移動するには、各バリアントごとに定理を再記述する必要がありました (例)。
もう1つの問題は、帰納的証明の仮定にProofDataを含める場合に発生します。例えば、次の定理は、pushRegexが元のNFAの内容を変更しないことを示しています (なぜなら、pushRegexは新しい状態を末尾に追加するからです)：
theorem ProofData.pushRegex_get_lt (pd : ProofData) (i : Nat) (h : i < pd.nfa.nodes.size) :
  pd.nfa'[i] = pd.nfa[i]
このスタイルの定義は、結果にアクセスする便利な方法 (pd.pushRegex_get_lt) を提供しますが、証明時に次の2つの問題を引き起こしました:
帰納法の際にinduction pd.e withと書くと、pd.eと各分岐で導入される変数間の等式が失われます。この問題はgeneralize expr_eq : pd.e = e'を使用することで回避できますが、依然として手間がかかります。
より重要なのは、pd : ProofDataがバリアント固有のデータを持たない点です。そのため、各分岐で再度サブクラス (例: Alternate) を導入する必要があります。この結果、異なるProofDataから生成された2つのnfaが存在することになります！ これらは等値であっても、非常に混乱を引き起こします。
これらの問題のため、私は次のように、nfa、next、eを自由変数として定義に含める方法に戻りました。
theorem pushRegex_get_lt {nfa next e result} (eq : pushRegex nfa next e = result) (i : Nat) (h : i < nfa.nodes.size) :
  result.val[i] = nfa[i] := by
  induction e with
  | ...
  | alternate e₁ e₂ ih₁ ih₂ =>
    let pd := Alternate.intro eq
    -- 証明が続く
このアプローチはより直感的ですが、冗長でもあります。各分岐で2つのnfa(引数のnfaとpd.nfa)の定義が存在するようになり、これらが定義的に等値(definitionally equal)であっても、simpやrw、omegaといったタクティックがが等値性を認識できないことが頻発します。このため、等式を解決するために頻繁にrflを使用する必要がありました。
これらの制限を解決する一つの方法として、pdに直接作用し、各バリアントに固有なProofDataに置き換えるカスタム帰納法原理を作成することが考えられます。このアプローチは、証明作業を簡略化し、冗長性を減らす可能性があります。ただし、この方法の実現可能性についてはまだ確認していません。また、少なくとも等値性の問題は簡約性 (reducibility) を調整することで解決できる可能性があります。Lean の専門家からのフィードバックを歓迎します！
動機

ProofData パターン

結果

課題

Discussion
