attribute
attribute
は、属性(attribute)を付与するためのコマンドです。
次の例では、命題に [simp]
属性を付与しています。これは simp
タクティクで利用される命題を増やすことを意味します。
theorem foo {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
constructor <;> intro h
· obtain ⟨hPQ, hP⟩ := h
constructor <;> repeat apply_assumption
· obtain ⟨hP, hQ⟩ := h
constructor <;> intros
all_goals assumption
-- `simp` では示せない
example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
simp
show P → P ∨ Q
intro (h : P)
left
assumption
-- `attribute` で属性を付与
attribute [simp] foo
-- `simp` で示せるようになった
example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
simp
属性の削除
与えた属性を削除することができることもあります。削除するには -
を属性の頭に付けます。
section
-- `[simp]` 属性を削除
attribute [-simp] foo
-- 再び示せなくなった
example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
simp
show P → P ∨ Q
intro (h : P)
left
assumption
end
属性の削除はデバッグを意図した機能で、常にローカルにはたらき、その section
の外に出ると削除された属性が戻ります。
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
· obtain ⟨hPQ, hP⟩ := h
constructor <;> repeat apply_assumption
· obtain ⟨hP, hQ⟩ := h
constructor <;> intros
all_goals assumption
example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
simp
有効範囲を制限する
特定の section
でのみ付与した属性を有効にするには、local
で属性名を修飾します。
example (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by
-- simp だけでは証明が終わらない
try simp
show ¬Q → Q → P
intro hnQ hQ
contradiction
section
-- 補題
theorem or_and_neg (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by
constructor <;> intro h
· obtain ⟨hPQ, hnQ⟩ := h
rcases hPQ with hP | hQ
· exact ⟨hP, hnQ⟩
· contradiction
· obtain ⟨hP, hnQ⟩ := h
exact ⟨by left; assumption, hnQ⟩
-- local に simp 補題を登録
attribute [local simp] or_and_neg
-- simp で証明ができる
example (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by simp
end
variable (P Q : Prop)
-- section を抜けると simp 補題が利用できない
example (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by
simp
-- 証明すべきことが残ってしまった
show ¬Q → Q → P
intro _ _
contradiction