Closed Seasawher closed 1 week ago
dsimp は simp の派生というよりも,unfold のより高度なバージョンかもしれない
simp 属性が付けられた補題は dsimp の挙動に影響するのだろうか?
もし unfold も紹介することがあれば,unfold との関連にも着目すべきかも
unfold は既に紹介していたので,間違いなく dsimp との差異は問題になる
dsimp と unfold の違いが現れるケース(のMathlibに依存しない例)
-- α の部分集合を表す型
def Set (α : Type) := α → Prop
-- 部分集合の共通部分を取る操作
def Set.inter {α : Type} (s t : Set α) : Set α := fun x => s x ∧ t x
-- ∩ という記法を使えるようにする
instance (α : Type) : Inter (Set α) where
inter := Set.inter
variable (s t : Set α)
example : s ∩ u = u ∩ s := by
dsimp [(· ∩ ·)]
-- 記法の部分だけを展開できる
show s.inter u = u.inter s
sorry
example : s ∩ u = u ∩ s := by
dsimp [Inter.inter]
show s.inter u = u.inter s
sorry
example : s ∩ u = u ∩ s := by
unfold Inter.inter
-- 展開結果の中にインスタンスが入り込んでしまう
show (instInterSet α).1 s u = (instInterSet α).1 u s
sorry
dsimp へのリンクを貼りたいことがあるのと,定義を展開するだけのタクティクには独特な需要があるので