【Coq】コンピューターで証明しよう【コック】©2ch.net

[0001 片山博文MZ ◆T6xkBnTXz7B0 転載ダメ©2ch.net 2015/01/23(金) 01:41:03.17 ID:kQ1pk3tS]

Coqというプログラムを使えば、計算機上で数学的な証明を厳密に行うことができます。

http://www.iij-ii.co.jp/lab/techdoc/coqt/
http://ja.wikipedia.org/wiki/Coq

使いこなすには、大学レベルの数学と論理学とプログラミングと英語の知識が必要。
さあ、試してみよう！

[0123 １３２人目の素数さん 2015/04/18(土) 09:18:54.32 ID:Q1uVLxMU]

直観主義では証明できないので
Require Import Classical.
Variable (p q r:Prop).
Theorem T:((p /\ q) -> r) -> ((p -> r)\/(q -> r)).
Proof.
apply NNPP.
intuition.
Qed.

もっと手を抜くなら
Proof.
tauto.
Qed.

[0124 １３２人目の素数さん 2015/04/18(土) 10:22:46.84 ID:Q1uVLxMU]

p, q に関する排中律だけ仮定して

Variable (p q r:Prop).
Hypotheses (EM_p: p\/~p) (EM_q: q\/~q).
Theorem T:((p /\ q) -> r) -> ((p -> r)\/(q -> r)).
Proof.
intro H.
elim EM_p.
intro H0.
elim EM_q.
intro H1.
apply or_introl.
intro.
apply H.
apply conj.
exact H0.
exact H1.
intro.
apply or_intror.
intro.
contradiction.
intro.
apply or_introl.
contradiction.
Qed.

[0125 １３２人目の素数さん 2015/04/18(土) 11:34:32.18 ID:Q1uVLxMU]

pに関する排中律だけで

Variable (p q r:Prop).
Hypothesis EM_p: p\/~p.
Theorem T:((p /\ q) -> r) -> ((p -> r)\/(q -> r)).
Proof.
intro H.
elim EM_p.
intro H0.
apply or_intror.
intro H1.
apply H.
apply conj.
exact H0.
exact H1.
intro H2.
apply or_introl.
intro H3.
absurd p.
exact H2.
exact H3.
Qed.