simp

[simp] 属性を定理に付与すると、simp タクティクによって単純化ルールとして使用されるようになります。

/-- 標準の`Nat`を真似て自作した型 -/
inductive MyNat where
  | zero
  | succ (n : MyNat)

/-- `MyNat`上の足し算 -/
def MyNat.add (m n : MyNat) : MyNat :=
  match n with
  | .zero => m
  | .succ n => succ (add m n)

instance : Add MyNat where
  add := MyNat.add

instance : Zero MyNat where
  zero := MyNat.zero

theorem MyNat.add_zero (n : MyNat) : n + 0 = n := by
  rfl

-- 最初は`simp`で示すことができない
example (n : MyNat) : (n + 0) + 0 = n := by
  fail_if_success simp

  rw [MyNat.add_zero n]
  rw [MyNat.add_zero n]

-- `[simp]`属性を付与する
attribute [simp] MyNat.add_zero

-- `simp`で示せるようになった！
example (n : MyNat) : (n + 0) + 0 = n := by
  simp

関数に付与した場合

[simp] 属性は定理だけでなく関数定義などにも付与することができます。関数定義に付与した場合、その関数について定義からただちに従う関数等式が自動的に見出だされて simp 補題として登録されます。

/-- フィボナッチ数列 -/
def Nat.fib (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 => Nat.fib (n + 1) + Nat.fib n

-- `rfl` ですぐ示せる関数等式があるが、`simp` では示せない
example : Nat.fib 0 = 0 := by
  fail_if_success simp
  rfl

example : Nat.fib 1 = 1 := by
  fail_if_success simp
  rfl

example (n : Nat) : Nat.fib (n + 2) = Nat.fib (n + 1) + Nat.fib n := by
  fail_if_success simp
  rfl

-- `Nat.fib` に対する `simp` 補題を生成する
attribute [simp] Nat.fib

-- `simp` で示せるようになる!
example : Nat.fib 0 = 0 := by
  simp

example : Nat.fib 1 = 1 := by
  simp

example (n : Nat) : Nat.fib (n + 2) = Nat.fib (n + 1) + Nat.fib n := by
  simp

simp 補題の優先順位

simp 補題による単純化は、おおむね「内側から外側へ」という順序で行われます。 これはオプションでsimpのトレース情報を出力させてみると確認できます。

/-- フィボナッチ数列 -/
def Nat.fib (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 => Nat.fib (n + 1) + Nat.fib n

@[simp]
theorem Nat.fib_zero : Nat.fib 0 = 0 := by
  rfl

-- `simp`の行った書き換えを追跡する
set_option trace.Meta.Tactic.simp.rewrite true in

-- 内側から外側へという順序で単純化を行っていることがわかる。
/-
trace: [Meta.Tactic.simp.rewrite] Nat.fib_zero:1000:
      Nat.fib 0
    ==>
      0
[Meta.Tactic.simp.rewrite] Nat.add_zero:1000:
      0 + 0
    ==>
      0
[Meta.Tactic.simp.rewrite] Nat.mul_zero:1000:
      37 * 0
    ==>
      0
[Meta.Tactic.simp.rewrite] eq_self:1000:
      0 = 0
    ==>
      True
-/
example : 37 * (Nat.fib 0 + 0) = 0 := by
  simp

[simp←]

simp 補題は通常「左辺を右辺に」単純化するために使用されますが、逆方向に使用したい場合は [simp←] とします。

/-- モノイド -/
class Monoid (α : Type) extends Mul α, One α where
  mul_one : ∀ a : α, a * 1 = a
  one_mul : ∀ a : α, 1 * a = a
  mul_assoc : ∀ a b c : α, (a * b) * c = a * (b * c)

variable {α : Type} [Monoid α]

@[simp←]
theorem mul_one_rev (a : α) : a = 1 * a := by
  rw [Monoid.one_mul a]

-- `simp?` で確認してみると、該当する補題に `←` が付与されている
/-
info: Try this:
  [apply] simp only [← mul_one_rev]
-/
example (a : α) : 1 * (1 * a) = a := by
  simp?

[simp↓]

simp はデフォルトでは部分式をすべて単純化した後に全体の式に単純化を適用しています。simp タクティクに、部分式が単純化されるよりも先に前処理として単純化したいルールがある場合は、[simp↓] を使用します。

/-- 整数のような何か -/
opaque MyInt : Type

variable [LE MyInt] [Add MyInt] [Zero MyInt]

@[simp]
axiom MyInt.add_zero (a : MyInt) : a + 0 = a

@[simp]
axiom MyInt.simp_le_add (a b c : MyInt) : a + b ≤ a + c ↔ b ≤ c


example (a b : MyInt) (h : a + 0 ≤ a + b) : 0 ≤ b := by
  simp at h

  -- `simp` により `add_zero` が先に適用されてしまう
  -- 本当は `simp_le_add` が先に適用されて欲しい…
  guard_hyp h : a ≤ a + b

  sorry

-- `[simp↓]` 属性を付与する
attribute [simp↓] MyInt.simp_le_add

-- `simp`の行った書き換えを追跡する
set_option trace.Meta.Tactic.simp.rewrite true

/-
trace: [Meta.Tactic.simp.rewrite] ↓ MyInt.simp_le_add:1000:
      a + 0 ≤ a + b
    ==>
      0 ≤ b
-/
example (a b : MyInt) (h : a + 0 ≤ a + b) : 0 ≤ b := by
  -- ちゃんと `simp_le_add` が先に適用されるようになった！
  simp at h
  assumption

優先度指定

simp 補題の中でも早い段階で適用してほしい補題や、遅い段階で適用してほしい補題があるとき、優先度を指定することができます。

simp high

[simp high] とすると優先度が高まり、他の simp 補題よりも先に適用されるようになります。

/-- 謎の自然数 -/
opaque foo : Nat

/-- 謎の自然数 -/
opaque bar : Nat

/-- 謎の自然数 -/
opaque baz : Nat

@[simp]
axiom foo_eq_bar : foo = bar

@[simp]
axiom foo_eq_baz : foo = baz


example : foo = baz := by
  -- 先に宣言された方の `foo_eq_bar` が適用されてしまって、
  -- 証明することができない
  simp

  guard_target =ₛ bar = baz

  sorry

attribute [simp high] foo_eq_baz

example : foo = baz := by
  -- `foo_eq_baz` の方が優先度が高いため、こちらが先に適用される
  simp

simp low

[simp low] とすると優先度が低くなり、他の simp 補題よりも後に適用されるようになります。

/-- 謎の自然数 -/
opaque foo : Nat

/-- 謎の自然数 -/
opaque bar : Nat

/-- 謎の自然数 -/
opaque baz : Nat

@[simp]
axiom foo_eq_bar : foo = bar

@[simp]
axiom foo_eq_baz : foo = baz


example : foo = baz := by
  -- 先に宣言された方の `foo_eq_bar` が適用されてしまって、
  -- 証明することができない
  simp

  guard_target =ₛ bar = baz

  sorry

-- `foo_eq_bar` の優先度を下げる
attribute [simp low] foo_eq_bar

example : foo = baz := by
  -- `foo_eq_baz` の方が優先度が高いため、こちらが先に適用される
  simp