/-
# attribute

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

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

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.md)の外に出ると削除された属性が戻ります。-/
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 `[irreducible]` 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`](./Section.md) 内でのみ付与した属性を有効にするには、[`local`](#{root}/Modifier/Local.md) で属性名を修飾します。
-/
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
