3
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

Falseの証明

Posted at

Coqで,次の2つの定理の証明を考えてみます.

  • True = False -> False
  • 1 = 0 -> False

どちらも正しくない等式からFalseを証明するものです.

各種定義

eqFalseTrueの定義を以下に示します.

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を証明して,今まで証明したtffpqrを使います.

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
3
0
2

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
3
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?