ac_rfl

ac_rfl は、結合的(associative)かつ可換(commutative)な演算に対して、結合性と可換性だけから示せる等式を示すタクティクです。

/-- 3次元格子点がなす空間 -/
@[ext]
structure Point : Type where
  x : Int
  y : Int
  z : Int


/-- `Point` 上の足し算 -/
def add (a b : Point) : Point :=
  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

/-- `Point` 上の足し算を `+` で表せるようにする -/
instance : Add Point where
  add := add

@[simp]
protected theorem x_add (a b : Point) : (a + b).x = a.x + b.x := rfl

@[simp]
protected theorem y_add (a b : Point) : (a + b).y = a.y + b.y := rfl

@[simp]
protected theorem z_add (a b : Point) : (a + b).z = a.z + b.z := rfl

/-- `Point` 上の足し算は可換 -/
protected theorem add_comm (a b : Point) : a + b = b + a := by
  ext
  all_goals
    simp
    apply Int.add_comm

/-- `Point` 上の足し算は結合的 -/
protected theorem add_assoc (a b c : Point) : a + b + c = a + (b + c) := by
  ext
  all_goals
    simp
    apply Int.add_assoc

-- `ac_rfl` から使えるように、`Std.Commutative` のインスタンスにする
instance : Std.Commutative (α := Point) (· + ·) where
  comm := Point.add_comm

-- `ac_rfl` から使えるように、`Std.Associative` のインスタンスにする
instance : Std.Associative (α := Point) (· + ·) where
  assoc := Point.add_assoc

-- 可換性と結合性から示せることなら示せる
example (a b c: Point) : (a + b) + c + (a + b) = a + a + b + b + c := by
  ac_rfl

ac_rfl は、上記の構造体 Point の例のように、自分で定義した演算が可換で結合的であることを後から簡単に利用できるようにしておきたいときに役立ちます。ここで @[simp] タグを付けるのは、可換性や結合法則は項の単純化ではないため上手くいかないということに注意してください。

よくあるエラー

ac_rfl は、可換性と結合性の両方がインスタンスとして登録されていないと使えないことがあります。以下は、可換性だけが登録されているときに、可換性だけで示せそうな命題が示せないという例です。

@[ext]
structure Color : Type where
  r : Nat
  g : Nat
  b : Nat

section

def add (a b : Color) : Color :=
  ⟨a.r + b.r, a.g + b.g, a.b + b.b⟩

instance : Add Color where
  add := add

/-- `add` は可換 -/
protected theorem add_comm (a b : Color) : a + b = b + a := by
  ext <;> apply Nat.add_comm

/-- `add_comm` を `Std.Commutative` に登録する。
local に宣言したので、このセクション内限定 -/
local instance : Std.Commutative (α := Color) (· + ·) where
  comm := Color.add_comm

example (a b : Color) : a + b = b + a := by
  -- ac_rfl がエラーになってしまう
  fail_if_success ac_rfl

  ext <;> apply Nat.add_comm

end

結合法則と ac_rfl

上記のように、ac_rfl は可換性だけで示せることを可換性だけで示せないのですが、往々にして結合法則だけで示せることは結合法則だけで示すことができます。

section

/-- `Color` の足し算は結合的 -/
protected theorem add_assoc (a b c : Color) : a + b + c = a + (b + c) := by
  ext <;> apply Nat.add_assoc

-- エラーになっているので、
-- Commutative のインスタンスはないことが確認できる
/--
error: failed to synthesize
  Std.Commutative fun x1 x2 => x1 + x2
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
  #synth Std.Commutative (α := Color) (· + ·)

/-- `add_comm` を `Std.Associative` に登録する。
local にしたのでセクション内でのみ有効 -/
local instance : Std.Associative (α := Color) (· + ·) where
  assoc := Color.add_assoc

-- 結合法則だけで示せることは示すことができる
example {a b c : Color} : (a + b) + (c + (b + a)) = a + b + c + b + a := by
  ac_rfl

end