よく知られているように、CoqをはじめとするLofの型理論では、等値性は「自身との間にのみ等値性が成立する」で定義されます。一方哲学者ライプニッツは「すべての性質を同じくするものの間には等値性が成立する」といったらしいです。
これも知られていますが、この二つの等値性は（型理論の枠組みでは）一致することが証明できるので、Coqの等値性とはライプニッツの等値性のことであるといわれます（特にJMeq などほかの等値性との比較の文脈で意識されます）。
にもかかわらず（いや、だからこそ？）Coqの標準ライブラリでは、ライプニッツの等値性に相当するInductiveな定義は存在しません。それに関連するLemmaが登録されているだけです（例えば f_equal や eq_ind_r がそれに相当するでしょう）。
本稿では、Coqのeq とライプニッツの等値性をCoq上で表現し、それらが同じものであることを直接証明してみます。なお、SoftwareFoundationsでも似た議論がありますが 、もう少し徹底してやってみます。
coqでのeq 相当を eq1, ライプニッツの等値性を eq2 として同値性は以下のように証明できます:
(* Lob Equality = Definitional equality *)
Inductive eq1 {A:Type} (x:A) : A -> Prop :=
| eq1_refl: eq1 x x.
(* Leibniz equality *)
Inductive eq2 {A:Type} (x:A) : A -> Prop :=
| eq2c y: (forall P, P x <-> P y) -> eq2 x y.
Theorem eq1_eq2_eq: forall (A:Type) (x y : A), eq1 x y <-> eq2 x y.
Proof. split.
intros []. pattern x. constructor. intros. split;trivial.
intros [z [H _]]. pattern z. apply H. apply eq1_refl.
Qed.
所感
- 型理論の枠組みで、Definitionalな等値性とライプニッツの等値性が同じだと証明できるという事実は、型理論を扱う限りはそれらを同一視できることをいうだけであり、ライプニッツの等値性をその等値性に還元できたということを意味しない、と思われる。意地悪ないいかたをすれば、型理論においてライプニッツの等値性はそのようなものとして粗視化・単純化して扱われているだけだ、という主張は通るのだろうか？
- 例えば Coq 上では 1+1=2 だが左辺は簡約できるという性質をもっているが、右辺は簡約できないという性質を持っている。したがって1+1と2は異なる性質をもち、区別できるとライプニッツはいうことができるはず。だから何だという話ではあるが……