正本：FormalLab/Logic/Equality.lean

第9章：等式・代入・外延性・一意存在#

(fun x => x) 2 と 2 は計算すれば同じ式になります。一方、変数 x と y が等しいことは、通常は仮定または証明を必要とします。さらに関数の等しさは、全ての入力で結果が等しいという観察から導く外延性を要します。「同じ」という語は、ここで少なくとも三つの仕事をしています。

本章では定義的等しさと命題的等式を分け、反射性から対称性・推移性・代入・合同性を導きます。続いて関数外延性と命題外延性が追加する原理を明示し、存在量化へ等式条件を加えて一意存在を定義します。これは商、普遍性、圏論で一意性を読む準備になります。

等しい対象をあらゆる性質の中で置き換える#

型理論の論文では少なくとも二種類の等しさを区別します。

\Gamma\vdash t\equiv u:A \qquad\text{と}\qquad \Gamma\vdash p:t={}_A u

は、それぞれ定義展開・簡約による判断的等しさと、型 $A$ の内部にある等式命題の証明を表します。

定義的等しさは、定義展開と計算で同じ式になることです。型検査器自身が判定に使い、新しい仮定を要求しません。これに対し x = y : Prop は命題的等しさで、その型の証明項を要求します。rfl は x = x の基本構成子です。両辺が定義的に同じ式へ計算される場合にも rfl を使えます。

この区別は「明らかな等式」と「難しい等式」の差ではありません。前者は型検査の一部で、後者は型の内部に現れるデータです。命題的等式を仮定として受け取れば、述語や関数の中へ運べます。この代入可能性が、等式を単なる二項関係以上のものにしています。

命題的等式の形成、反射性、代入、計算は次の規則でまとめられます。 $P:A\to\mathsf{Prop}$ は等しい項を入れ替える文脈です。

\frac{\Gamma\vdash x:A\qquad\Gamma\vdash y:A} {\Gamma\vdash x={}_A y:\mathsf{Prop}} \qquad \frac{\Gamma\vdash x:A}{\Gamma\vdash \mathsf{refl}_x:x={}_A x}

\frac{\Gamma\vdash h:x={}_A y\qquad\Gamma\vdash p:P(x)} {\Gamma\vdash \mathsf{transport}_P(h,p):P(y)}, \qquad \mathsf{transport}_P(\mathsf{refl}_x,p)\equiv p.

最後の式は反射性に沿った移送が何もしないという計算規則です。対称性・推移性・合同性は、この除去と計算から導出する性質であり、等式へ別々に追加する原始規則ではありません。

Leankernel-checked counterpartL58–60

namespace FormalLab.Logic.Equality

universe u v

等式を作る・反転する・つなぐ#

Leanの Eq は、概略的には次のように反射性だけから生成される帰納族です。

inductive Eq {α : Sort u} (a : α) : α → Prop where
  | refl : Eq a a

右辺が変化する型族になっているため、h : x = y を除去するときは y を x に置き換えてよいことが導かれます。対称性や推移性は追加の構成子ではなく、この除去原理から証明できる性質です。

任意の項は自分自身と等しいという反射性です。

Leankernel-checked counterpartL78–79

theorem reflexive {α : Type u} (x : α) : x = x :=
  rfl

等式の向きを反転します。

Leankernel-checked counterpartL82–83

theorem symmetric {α : Type u} {x y : α} (h : x = y) : y = x :=
  h.symm

二つの等式を中間項でつなぎます。

Leankernel-checked counterpartL86–87

theorem transitive {α : Type u} {x y z : α} (hxy : x = y) (hyz : y = z) : x = z :=
  hxy.trans hyz

計算で閉じる等式と、仮定を使う等式#

次の左辺は関数適用と自然数の計算を進めると右辺になるので、証明は rfl です。これは「rfl が算術定理を知っている」のではなく、両辺が同じ正規形へ計算されるからです。

Leankernel-checked counterpartL96–97

example : (fun n : Nat => n + 1) 2 = 3 :=
  rfl

変数 x と y は計算だけでは一致しません。hxy : x = y が与えられて初めて、 x + 1 の中の x を y へ置換できます。rw [hxy] はこの等式除去を使うためのタクティク記法です。

