📚

Lean言語で回文を定義して基本的な性質を示す

に公開
lean4
tech

回文の２つの定義の同値性

Leanで帰納的述語を扱う例として、回文(palindrome)を定義してその基本的な性質を示す例を示します。

まず、回文は帰納的述語としては次のように定義できます。

variable {α : Type}

/-- 回文を表す帰納的述語 -/
@[grind]
inductive Palindrome : List α → Prop
  /-- 空リストは回文 -/
  | nil : Palindrome []
  /-- 要素が一つだけのリストは回文 -/
  | single (a : α) : Palindrome [a]
  /-- 回文の両端に同じ要素を追加しても回文 -/
  | sandwich {a : α} {as : List α} (ih : Palindrome as) : Palindrome ([a] ++ as ++ [a])

別の考え方をすることもできて、reverse xs = xs であることをもって xs が回文であることの定義としても良いですね。
これらが同値であることを証明してみましょう。

まず「回文であるならば、reverse しても不変」という方向ですが、こちらは比較的簡単です。

variable {a : α} {as : List α}

/-- 回文であるならば、`reverse`しても変わらない -/
theorem reverse_eq_of_palindrome (h : Palindrome as) : as.reverse = as := by
  induction h with simp_all

逆方向が少し問題ですね。
やってみるとわかりますが、通常のリストに対する帰納法だと「空か、そうでないか」という場合分けをするのに対し、Palindrome は「空か、シングルトンか、先頭と末尾に要素が追加されているか」の場合分けで定義されているのでマッチしなくて困ります。

example (h : as.reverse = as) : Palindrome as := by
  induction as with
  | nil => grind
  | cons a as ih =>
    /-
    α : Type
    a : α
    as : List α
    ih : as.reverse = as → Palindrome as
    h : (a :: as).reverse = a :: as
    ⊢ Palindrome (a :: as)
    -/
    sorry

そこで、まず Palindrome と同様の分岐を使った帰納法の原理を手作りします。
Palindrome の定義に合わせて「空か、シングルトンか、先頭と末尾に要素が追加されている形か」の場合分けをします。

ここでカギになるのは、a₁ :: a₂ :: as という形のリストを、「空でないリストの末尾の要素を取得する」関数を使って、むりやり [a₁] ++ xs ++ [x] という形に分解することです。

また、palindrome_ind を再帰的に呼びだすことで、タクティクを使わずに帰納法を実行していることにも注意してください。

theorem List.palindrome_ind {motive : List α → Prop}
    (nil : motive [])
    (single : (a : α) → motive [a])
    (sandwich : (a b : α) → (as : List α) → motive as → motive ([a] ++ as ++ [b]))
    (as : List α)
    : motive as :=
  match as with
  | [] => nil
  | [a] => single a
  | a₁ :: a₂ :: as' =>
    have ih := palindrome_ind nil single sandwich (a₂ :: as').dropLast
    let xs := (a₂ :: as').dropLast
    let x := (a₂ :: as').getLast (by simp)
    have : [a₁] ++ xs ++ [x] = a₁ :: a₂ :: as' := by
      grind [List.dropLast_concat_getLast]
    this ▸ sandwich _ _ _ ih
termination_by as.length

これを使えば、reverse して不変ならば回文であることの証明が簡単になります。

/-- `reverse` しても変わらないならば回文である -/
theorem palindrome_of_eq_reverse (h : as.reverse = as) : Palindrome as := by
  induction as using List.palindrome_ind with grind

これで二つの定義が同値であることが示せました。

theorem palindrome_iff_eq_reverse : Palindrome as ↔ as.reverse = as := by
  grind only [reverse_eq_of_palindrome, palindrome_of_eq_reverse]

おまけ: 帰納法の原理の自動生成

今回の証明でいちばん難しい部分は、Palindrome の証明で使うための帰納法の原理を生成するところでした。面倒なので、自動化できるようにしましょう。

残念ながら Lean には帰納的述語から自動的に帰納法の原理を生成するような機能はありませんが、「再帰関数から自動的に帰納法の原理を生成する」機能は存在します。そこで、回文判定を行う再帰関数を定義して、それに対して自動生成された帰納法の原理を利用するという方法がとれます。

open scoped Classical in

/-- 回文判定を行う再帰関数 -/
def isPalindrome (as : List α) : Prop :=
  match as with
  | [] => true
  | [a] => true
  | a₁ :: a₂ :: as =>
    let xs := (a₂ :: as).dropLast
    let x := (a₂ :: as).getLast (by simp)

    -- 後に証明に使うときの利便性のために補題を示しておく
    have : [a₁] ++ xs ++ [x] = a₁ :: a₂ :: as := by
      grind [List.dropLast_concat_getLast]

    if a₁ = x then
      isPalindrome xs
    else
      false
termination_by as.length

example (h : as.reverse = as) : Palindrome as := by
  induction as using isPalindrome.induct with grind

参考文献

Palindrome を扱う例は、定理証明支援系のチュートリアルにはありがちな例です。
Lean の公式サイトにも例が載っています。
今回はこれを参考にしました。

Discussion