Coqで,次の2つの定理の証明を考えてみます.
True = False -> False
1 = 0 -> False
どちらも正しくない等式からFalse
を証明するものです.
各種定義
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