Leankernel-checked counterpartL105–106

example {x y : Nat} (hxy : x = y) : x + 1 = y + 1 := by
  rw [hxy]

代入と合同性#

p : α → Prop を、穴に値を入れると命題になる文脈だと考えます。hxy : x = y があれば、穴へ x を入れて得た証明 p x を、y を入れた側の p y へ運べます。記法 hxy ▸ proof の三角形は、等式に沿った置換を表します。向きが逆なら hxy.symm を使います。

x = y を使い、x に依存する命題の証明を y 側へ運びます。

Leankernel-checked counterpartL118–120

theorem substitute {α : Type u} (p : α → Prop) {x y : α}
    (hxy : x = y) (proof : p x) : p y :=
  hxy ▸ proof

関数は等しい入力を等しい出力へ送ります。

Leankernel-checked counterpartL123–125

theorem congruence {α : Type u} {β : Type v} (f : α → β)
    {x y : α} (hxy : x = y) : f x = f y :=
  congrArg f hxy

同じ関数同士が等しければ、同じ引数へ適用した結果も等しくなります。

Leankernel-checked counterpartL128–130

theorem congruenceOfFunctions {α : Type u} {β : Type v} {f g : α → β}
    (hfg : f = g) (x : α) : f x = g x :=
  congrFun hfg x

関数と引数をそれぞれ等しいものへ替えても、適用結果は等しい。

Leankernel-checked counterpartL133–135

theorem congruenceOfApplication {α : Type u} {β : Type v} {f g : α → β}
    {x y : α} (hfg : f = g) (hxy : x = y) : f x = g y :=
  (congrFun hfg x).trans (congrArg g hxy)

congrArg は「等しい入力を同じ関数へ」、congrFun は「等しい関数を同じ入力へ」運びます。両方を組み合わせれば、関数と引数がそれぞれ等しい場合も扱えます。ただし合同性は一方向です。f x = f y から x = y が戻るには、後に導入する単射性が必要です。

外延性：観察結果から対象の等しさへ#

合同性は関数の等しさから各点の等しさを得ます。関数外延性は逆向きに、すべての入力で観察結果が等しければ関数自体も等しいと述べます。この結論は一般に計算だけでは得られないため、rfl ではなく funext を使います。

全入力で値が等しい関数は等しい、という関数外延性です。

Leankernel-checked counterpartL151–154

theorem functionExtensionality {α : Type u} {β : Type v} {f g : α → β}
    (pointwise : ∀ x, f x = g x) : f = g := by
  funext x
  exact pointwise x

論理的に同値な二命題は命題として等しい、という命題外延性です。

Leankernel-checked counterpartL157–158

theorem propositionExtensionality {P Q : Prop} (bothWays : P ↔ Q) : P = Q :=
  propext bothWays

P ↔ Q と P = Q も同じ構文ではありません。前者は二方向の含意、後者は命題を項として見た等式です。propext は論理的同値から命題の等しさへ進む外延性原理です。

Leankernel-checked counterpartL165–165

open FormalLab.Foundation.Functions

合成の結合則は、各入力で両辺を計算して関数外延性を使います。

Leankernel-checked counterpartL168–172

theorem composeAssociative {α β γ δ : Type}
    (h : γ → δ) (g : β → γ) (f : α → β) :
    compose h (compose g f) = compose (compose h g) f := by
  funext x
  rfl

この証明は二つの推論から成ります。

funext x で、関数の等式を任意の入力 x における値の等式へ変える。
両側の合成を展開すると同じ式になるので、rfl で閉じる。

つまり結合則全体は定義的等しさではありませんが、外延性で観察点へ移った後の等式は計算で成立します。外延性を使う箇所と定義展開だけで閉じる箇所が、証明項にも順に現れます。

存在に等式を加えて一意性を述べる#

単なる ∃ x, p x は、条件を満たす項を一つ提供しますが、別の項が同じ条件を満たす可能性を排除しません。一意存在は、存在証人に加えて、任意の別候補がその証人と等しいことを要求します。

\exists!x:A.\,P(x) \quad\Longleftrightarrow\quad \exists x:A.\,P(x)\land\forall y:A.\,P(y)\to y=x.

述語 p を満たす項が存在し、満たす項が全てその証人と等しいという定義です。

