Lean4における加法の単調性を証明

今回は、足し算が順序関係を保つこと(単調性)を証明していきます。あわせて、同じ形の証明を何度も書かずに済むように、compatible というカスタムタクティクを作成します。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

加法の単調性

まず、両辺の左に同じ値を足しても順序関係が保たれることを証明します。

variable {a b m n : MyNat}

theorem MyNat.add_le_add_left (h : n ≤ m) (l : MyNat) : l + n ≤ l + m := by
  rw [MyNat.le_iff_add] at *
  obtain ⟨k, hk⟩ := h
  -- h : ∃ k, n + k = m
  -- l : MyNat
  -- ⊢ ∃ k, n + k = m
  exists k
  rw [← hk] -- hk : n + k = m ⊢ l + n + k = l + (n + k)
  ac_rfl

theorem MyNat.add_le_add_right (h : m ≤ n) (l : MyNat) : m + l ≤ n + l := calc
  _ = l + m := by ac_rfl
  _ ≤ l + n := by apply MyNat.add_le_add_left h l
  _ = n + l := by ac_rfl

MyNat.add_le_add_left の証明では、MyNat.le_iff_add によって \( n \le m \) を \( \exists k,\ n + k = m \) の形に書き換え、得られた \( k \) をそのまま使って \( l + n \le l + m \) を示しています。最後は ac_rfl で足し算の順序を整えれば証明が完了します。

MyNat.add_le_add_right の方は、可換性を使って左に足す形に帰着させることで、既に証明した MyNat.add_le_add_left を再利用できます。

より一般に、二つの和についても順序関係が保たれることを証明できます。

theorem MyNat.add_le_add (h1 : m ≤ n) (h2 : a ≤ b) : m + a ≤ n + b := calc
  _ ≤ m + b := by exact add_le_add_left h2 m
  _ ≤ n + b := by exact add_le_add_right h1 b

定理を再利用可能にする

これらの定理を素朴に使うと、次のように apply の後に仮定を渡す書き方になります。

example (h : n ≤ m) (l : MyNat) : l + n ≤ l + m := by
  apply MyNat.add_le_add_left h

仮定を一つずつ渡す代わりに、<;> assumption でまとめて解決させることもできます。

example (h : n ≤ m) (l : MyNat) : l + n ≤ l + m := by
  apply MyNat.add_le_add_left <;> assumption

この書き方を三つの定理すべてに使えるように、compatible というタクティクを作成します。

syntax "compatible" : tactic

section

  local macro_rules
    | `(tactic| compatible) =>
      `(tactic| apply MyNat.add_le_add_left <;> assumption)

  local macro_rules
    | `(tactic| compatible) =>
      `(tactic| apply MyNat.add_le_add_right <;> assumption)

  local macro_rules
    | `(tactic| compatible) =>
      `(tactic| apply MyNat.add_le_add <;> assumption)

  example (h : n ≤ m) (l : MyNat) : l + n ≤ l + m := by
    compatible

  example (hle : n ≤ m) (l : MyNat) : n + l ≤ m + l := by
    compatible

  example (h1 : m ≤ n) (h2 : a ≤ b) : m + a ≤ n + b := by
    compatible

end

ラベル属性で拡張可能にする

macro_rules による実装では、新しい定理を追加するたびにマクロ自体を書き換える必要があります。そこで、@[compatible] という属性を付けるだけで登録できるように変更します。

まず、属性そのものを新しいファイルで宣言します。register_label_attr はファイルを跨がないと適用できないため、別ファイルに分けています。

import Lean

register_label_attr compatible

次に、実際のタクティクを elab で定義します。elab は macro と異なり手続き的なメタプログラミングに向いたキーワードです。[compatible] が付いた定理を順番に取得し、apply $declStx <;> assumption が成功するまで試し続けます。

open Lean Elab Tactic in

elab "compatible" : tactic => do
  let taggedDecls ← labelled `compatible
  if taggedDecls.isEmpty then
    throwError "theorem of [compatible] has not been assigned"
  for decl in taggedDecls do
    let declStx := mkIdent decl
    try
      evalTactic <| ← `(tactic| apply $declStx <;> assumption)

      return ()
    catch _ =>
      pure ()
  throwError "Unable to close the goal."

あとは対象の定理に属性を付けるだけで、compatible タクティクから利用できるようになります。

attribute [compatible] MyNat.add_le_add_left MyNat.add_le_add_right MyNat.add_le_add

example (h : n ≤ m) (l : MyNat) : l + n ≤ l + m := by
  compatible

example (hle : n ≤ m) (l : MyNat) : n + l ≤ m + l := by
  compatible

example (h1 : m ≤ n) (h2 : a ≤ b) : m + a ≤ n + b := by
  compatible

狭義順序でも成り立つことを示す

足し算は狭義順序 \( \lt \) についても両立性を持ちます。@[compatible] を付けておくことで、後の証明でも compatible を使い回せます。

@[compatible]
theorem MyNat.add_lt_add_left {m n : MyNat} (h : m < n) (k : MyNat) : k + m < k + n := by
  notation_simp at *  -- h : m + 1 ≤ n ⊢ k + m + 1 ≤ k + n
  have : k + m + 1 ≤ k + n := calc
    _ = k + (m + 1) := by ac_rfl
    _ ≤ k + n := by compatible

  assumption

@[compatible]
theorem MyNat.add_lt_add_right {m n : MyNat} (h : m < n) (k : MyNat)
  : m + k < n + k := calc
  _ = k + m := by ac_rfl
  _ < k + n := by compatible
  _ = n + k := by ac_rfl

両辺から同じ値を引いても順序は保たれる

最後に、逆方向、つまり両辺から同じ値を引いても順序関係が保たれることを証明します。

section
variable (m n k : MyNat)

theorem MyNat.le_of_add_le_add_left : k + m ≤ k + n → m ≤ n := by
  intro h
  -- h : k + m ≤ k + n ⊢ m ≤ n
  rw [MyNat.le_iff_add] at *
  -- h : ∃ k_1, k + m + k_1 = k + n ⊢ ∃ k, m + k = n
  obtain ⟨d, hd⟩ := h
  exists d -- hd : k + m + d = k + n ⊢ MyNat
  have : m + d + k = n + k := calc
    _ = k + m + d := by ac_rfl
    _ = k + n := by rw [hd]
    _ = n + k := by ac_rfl
  simp_all

theorem MyNat.le_of_add_le_add_right : m + k ≤ n + k → m ≤ n := by
  rw [MyNat.add_comm m k, MyNat.add_comm n k]
  apply MyNat.le_of_add_le_add_left

@[simp] theorem MyNat.add_le_add_iff_left : k + m ≤ k + n ↔ m ≤ n := by
  constructor
  · apply MyNat.le_of_add_le_add_left
  · intro h
    compatible

@[simp] theorem MyNat.add_le_add_iff_right : m + k ≤ n + k ↔ m ≤ n := by
  constructor
  · apply MyNat.le_of_add_le_add_right
  · intro h
    compatible

end

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

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