MyNatの順序関係を決定可能にする

今回は具体的な数値の大小関係の証明について考えます。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。MyNat.le.stepを繰り返し適用すれば個々の命題を証明することはできますが、命題ごとに証明を書くのは効率的ではありません。そこで、より汎用的な方法で大小関係を判定できるように準備します。

力技での証明は次のような形になります。

example : 0 ≤ 3 := by
  apply MyNat.le.step
  apply MyNat.le.step
  apply MyNat.le.step
  apply MyNat.le.refl

Decidable型クラス

ここで使うのがDecidable型クラスです。Decidableは命題が決定可能であること、つまり計算によって真偽を判定できることを表す型クラスで、計算結果を証明に利用するための仕組みを提供します。

DecidableEqの導入

等式をDecidableのインスタンスにしたい場面は多いため、Leanには専用のDecidableEq型クラスが用意されています。derivingキーワードを使うことで、既存の型に対して自動的にインスタンスを導出できます。

以下のようにderivingを用いた宣言でMyNatをDecidableEqとして登録できます。登録後はdecideタクティクで等式や不等式を証明できるようになり、#evalで計算結果を直接確認することもできます。

deriving instance DecidableEq for MyNat

example : 32 + 13 ≠ 46 := by
  decide

#eval 32 + 13 ≠ 46

MyNat.bleの定義

次は順序関係をDecidableとして登録するための準備として、真偽値を返す関数を定義します。MyNat.ble a bは\(a \le b\)を満たすときにtrueを返す関数です。

-- bool less than or equals to
def MyNat.ble (a b : MyNat) : Bool :=
  match a, b with
  | 0, _ => true
  | _ + 1, 0 => false
  | a + 1, b + 1 => MyNat.ble a b

#eval MyNat.ble 0 0 -- true
#eval MyNat.ble 3 4 -- true
#eval MyNat.ble 4 3 -- false

DecidableLEの登録

順序関係のDecidableクラスであるDecidableLEを登録するには、MyNat.ble m n = true ↔ m ≤ nを証明する必要があります。

instance : DecidableLE MyNat := fun n m =>
  decidable_of_iff (MyNat.ble n m = true) (MyNat.le_impl n m)

補助補題の証明

本題の証明に入る前に、必要な補題をいくつか証明しておきます。いずれも定義から直接導けるためrflで証明できます。

@[simp]
theorem MyNat.ble_zero_left (n : MyNat) : MyNat.ble 0 n = true := by
  rfl

@[simp]
theorem MyNat.ble_zero_right (n : MyNat) : MyNat.ble (n + 1) 0 = false := by
  rfl

@[simp]
theorem MyNat.ble_succ (m n : MyNat) : MyNat.ble (m + 1) (n + 1) = MyNat.ble m n := by rfl

MyNat.le_implの証明

MyNat.bleは場合分けを伴う帰納的な定義になっているため、通常のinductionタクティクではうまく場合分けできません。そこで、MyNat.ble.inductAuxという補助関数を使い、これをinduction ... usingに渡すことで、bleの定義に沿った場合分けによる帰納法を行います。

theorem MyNat.le_impl (m n : MyNat) : MyNat.ble m n = true ↔ m ≤ n := by
  induction m, n using MyNat.ble.inductAux with
  | case1 n => simp
  | case2 n =>
    suffices ¬ n + 1 ≤ 0 from by simp_all
    intro h
    simp_all
  | case3 m n ih =>
    simp [ih]

case1はMyNat.ble 0 n = true ↔ 0 ≤ nに対応するケースで、MyNat.ble_zero_leftによって左辺が常にtrueになるため、simpだけで証明できます。

case2はMyNat.ble (n + 1) 0 = true ↔ n + 1 ≤ 0に対応するケースです。左辺はMyNat.ble_zero_rightによって常にfalseになるため、同値を示すには¬ n + 1 ≤ 0を示せば十分です。これはn + 1 ≤ 0という仮定からsimp_allで矛盾を導いています。

case3はMyNat.ble (m + 1) (n + 1) = true ↔ m + 1 ≤ n + 1に対応するケースで、帰納法の仮定ihであるMyNat.ble m n = true ↔ m ≤ nを使ってsimpで証明できます。

なお、教科書ではcase2とcase3でdsimp [MyNat.ble]が使われていましたが、実際に試すとno progressというエラーになってしまうため、今回は省略しています。

これで数値の大小関係を計算で評価できるようになりました。

#eval 0 ≤ 0 -- true
#eval 1 ≤ 3 -- true
#eval 3 ≤ 1 -- false

狭義順序への拡張

広義順序で行ったのと同様の手順を、狭義順序に対しても行います。

theorem MyNat.lt_impl (m n : MyNat) : MyNat.ble (m + 1) n ↔ m < n := by
  rw [MyNat.le_impl]
  rfl

instance : DecidableLT MyNat := fun n m =>
  decidable_of_iff (MyNat.ble (n + 1) m = true) (MyNat.lt_impl n m)

example : 1 < 4 := by
  decide

コードは以下のリポジトリで公開しています。

https://github.com/ringring-creator/LearnLean