Leankernel-checked counterpartL198–199

def ExistsExactlyOne {α : Type u} (p : α → Prop) : Prop :=
  ∃ x, p x ∧ ∀ y, p y → y = x

0 は n = 0 を満たす唯一の自然数です。

Leankernel-checked counterpartL202–203

theorem existsUniqueZero : ExistsExactlyOne (fun n : Nat => n = 0) :=
  ⟨0, rfl, fun _ proof => proof⟩

existsUniqueZero の三成分を順に読むと、証人は 0、存在条件 0 = 0 は rfl、別候補 y の条件 proof : y = 0 はそのまま必要な一意性 y = 0 になります。一意性の等式を y = x と置くか x = y と置くかは慣習の差で、必要なら対称性で変換できます。

三種類の「同じ」を混同しない#

funext と propext の結論は定義的等しさではありません。Leanの論理が提供する外延性原理を明示的に使っています。また f x = f y から x = y は一般には戻せず、戻せる関数を「数学的関数とその性質」で単射と定義します。

この章の Eq を、型の同値や同型と混同してはいけません。二つの型の間に往復する関数があっても、それだけで型が命題的に等しいとは限りません。型同士をいつ同一視できるかは、より強い原理や後の構造の議論に関わります。

Leanの等式証拠は Prop に属するため、同じ等式を示す二証拠は証明無関連性により等しいと扱われます。一般の同一性型理論ではこの一意性は自動的ではありません。端点の置換に使えることから、経路間の高次情報まで同じだとは結論しません。

要点#

定義的等しさはkernelが計算と展開で判定し、証明項を追加しない。
命題的等式 x = y は型内部の命題で、rfl と等式除去から扱う。
代入は、x に依存する性質を等式に沿って y 側へ運ぶ。
合同性は対象の等しさから観察結果の等しさへ、外延性は十分な観察結果から対象の等しさへ進む。
一意存在は、証人・存在条件・他の候補との等式の三成分を持つ。

研究史と文献案内#

Fregeの論理にも同一性は含まれますが [FRE79]、型に依存する同一性型とは役割が異なります。 Martin-Löf型理論は判断的等しさと同一性型を区別して意味説明を与えます [ML84]。Leanの Eq は反射性を唯一の構成子に持つ帰納族ですが、Leanのkernel規則をMartin-Löf型理論の特定版と同一視しません。現行の Eq、propext、商による等式生成は [LEAN-REF] を参照します。

問題#

等式除去を置き換えの原理として展開する#

h : x = y から y = x を cases h と rfl だけで証明し、cases h の前後で文脈と目標がどう変わったかを書いてください。この変化を「等式を場合分けした」という表面的な説明で済ませず、任意の述語 p : A → Prop に対して p x から p y へ移送できる原理の特殊例として述べます。

x = y と f = g から f x = g y を二通り証明します。一方は項の等式を先に消去し、他方は関数の等式を先に消去します。中間目標を全て記録し、除去順が変わっても最終的な証拠の型が一致することを検証してください。

定義的等しさと外延性の役割分担を証明の各段で指す#

composeAssociative の証明を、関数等式を点ごとの等式へ移す段階と、各点で両辺が計算によって同じ項になる段階に分けてください。 funext と rfl のどちらかを取り除いた場合に、どの形の目標が未解決で残るかを具体的に示します。

さらに定数関数 fun _ : Bool => 0 を使い、f false = f true が成り立っても false = true は導けないことを反例として完成させます。関数合同性と関数外延性を逆向きの原理と誤読せず、逆を得るには単射性という追加仮定が必要だと説明してください。

存在と一意存在が持つ証拠の成分を分解する#

∃ x, p x の証明と ExistsExactlyOne p の証明を、証人、性質の証明、任意の他の候補との等式という成分に分けてください。存在証明だけでは二つの候補が異なることを排除できない例と、一意性だけでは候補が一つも存在しない場合を排除できない例をそれぞれ作ります。

最後に、Nat 上で「x + 1 = 3」の一意解を述べる命題を書き、存在、性質、一意性の各部を個別に証明します。解答は ∃! の記法だけで終えず、Leanの構成子へ展開したときにどの証明がどのフィールドを満たすかまで示します。