congrArg

LeanのcongrArgタクティクについて

congruence argumentの略？

関数の引数がa₁ = a₂という仮定があったなら、f a₁と f a₂の値同士はf a₁ = f a₂と見なせる

以下mathlib4のドキュメントの翻訳

code:memo

theorem congrArg {α : Sort u} {β : Sort v} {a₁ : α} {a₂ : α} (f : α → β) (h : a₁ = a₂) :

f a₁ = f a₂

関数引数の合同：任意の（非依存）関数fに対して、a₁＝a₂ならば、f a₁＝f a₂となる。これは、見た目よりも強力で、fのラムダ式を使って、＜a₁を含む何か＞＝＜a₂を含む何か＞を証明することもできる。この関数は、部分項の内部で等式を適用するために、congrやsimpのような戦術によって内部的に使われる。

code:lean

variable (α : Type)

variable (a b : α)

variable (f g : α → Nat)

variable (h₁ : a = b)

/-

α : Type

a b : α

f g : α → ℕ

h₁ : a = b

⊢ f a = f b

↓

⊢ a = b

-/

example : f a = f b := congrArg f h₁

code:lean

theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=

h ▸ rfl

確認用

Q. Lean 4のcongrArgとはどんなものか

参考

関連

メモ

Eq.subst 規則は、より明示的な置換を行う以下の補助規則を定義するために使われる。これらは関数適用項、つまり s t の形の項を扱うためのものである。具体的には、congrArg は s を固定して t を置換するのに使われ、congrFun は t を固定して s を置換するのに使われ、congr は s と t の両方を一度に置換するのに使われる。

調査用