ext
ext
は、外延性(extensionality)を使うタクティクです。外延性とは、「同じものから作られているものは同じである」という主張のことです。たとえば以下のようなことを指します。
- 集合
A, B ⊂ α
についてA = B
はx ∈ A ↔ x ∈ B
と同じ。 - 2つの写像
f g : A → B
があるときf = g
は∀ a ∈ A, f a = g a
と同じ。
@[ext]
で登録されたルールを使用するため、集合の等式 A = B
を示すときは Mathlib.Data.SetLike.Basic
も必要です。
import Aesop -- `aesop` タクティクを使うために必要
import Mathlib.Data.SetLike.Basic -- `ext` タクティクで集合の等号を展開するために必要
variable {α : Type}
-- `s` と `t` は `α` の部分集合
variable (s t : Set α)
example : s ∩ t = t ∩ s := by
-- `x ∈ α` を取る。
ext x
-- ` x ∈ s ∩ t ↔ x ∈ t ∩ s` を証明すればよい
show x ∈ s ∩ t ↔ x ∈ t ∩ s
aesop
[ext] 属性
[ext]
属性を命題に与えると、上記のようにその命題は ext
タクティクで利用できるようになります。さらに、[ext]
属性は構造体に対しても与えることができます。このとき、その構造体に対して自動的に .ext
と .ext_iff
の2つの定理が生成されます。
variable {α : Type}
structure Point (α : Type) where
x : α
y : α
-- 最初は存在しない
#check_failure Point.ext
#check_failure Point.ext_iff
-- `Point` に `[ext]` 属性を与える
attribute [ext] Point
-- 自動生成された定理
-- 各フィールドの値が等しければ、2つの `Point` は等しいという主張
#check (Point.ext : ∀{x y : Point α}, x.x = y.x → x.y = y.y → x = y)
-- 自動生成された定理その2
-- 2つの `Point` の点が等しいことは、各フィールドの値が等しいことと同値
#check (Point.ext_iff : ∀{x y : Point α}, x = y ↔ x.x = y.x ∧ x.y = y.y)