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 の２つの定理が生成されます．

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つの `Point` の点が等しいことは，各フィールドの値が等しいことと同値
#check (Point.ext_iff : (x y : Point α) → x = y ↔ x.x = y.x ∧ x.y = y.y)