Coqでの背理法の一例

Software Foundations Rel.vより

Definition partial_function {X: Type} (R: relation X) :=
forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.

Theorem le_not_a_partial_function :
~ (partial_function le).
Proof.
 unfold not.
 unfold partial_function.
 intros.
 
 assert (0 = 1) as Nonsense.
 apply H with (x:=0) (y1:=0) (y2:=1).
   apply le_n. apply le_S. apply le_n. inversion Nonsense.
Qed.

いきなり、0 = 1ってなんぞ？？？？と思ったけど、
仮定H

 H : forall x y1 y2 : nat, x <= y1 -> x <= y2 -> y1 = y2

の x = 0, y1 = 0, y2 = 1の場合のHの結論部分(y1 = y2)か。

背理法に限らず、forallを持つ定理／仮定の、特定の値の場合を新たな仮定として置きたい時に使えるな。なるほど。

=== 追記 ===
これってでも、背理法じゃねーよな。
前提のFalseからの爆発原理を使った普通の証明だ。

Coqは直観主義論理を使用した証明器なので、背理法や二重否定はビルトインされてない。そうな。Definitionで追加したり、Classic Moduleをインポートすれば使えるらしいが。
=== 追記終り ===

しかし、SoftwareFoundationsも改訂されて、Rel.vが、Prop.vやSflib.vの章の前に置かれるようになったのに、Require Exportしてるのが、前のSflibのままだな。

それに、total_relationは、Logic.vじゃなくて、この後の章のProp.vで定義されてるぞ？？？
この辺もさらに修正ありそうだな。