各種定義

eq，False，Trueの定義を以下に示します．

Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
Inductive False : Prop :=  
Inductive True : Prop :=  I : True

True = False -> Falseの証明

通常の方法で証明すると次のようになります．

Theorem tff : True = False -> False.
Proof.
  intros. rewrite <- H. apply I.
Qed.

matchを使って証明すると次のようになります．

fun H : True = False => match H in (_ = y0) return y0 with
                        | eq_refl => I
                        end
     : True = False -> False

eq_indを使って証明すると次のようになります．

fun H : True = False => eq_ind True (fun P : Prop => P) I False H
     : True = False -> False

なお，eq_indの主張は以下の通りで，ここで少し説明しています．

eq_ind : forall (A : Type) (x : A) (P : A -> Prop),
    P x -> forall y : A, x = y -> P y

1 = 0 -> Falseの証明

ちょっとした道具を用意しておきます．

Definition disc n := match n with O => False | S n' => True end.

Theorem pqr P Q R : (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  intros. apply X0. apply X. apply X1.
Qed.

1 = 0 -> Falseを証明するためには1 = 0 -> True = Falseを証明して，今まで証明したtffとpqrを使います．

1 = 0 -> True = Falseの証明は以下の通りです．

Definition tf10 := fun H : 1 = 0 =>
eq_ind 1 (fun n : nat => disc 1 = disc n) (eq_refl (disc 1)) 0 H.
     : 1 = 0 -> disc 1 = disc 0

これで1=0 -> Falseの証明ができます．

pqr (1 = 0) (True = False) False tf10 tff
     : 1 = 0 -> False