attribute

attribute は、属性(attribute)を付与するためのコマンドです。

次の例では、命題に [simp] 属性を付与しています。これは simp タクティクで利用される命題を増やすことを意味します。

theorem foo {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  constructor <;> intro h
  all_goals
    refine ⟨?_, by simp_all⟩
    simp_all

example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  -- `simp` では示せない
  fail_if_success solve
  | simp

  sorry

-- `attribute` で属性を付与
attribute [simp] foo

example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  -- `simp` で示せるようになった
  simp

属性の削除

与えた属性を削除することができることもあります。削除するには - を属性の頭に付けます。属性の削除はデバッグを意図した機能で、常にローカルにはたらき、そのセクションの外に出ると削除された属性が戻ります。

section
  -- `[simp]` 属性を削除
  attribute [-simp] foo

  -- 再び `simp` では示せなくなった
  example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
    fail_if_success solve
    | simp

    sorry
end

-- `simp` で示せるようになった
example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by simp

属性によっては、削除することができないこともあります。

@[irreducible] def greet := "Hello"

/-- error: attribute cannot be erased -/
#guard_msgs in
  attribute [-irreducible] greet

タグ

attribute コマンドを使用すると定義の後から属性を付与することができますが、定義した直後に属性を付与する場合はタグと呼ばれる @[..] という書き方が使えます。

@[simp]
theorem bar {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  constructor <;> intro h
  all_goals
    refine ⟨?_, by simp_all⟩
    simp_all

example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  simp

有効範囲を制限する

特定の section 内でのみ付与した属性を有効にするには、local で属性名を修飾します。

example (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by
  -- simp だけでは証明できない
  fail_if_success solve
  | simp

  sorry

section
  -- 補題
  theorem or_and_neg (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by
    constructor <;> intro h
    · refine ⟨?_, by simp_all⟩
      have : ¬ Q := h.right
      simp_all
    · refine ⟨?_, by simp_all⟩
      simp_all

  -- local に simp 補題を登録
  attribute [local simp] or_and_neg

  -- simp で証明ができるようになった！
  example (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by simp
end

example (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by
  -- section を抜けると simp 補題が利用できなくなった
  fail_if_success solve
  | simp

  sorry