simps

補題を simp で使えるようにするのは [simp] 属性を付与することで可能ですが、[simps] 属性(または @[simps] タグ)を利用すると simp で使用するための補題を自動的に生成してくれます。

例えば、ユーザが Point という構造体を定義し、Point 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「Point の和の x 座標」は x 座標の和ですが、これはそのままでは simp で示すことができません。[simps] 属性を Point.add 関数に付与することで、simp で示せるようになります。

import Mathlib.Tactic.Simps.Basic -- [simps] 属性を使うため

@[ext]
structure Point where
  x : Int
  y : Int

/-- Point の和 -/
def Point.add (p q : Point) : Point :=
  { x := p.x + q.x, y := p.y + q.y }

/-- 和の x 座標は x 座標の和 -/
example (a b : Point) : (Point.add a b).x = a.x + b.x := by
  -- この状態だと `simp` で示せない
  fail_if_success simp

  rfl

-- `Point.add` に `[simps]` 属性を付与する
attribute [simps] Point.add

example (a b : Point) : (Point.add a b).x = a.x + b.x := by
  -- simp 補題が自動的に生成されて、simp で示せるようになった
  simp

上記の例では attribute コマンドで属性を付与していますが、タグも使用できます。

@[simps]
def Point.sub (p q : Point) : Point :=
  { x := p.x - q.x, y := p.y - q.y }

example (a b : Point) : (Point.sub a b).x = a.x - b.x := by simp

@[simps?] に換えると、生成された補題を確認することができます。

/-
trace: [simps.verbose] The projections for this structure have already been initialized by a previous invocation of `initialize_simps_projections` or `@[simps]`.
    Generated projections for Point:
    Projection x: fun x => x.x
    Projection y: fun x => x.y
[simps.verbose] adding projection Point.mul_x:
      ∀ (p q : Point), (p.mul q).x = p.x * q.x
[simps.verbose] adding projection Point.mul_y:
      ∀ (p q : Point), (p.mul q).y = p.y * q.y
-/
@[simps?] def Point.mul (p q : Point) : Point :=
  { x := p.x * q.x, y := p.y * q.y }