■

Coqにおける等号は「Leibniz Equality」というもので、

  (forall P: Prop, P x -> P y) <-> x = y.

つまり「任意の命題に関して、同じ結論を与えるなら二つは等しい」というのが等しいの定義らしい。

等しくないことを示すにはどうすればよいかというと、結果が等しくならない命題を作ってやればいいわけだ。

たとえば Inductive で

Inductive X : Set := a | b.

とした場合は当然「a <> b」であって欲しいわけなのだが、「a」と「b」で結論が違うものをどうやって構成するかというと、奇妙なことに

Definition eq_a (x:X) := match x with a => True | b => False end.

でできるのである。この関数「eq_a」は「match」を使って引数が「a」だったら真を返し、「b」だったら偽を返す。
これを使って「a <> b」を証明する。

Lemma a_ne_b : a <> b.
unfold not; intros.
absurd (eq_a a).
rewrite H.
auto.
unfold eq_a.
trivial.
Qed.

というわけで、Inductiveの場合はmatchが二つのコンストラクタを必ず区別するということから、等しくないことを証明できた。

一般の場合も、二つを区別する述語が存在すれば等しくないことを証明できる。

Variable Y : Set.

Lemma neq : forall x y: Y, (exists P: Y->Prop, P x /\ ~P y) -> x <> y.
intros.
elim H.
intros.
unfold not.
elim H0.
intros.
absurd (x0 x).
rewrite H3.
auto.
auto.
Qed.

というふうにだいたい上のと同じ。

Leibniz Equality の重要な性質は「x=y」を仮定すれば、ほかのところに現れる「x」を勝手に「y」に置き換えてもよいということである。

最初の証明は実は「inversion」を使えば勝手にできる。