http://www.iij-ii.co.jp/lab/techdoc/coqt/
http://ja.wikipedia.org/wiki/Coq
使いこなすには、大学レベルの数学と論理学とプログラミングと英語の知識が必要。
さあ、試してみよう！
探検
【Coq】コンピューターで証明しよう【コック】©2ch.net
■ このスレッドは過去ログ倉庫に格納されています
http://www.iij-ii.co.jp/lab/techdoc/coqt/
http://ja.wikipedia.org/wiki/Coq
使いこなすには、大学レベルの数学と論理学とプログラミングと英語の知識が必要。
さあ、試してみよう！
Require Import Arith.
Theorem t: forall n:nat, 2*n = n+n.
intros.
replace (n+n) with (1*n + 1*n).
replace 2 with (1+1).
apply mult_plus_distr_r.
auto.
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
Qed.
Require Import Even.
Theorem t:forall n:nat, even (n * (1+n)).
intros.
apply even_mult_aux.
elim n.
left.
apply even_O.
intros.
elim H.
right.
apply even_S.
apply odd_S.
apply H0.
left.
apply H0.
Qed.
まずはTutorialを読むことから始めましょう。
natは自然数(natural numbers)の略です。
Coqでは英語や英語の略語がよく使われます。
そこんとこ誤解させんなよ
／⌒ ⌒＼
／ 癶 癶 ＼
／::::::⌒（__人__）⌒::::: ＼ あらあらうふふ
| |r┬-| |
＼ `ー'´ ／
すみません。
>>6
English speakerに前置きなく「コック」って言ったら誤解を産むよね。
「Arith」というモジュール(部品)を読み込むコマンドだ。
コマンド「Theorem t: forall n:nat, 2*n = n+n.」について。
「Theorem t:」は、これから「t」という名前の定理を証明するよって意味。
「forall n:nat,」は、「∀n∈Ｎ」という意味。
ここで「∀」は論理学における「任意の…に対して」という意味。
「∈」は集合論の「…に属する」に相当する。
自然数について調べたいなら「SearchAbout nat.」を入力。
足し算なら「SearchAbout plus.」。
証明モードでは、証明するための「タクティク」(戦術)を入力できる。
コマンドは大文字で始まるが、タクティクは小文字で始まる。
タクティクの例を挙げると、intros,symmetry,left,right,auto,elim,applyなど、いろんなタクティクがある。
証明の終わりでは「Qed.」コマンドを入力する。
黒い画面に「Coq <」と表示されるだろう。
これはCoqのプロンプトであり、入力待ちであることを表している。
黒い画面が消えるであろう。
このスレは人集まらないだろう。
数板ではプログラムの素養がネックになるか？
証明するの？
x^2 - 2x + 1 ＝ (x - 1)^2の証明。
いやいや、いいスレだ。せいぜい集まろうぜ
-の方はまだできてない。
Require Import Omega.
Require Import Arith.
Theorem t:forall n:nat,n*n+2*n+1=(n+1)*(n+1).
intros.
replace (2*n) with (n+n).
symmetry.
replace ((n+1)*(n+1)) with (n*(n+1)+1*(n+1)).
replace (n*(n+1)) with (n*n+n*1).
omega.
symmetry.
apply mult_plus_distr_l.
symmetry.
apply mult_plus_distr_r.
omega.
Qed.
もう少しだな。-2x＝+(-2)xを使えば、できるはずだ。
Ｙ
八 ヽ
（ __／/. ヽ,, ,）
丶1 八. !/
ζ, 八. j
i 丿 ､ j
| 八 |
| ! i ､ |
| i し " i '|
|ﾉ ( i i|
( '~ヽ ! ‖
│ i ‖
| ! ||
| │ |
| | | |
| | | |
| ! | |
Calculus of Inductive Construction (CIC)
（？：何種類かあって良く分からない）
について調べたいのですが良い文献ないですか？
整数か実数か複素数を使わないと。
Require Import Omega.
Open Scope Z_scope.
Theorem t: forall n:Z, n*n - 2*n + 1 = (n-1)*(n-1).
intros.
symmetry.
replace ((n-1)*(n-1)) with (n*(n-1)-1*(n-1)).
replace (1*(n-1)) with (n-1).
replace (n*(n-1)) with (n*n-n).
replace (n*n-n-(n-1)) with (n*n-(n-1)-n).
replace (n*n-(n-1)) with (n*n-n+1).
replace (n*n-n+1-n) with (n*n-n-n+1).
replace (n*n-n-n) with (n*n-2*n).
omega.
omega.
omega.
omega.
omega.
symmetry.
replace (n*n-n) with (n*n-n*1).
apply Z.mul_sub_distr_l.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.
Open Scope Z_scope.
の後で
SearchAbout Z.するとZの定義が見られるからね。
俺の環境だと証明が通らないんだが。
なんかミスってない？
訂正。ガラケーで入力大変。
(誤)
apply Z.mul_sub_distr_l.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.
(正)
apply Z.mul_sub_distr_l.
omega.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.
「３の倍数に６を足したものは３の倍数である」を証明せよ。
通った。
聞いた覚えはないな
「xは３の倍数である」
⇔
∃y∈Ｚに対して「x＝3y」、
だな。１階述語とexistsを使って解いてくれ。
Definition trimul (n:nat) := exists m:nat, n = 3*m.
と定義すればtrimul(0)は次のように証明できる。
Theorem tmzero: trimul(0).
unfold trimul.
exists 0.
auto.
Qed.
Require Import Arith.
Require Import Omega.
Open Scope Z_scope.
Definition trimul (x:Z) := exists y:Z, x = 3*y.
Theorem t: forall x:Z, trimul(x) -> trimul(x+6).
intros.
unfold trimul.
destruct H.
exists (x0+2).
replace (x) with (3*x0).
omega.
Qed.
「unfold x.」はゴールにあるxをその定義に展開するタクティクだ。
「destruct H.」はHを崩すタクティク。
「３の倍数に４を掛けたものは６の倍数である」を証明。
Require Import Omega.
Require Import Arith.
Open Scope Z_scope.
Definition tr(x:Z) := exists y:Z , x=3*y.
Definition s(x:Z) := exists y:Z,x=6*y.
Theorem t: forall x:Z,tr(x)->s(4*x).
intros.
unfold s.
destruct H.
exists (2*x0).
replace x with (3*x0).
omega.
Qed.
多分このスレには片山さんと俺しかいないぞｗ
正解！
このスレを立てた目的は…
１．Coqの知名度アップと啓蒙。
２．Coqによる「片山QZの定理」の証明。
３．Coqと人工知能の連携を考えること。
ここをもう少し詳しく
Coqでの証明法がだれにも分かりやすくなるようあえて題材は
簡単なものを選んでいるの？
もっとCoqの強力さが分かる位難しい題材でやってくれんかな。
そもそもCoqではどの位難しいものがどの位の手間で証明できるの？
単純に言えば、コンピューターでできた数学者を作ろうとしている。
数学の問題は、式の変形と問題の分解と解の探索の問題に還元されるから、
人工知能でもいくつかの問題を解くことができるはずだ。
はじめは基礎と慣れが大事。不満なら君も出題してもかまわない。
次は集合論から出題したまえ。
なぜ集合論？
一応念のためいっとくが>>42は某スレの1(俺)とは別人だぞ。
「Z⊆XかつZ⊆YならばZ⊆X∩Y」を証明せよ。
Coqあるいは片山さんは、東大ロボプロジェクトはどう評価してるの？
集合問題でなく整数問題の系統だが、まずはこういう易しめのお題はどう？
お題：正整数m、nがあり、LCM(m,n) + GCD(m,n) = m + n とする。
このとき、m, n のどちらか一方は、他方によって割り切れることを示せ。
だが人間にとって証明問題といえばふつうこれくらいからだろ？
☆ 自民党、グッジョブですわ。 ☆
http://www.soumu.go.jp/senkyo/kokumin_touhyou/index.html
☆ 日本国民の皆様方、2016年7月の『第24回 参議院選挙』で、改憲の参議院議員が
3分の2以上を超えると日本国憲法の改正です。皆様方、必ず投票に自ら足を運んでください。
そして、私たちの日本国憲法を絶対に改正しましょう。☆
http://ideone.com/Aa07zr
「Z.lcm m n = m0 * n0 * Z.gcd m n」の証明が難しい。
名古屋大学 佐藤雅大さん
http://shirodanuki.cs.shinshu-u.ac.jp/TPP/TPP2013_satou.pdf
からTutorial.pdfとReference-Manual.pdfとrefman.tar.gzを
ダウンロードすること。
まじめにやってくれてサンクス。
それで
>http://ideone.com/Aa07zr
これはすべて人が書いてるんだね？ だとするとメリットがわからんな。
「コンピュータを使って定理証明する」て、人が形式証明を計算機に打ち込む
ということか？ふつうはそれとは違う意味で言うことだが。
それは私が書きました。
Classicalモジュールを使えばね
東大ロボは>>48くらいは当然自動で解くんだがね
Ensemblesってのでいいのか？
そこからわからんｗ
もうちょっとやってみるわ
よくわからぬ。
自動定理証明器の設計の話題にまで広がりますように
賛成かな？
ただ俺の場合は、Coqの細かい話はうんざりだ。単なる証明支援の今のCoqなら将来はないんだから。
早く自動証明の話をしてくれ
Coqのソースコードは同じ場所でダウンロードできる。
自動証明を行いたいなら、Omegaのようなモジュールを自作するか、
Coqを改造するか、Coqと対話する必要がある。
coq-8.4pl5というフォルダーができる。
ここにパスcoq-8.4pl5/plugins/omega/にOmegaが記述されている。
ファイルの中身はテキストエディターなどで確認できる。
Coqスレ
http://peace.2ch.net/test/read.cgi/tech/1300017923/
> Coqを改造するか、Coqと対話する必要がある。
Coqの延長でできる風に言ってるが、それはもうCoqではないだろう
人間も結局過去の膨大な証明から経験的に学んでるわけだし。
それとも人間が証明できる定理は原理的にCoqでも証明できる？
Coqはなにも証明しない！人間が証明してる。Coqは証明用ワープロ
えっ、正しい論証になってるかチェックしてくれないの？
すぐメモリたんなくなるだろうけど。
一苦労どころじゃないだろｗ
このスレッドを見ても、ほとんど定義そのもの程度の命題の証明がお題になるくらいだからな
OCamlな。
Coqの動作原理を知りたいならOCamlで書かれたCoqのソースとにらめっこ
心臓部を理解すれば後は枝葉
心臓部とか何ステップくらいなのよ？
数学の本スレでちょっと前に誰かが聞いて、
経験者らしきそっちの学識ありそうな誰かが応えてた
自動定理証明器の古典本あたりから読まないと・・・
勉強会とかするなら参加したいわ
当たり前の真実である「公理(axiom)」の集合から「定理(theorem)」を証明により導出し、
さらに既存の公理の集合と、証明された定理の集合から導出された、新しい定理をさらに土台とする。
そのように数学は、間違いのない証明によって次々と築き上げるものである。
どんな命題でも証明可能になり、証明が無意味となる。
なにを言いたい？
なお、証明が間違っていても公理系は崩壊しないｗ
この船頭では…
公理の集合のことを公理系って言うんだったね。
よって>>95-96は間違い。
それは前から分かっていること
http://ja.wikipedia.org/wiki/%E3%82%AF%E3%83%AF%E3%82%A4%E3%83%B3%E3%83%BB%E3%83%9E%E3%82%AF%E3%83%A9%E3%82%B9%E3%82%AD%E3%83%BC%E6%B3%95
証明のコードを生成してみるのもまた愉し。
一例の場合か全ての場合かってこと？
証明システムなら人工知能が結論までの道筋を自ら見つけるということになるはず。
Variable B:(A -> Type) -> A -> Type.
Definition mu := fun (x:A) => forall P:(A -> Type), (forall (y:A), B P y -> P y) -> P x.
Hypothesis m : forall (P Q:A -> Type), (forall (x:A), P x -> Q x) -> (forall (x:A), B P x -> B Q x).
での
Theorem r1:forall (x:A), B mu x -> mu x.
の証明なんだけど、
2 subgoals
A : Type
B : (A -> Type) -> A -> Type
m : forall P Q : A -> Type,
(forall x : A, P x -> Q x) -> forall x : A, B P x -> B Q x
x : A
a : B mu x
P : A -> Type
b : forall y : A, B P y -> P y
x0 : A
y : mu x0
============================
forall y0 : A, B (fun x1 : A => P x1) y0 -> P y0
subgoal 2 is:
B mu x
のあとどうすればいいでしょうか？上記のsubgoalの中の
(fun x1 : A => P x1)をPに変える命令とかあるんでしょうか？
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.
までが上記の結果です。
>数学の体系は、公理系によって成り立っている。すなわち、
>当たり前の真実である「公理(axiom)」の集合から「定理(theorem)」を証明により導出し、
>さらに既存の公理の集合と、証明された定理の集合から導出された、新しい定理をさらに土台とする。
>そのように数学は、間違いのない証明によって次々と築き上げるものである。
ゲーデルの不完全性定理によれば
あんたの言ってる事は数学の本性の上っ面でしかない
浦山
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.
intro y0.
apply (b y0).
apply a.
Qed.
は証明できますか
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.
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.
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.
レス大感謝です。しかし、
apply (b y0).
のところで、
Error: Impossible to unify "B P y0 -> P y0" with
"B (fun x0 : A => P x0) y0 -> P y0".
と叱られました。Coqのバージョンが
Welcome to Coq 8.3pl3
で古いのでしょうか。
ありがとうございます。
知らなったタクティクがいっぱいありますね。
coq8.4からη変換が入ったみたいね
多分これでη変換無しで行けると思う
Variable A:Type.
Variable B:(A -> Type) -> A -> Type.
Definition mu := fun (x:A) => forall P:(A -> Type), (forall (y:A), B P y -> P y) -> P x.
Hypothesis m : forall (P Q:A -> Type), (forall (x:A), P x -> Q x) -> (forall (x:A), B P x -> B Q x).
Theorem r1:forall (x:A), B mu x -> mu x.
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.
intros y0 c.
apply b.
apply (m (fun x : A => P x) P).
trivial.
exact c.
exact a.
Qed.
レス大感謝です。さて、また私にとって難題です。エラーが出る最小限の
手順を用意しましたので、偉い方、どうかお付き合いください。
第1の例
Definition Eqt (A B:Type): Prop := (A = B) \/ (B = A).
Axiom Ee : forall (a b:Set), Eqt a b -> ((a = b) /\ (b = a)).
Theorem Eab : forall (a b:Set), ((a = b) \/ (b = a)) -> a = b.
Proof.
intros a b Hab.
assert (Hta:(a = b) /\ (b = a)).
apply Ee.
unfold Eqt.
assumption.(*ここでエラーが出ます*)
Qed.
これは、Display implicit argumentsとDeactivate notations display
をすることによって、Implicitな変数が原因であることがわかりました。
Proof completed.が表示されるのに、Qedの後エラーとなるのです。
第2の例
Definition Eqt (A B:Type): Prop := (A = B) \/ (B = A).
Axiom Ee : forall (a b:Set), Eqt a b -> ((a = b) /\ (b = a)).
Theorem Eab : forall (a b:Set), ((a = b) \/ (b = a)) -> a = b.
Proof.
intros a b Hab.
assert (Hta:(a = b) /\ (b = a)).
apply Ee in Hab.
assumption.
elim Hta.
intros H H0.
assumption.
Qed.
どうかお救いください。トホホ
130のようなQedでエラーになるのは結構あって、証明モードの途中ではあんまり頑張って型検査しないから、
こういう微妙な型の差しかないときはしかたないかな。
証明法を探すのではなく、>>129の
＞Definition Eqt (A B:Type): Prop := (A = B) \/ (B = A).
の部分を
Definition Eqt (T:Type) (A B:T) : Prop := (eq (A := T) A B) \/ (eq (A := T) B A).
Implicit Arguments Eqt [T].
と変えました。これで、>>129の証明の仕方でもエラーは出なくなりました。
ちなみに最期まで証明すると、
Axiom Ee : forall (a b:Set), Eqt a b -> ((a = b) /\ (b = a)).
Theorem Eab : forall (a b:Set), ((a = b) \/ (b = a)) -> a = b.
Proof.
intros a b Hab.
assert (Hta:(a = b) /\ (b = a)).
apply Ee.
unfold Eqt.
assumption. (*ここでエラーが出ずに先へ進めます*)
elim Hta; intros H1 H2.
assumption.
Qed.
詳しいことがわかるURLないでしょうか。
http://compcert.inria.fr/compcert-C.html
読んでみます。
こりゃすげーや
停止するコードは必ずCoqでも等価なコードがかけるのかどうか気になります。
書けるんでしょうか？
大まかでいいので。
http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
があって、ここのdownloadから拾ってきたものでPDF作る（make, make pdfする）と章順が逆になって、最初にPostscriptが
最後がPrefaceとSymbolになったものができてしまいます。
正しくmakeできた方いたら、やり方教えて下さい。
このライブラリを使えばいいんじゃないかな、
https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ConstructiveEpsilon.html
nステップ以下で停止するって述語が
Hypothesis P_dec : forall n, {P n}+{~(P n)}.
を満たしていれば、停止するステップ数を構成してくれるよ。
これをシェルスクリプトで逆順にしたら、それらしい順番のPDFになりました。
書き忘れましたが、使ってた環境はcoq 8.4pl6です。
お騒がせしました
返信遅れてすいません。
読んでもよく理解できないTT
たとえば２つのプログラムが与えられて、
どちらが後に停止するか、みたいなことはできるんでしょうか。
アッカーマン関数のような巨大な関数との比較がしたいのですが。
特集 コンピュータにできる数学・できない数学
Coq:型理論から来た証明支援系, Jacques Garrigue
「x>1ならば、そのべき乗は、いつか特定の数を追い抜く」という命題が証明できません。
Require Import Omega.
Theorem multi_inf_gt3:
forall (x : nat), x>1 -> exists m : nat, x^m > 1000.
proof.
intros.
exists 1000.
induction x.
omega.
assert (x>1 -> x^1000<S x^1000).
intro.
apply (Nat.pow_lt_mono_l_iff x (S x) 1000).
auto.
auto.
assert ((x>1->x^1000>1000)->(x>1->x^1000<S x^1000)->(x>1->S x^1000>1000)).
omega.
apply H1 in H0.
apply H0.
apply IHx.
ここで、仮定は「S x > 1」、ゴールは「x > 1」となって、証明できません。
お知恵を貸していただけないでしょうか……
Require Import Omega.
Theorem t:
exists m : nat, 2^m > 1000.
Theorem t:
2^10 > 1000.
僕もomega単独では解けませんでした。
Theorem t1:
2^10 > 1000.
(* proof. *)
simpl.
omega.
Qed.
Theorem t2:
exists m : nat, 2^m > 1000.
(* proof. *)
exists 10.
simpl.
omega.
Qed.
元の問題にもsimpl使えない？
プレスバーガー算術を対象としているから、らしい
simplは単に定義に従って簡約してくれる
よって>>149には適用できるが、>>148はmatchできなくて無理
2^10=1024 > 1000を使うのがポイントだったみたいです。
Require Import Omega.
Theorem multi_inf_gt4:
forall (x : nat), x>1 -> exists m : nat, x^m > 1000.
(* proof. *)
intro.
intro.
destruct x.
omega.
exists 10.
assert (S x>1 -> 2^10 <= S x^10).
intro.
apply (Nat.pow_le_mono_l_iff 2 (S x) 10).
auto.
auto.
change (S x > 1 -> 1024 <= S x ^ 10) in H0.
apply H0 in H.
omega.
Qed.
レスして下さった皆様、ありがとうございます。
次は実数でチャレンジするかも!?
x^10を原始的にxで割っていく方法です。 右辺が10000だったらどーするんだwww
Require Import Rbase.
Require Import Fourier.
Theorem multi_inf_gt6:
forall (x : R), x>2 -> exists m : nat, (Rpow_def.pow x m)>1000.
Proof.
intro.
intro.
exists 10%nat.
simpl.
apply Rmult_le_0_lt_compat.
fourier.
fourier.
apply H.
apply Rmult_le_0_lt_compat.
fourier.
fourier.
apply H.
apply Rmult_le_0_lt_compat.
fourier.
fourier.
apply H.
assert (2*/2*125=125).
apply Rinv_r_simpl_r.
discrR.
assert (forall (a b c d:R), a*b*c = a*(b*c)).
intros.
ring.
rewrite H1 in H0.
rewrite <- H0.
apply (Rmult_le_0_lt_compat 2 x (/2*125) (x*(x*(x*(x*(x*(x*1)))))) ).
fourier.
fourier.
apply H.
all: cycle 1.
apply x.
apply (Rinv_r_simpl_r 2 (/2*125)).
discrR.
rewrite H1 in H2.
rewrite <- H2.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*125)) (x*(x*(x*(x*(x*1))))) ).
fourier.
fourier.
apply H.
assert (2*/2*(/2*(/2*125))=/2*(/2*125)).
apply (Rinv_r_simpl_r 2 (/2*(/2*125)) ).
discrR.
rewrite H1 in H3.
rewrite <- H3.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*125))) (x*(x*(x*(x*1)))) ).
fourier.
fourier.
apply H.
assert ( 2*/2*(/2*(/2*(/2*125))) = /2*(/2*(/2*125)) ).
apply (Rinv_r_simpl_r 2 (/2*(/2*(/2*125))) ).
discrR.
rewrite H1 in H4.
rewrite <- H4.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*(/2*125)))) (x*(x*(x*1))) ).
fourier.
fourier.
apply H.
assert ( 2*/2*(/2*(/2*(/2*(/2*125)))) = /2*(/2*(/2*(/2*125))) ).
apply (Rinv_r_simpl_r 2 (/2*(/2*(/2*(/2*125)))) ).
discrR.
rewrite H1 in H5.
rewrite <- H5.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*(/2*(/2*125))))) (x*(x*1)) ).
fourier.
fourier.
apply H.
assert ( 2*/2*(/2*(/2*(/2*(/2*(/2*125))))) = /2*(/2*(/2*(/2*(/2*125)))) ).
apply (Rinv_r_simpl_r 2 (/2*(/2*(/2*(/2*(/2*125))))) ).
discrR.
rewrite H1 in H6.
rewrite <- H6.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*(/2*(/2*(/2*125)))))) (x*1) ).
fourier.
fourier.
apply H.
apply x.
apply x.
apply x.
apply x.
apply x.
Qed.
1<x<2の場合はどうするんだろう？
俺は力になれないが頑張れｗ
今日のCoq：
Require Import Rbase.
Require Import Fourier.
Lemma l2:
forall (x y:R), y>1 -> x=1+1/y -> 1<x<2.
Proof.
intros.
rewrite H0.
assert (forall (a b:R), a<b -> 1+a<1+b).
intro.
intro.
intro.
fourier.
apply conj.
assert (1+0=1).
ring.
replace (1<1+1/y) with (1+0<1+1/y).
apply (H1 0 (1/y)).
all: cycle 1.
rewrite H2.
reflexivity.
all: cycle 1.
assert (0<1 -> 0<1/y -> 1/y*0<1/y*1).
intro.
apply (Rfourier_lt 0 1 (1/y)).
auto.
assert (1/y*0 = 0).
ring.
rewrite H4 in H3.
assert (1/y*1 = 1/y).
ring.
rewrite H5 in H3.
ここまでで、仮定が0 <1 -> 0<1/ y -> 0 <1/ y、
サブコールが0 < 1 / yで頓挫。。。
>>159はあきらめます。
まず1<x<2 -> x^m>2^10を証明して、それから1<x<2 -> x^m>1000を証明しています。
Require Import Rbase.
Require Import Fourier.
Theorem multi_inf_gt7':
forall (x y:R), 1<x<2 ->
x=1+1/y ->
(Rpow_def.pow x (Z.to_nat (up y)))>2 ->
(Rpow_def.pow x ((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))))>2*2*2*2*2*2*2*2*2*2.
Proof.
intros.
rewrite Rdef_pow_add.
（↑を9回）
apply Rmult_le_0_lt_compat.
fourier.
fourier.
（↑を9回）
apply H1.
（↑を10回）
Qed.
forall (x y:R), 1<x<2 ->
x=1+1/y ->
(Rpow_def.pow x (Z.to_nat (up y)))>2 ->
(Rpow_def.pow x ((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))))>1000.
Proof.
intros.
assert ((Rpow_def.pow x ((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))))>2*2*2*2*2*2*2*2*2*2 ->
(Rpow_def.pow x
((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))))>1000).
intro.
fourier.
apply H2.
apply multi_inf_gt7'.
apply H.
apply H0.
apply H1.
Qed.
これをCoqで証明するのは難しそうなので、
このへんにしておきます。
１．都内でCoq大会を開きたい。ゲーム形式でCoqの技能を競う。
２．Coqの数式操作をGUIでできるようにしたい。部分数式ごとに適用できるタクティクを「見える化」したい。
３．Coq Twitter BotやCoq onlineを作りたい。
やらないといけないことが他にもあるし。
まあ頑張ってくれ。
インタラクティブなやつならなお良し。
onlineはproofwebやらjscoqやらあるしbotの方が面白そうだな
140字でどの程度のことができるのかわからんが
http://gathery.recruit-lifestyle.co.jp/article/1146775541637910801
表示してくれるのですが、その機能をローカルに自分のパソコンでも
使えるようにできるのですか？できるのでしたらやり方を教えてもらえないで
しょうか。
http://proofweb.cs.ru.nl/install.php
レスありがとうございます。でも今Linuxは無理です。
残念です。
仮想環境のVirtualBoxを使う手がある。
405 ： 猫は唯の馬鹿 ◆MuKUnGPXAY [age] 投稿日：2011/04/09(土) 15:29:50.46
猫
￥
￥
https://goo.gl/ji1QUd
> English speakerに前置きなく「コック」って言ったら誤解を産むよね
日本語話者にも開発者のCoquandの名前を「コカン」って呼んだら誤解生みそう
「Coqはコカンが生みました」
？？？？？
それは翻訳じゃなくて詳細な機械証明をつけたことになるからいいんじゃね？
やれるもんならやってごらん（挑発）
学コン・宿題ボイコット実行委員会@gakkon_boycott 9月1日
#拡散希望
#みんなで学コン・宿題をボイコットしよう
雑誌「大学への数学」の誌上で毎月開催されている学力コンテスト(学コン)と宿題は、添削が雑で採点ミスが多く、訂正をお願いしても応じてもらえない悪質なコンテストです。(私も7月号の宿題でその被害に遭いました。)このようなコンテストに参加するのは時間と努力の無駄であり、参加する価値はありません。そこで私は、これ以上の被害者を出さないようにするため、また、出版社に反省と改善を促すために、学コン・宿題のボイコットを呼び掛けることにしました。少しでも多くの方がこの活動にご賛同頂き、このツイートを拡散して頂ければ幸いです。
https://twitter.com/gakkon_boycott/status/1300459618326388737
https://twitter.com/5chan_nel (5ch newer account)
ありがとうございます😊
やってみようと思います。
ありがとうございます．
その本は読んだことがあるのですが，何が書いてあるのかよくわかりませんでした．
その本を読むための予備知識はどんな本を読めばいいのでしょうか？
あんまり伸びてないけど、ム板にこういうスレがある。
【F*】依存型っていいの？【Coq】
https://mevius.5ch.net/test/read.cgi/tech/1554809503/
みたいな関数ってCoqでどう性質を証明しますか？ifの条件で場合分けしたいです
タクティックでcase ( x< 10)としても、
仮説にならないで、場合わけにならずに困っています。
はっきり見てないけど、こことか参考にならないかな？
https://stackoverflow.com/questions/16555022/proving-if-then-else-in-coq
まさにこれっぽいです。ありがとうございます！
Asciiは扱えるみたいです。
これの練習問題の2つ目が分からない。
＞問1. 任意の命題 A B C に対して、「A ならば B ならば C」ならば「B ならば A ならば C」が成り立つ。
要するにこれはB⇒Aが可能なら、前提条件からA⇒Cだと思ったけど。
どう書くの？全然分からん
Definition prop4 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C):=
fun A B C a b c => ?.
Definition prop4 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C) :=
fun A B C f b a => f a b.
かな。f の型が (A -> B -> C) で、b の型が B で、a の型が A 。
「ならば」(->) は右結合だから、(B -> A -> C) の部分の括弧は外す事ができる。
https://developers.srad.jp/story/21/06/16/1737205/
もっと勉強しなくては
|Д｀) ﾀﾞﾚﾓｲﾅｲ･･ｵﾄﾞﾙﾅﾗ ｲﾏﾉｳﾁ
|⊂
|
♪ Å
♪ ／ ＼ ﾗﾝﾀ ﾀﾝ
ヽ(´Д｀;)ﾉ ﾗﾝﾀ ﾀﾝ
( へ) ﾗﾝﾀ ﾗﾝﾀ
く ﾀﾝ
♪ Å
♪ ／ ＼ ﾗﾝﾀ ﾗﾝﾀ
ヽ（;´Д｀）ﾉ ﾗﾝﾀ ﾀﾝ
(へ ) ﾗﾝﾀ ﾀﾝﾀ
> ﾀﾝ
|Д｀) ﾀﾞﾚﾓｲﾅｲ･･ｵﾄﾞﾙﾅﾗ ｲﾏﾉｳﾁ
|⊂
|
♪ Å
♪ ／ ＼ ﾗﾝﾀ ﾀﾝ
ヽ(´Д｀;)ﾉ ﾗﾝﾀ ﾀﾝ
( へ) ﾗﾝﾀ ﾗﾝﾀ
く ﾀﾝ
♪ Å
♪ ／ ＼ ﾗﾝﾀ ﾗﾝﾀ
ヽ（;´Д｀）ﾉ ﾗﾝﾀ ﾀﾝ
(へ ) ﾗﾝﾀ ﾀﾝﾀ
> ﾀﾝ
https://i.imgur.com/KhOaFYh.jpg
https://i.imgur.com/G6EhYnQ.jpg
https://i.imgur.com/Wko98J0.jpg
https://i.imgur.com/lBK5S88.jpg
https://i.imgur.com/wiB134L.jpg
https://i.imgur.com/dfbPv74.jpg
https://i.imgur.com/JV7dvrw.jpg
https://i.imgur.com/5Xy5Ysa.jpg
https://i.imgur.com/gG6jyLz.jpg
https://i.imgur.com/ecuGrKr.jpg
https://i.imgur.com/hqUKYvN.jpg
選択公理が命題として他の公理とは独立であることの証明とかできるかな？
もっと素朴に、√2が有理数では無いことの証明とか、
eやπが有理数ではないことの証明とか、
複素数係数の代数方程式は複素数の根を必ず持つことの証明とか。。。
勉強しないとだめですよね。
数学の知識よりも、プログラミングの知識のほうが重要だと思う。
関数型言語についてとか。
>ゲーデルの不完全性定理の証明
無矛盾(矛盾が証明されない)ならば
無矛盾性が証明されない、と読むから
神秘性や難しさを感じる
矛盾が証明されると矛盾する、という証明から
矛盾の証明が出来る、と読めばただのトリック
初心者は必ず騙されるが
証明論とは命題の証明方法の理論ではない
ちなみに命題の証明方法は別に難しくない
ただ証明がない場合、止まらないので
「アルゴリズム」とは言えないが
> √2が有理数では無いことの証明
Coqと同様の定理証明支援系であるHOL LightのTutorialに
11.1 Irrationality of √2がある
www.cl.cam.ac.uk/~jrh13/hol-light
実際にそこで証明しているのは
∀p,q. p×p=2×q×q ⇒ q=0 だけど
数学とプログラミングが統一される前に時間切れでシンギュラリティが来そう。
ただし、その有限回なる回数が一体どのぐらいの有限なのかだ。宇宙が終わるまで
かけても終わらない程の大きな回数であっても有限だから。
その証明が正しいことを確認する作業は、必ず証明の
記述の長さの多項式オーダーの手間で可能なのだろうか？
必ず有限の時間で検証を終えて停止するのだろうか？
その有限の時間だといっても途方も無く長くなったりしないのだろうか？
検証を行う前に、証明の記述に応じてそれに対する検証時間の上界が
事前に得られるものだろうか？
それともそのような上界は一般にはなくて、ただただ結果が出るまで
ずーっと待って運良く生きているうちに終わることを期せねばならないのだろうか？
C言語とかAlgolのような普通のプログラミング言語は、
コンパイルすべきプログラムの長さNに対するコンパイル完了までの時間は
O（N log N)程度になってる。もしもコンパイルの時間がたとえばO(N^2)
かかるような言語とかコンパイラであると、プログラムの記述が大規模になれば
実用性が低くて使い物にならない感じになる。
証明になっているか否かのチェックは有限時間で可能
証明になってないギャップについて
ギャップが埋められるかどうかは
命題が証明できるかどうかと同じなので
有限時間では判定できない
しないのであれば、検証システムは使い物になるが、Nについてたとえば多項式
オーダーではなかったならば、少しばかり長い「証明」を検証しようとすれば
現実的には「いつまでたっても終わらないなぁsigh、修論が落ちるな」、
ということになりそうだけれども、そのあたりはどうなっているのでしょうか？
著者は自分の証明を検証系にかけて、
検証系に与えたソースコードも併せて提出する。
論文の査読者はそのソースコードが正しく論文の定理や命題を表していることを
（ああたいへんだ）チェックして（そこが間違ってたらどうする？）、
検証系にかけて、正しく証明されることを確認したら、アクセプトする。
そうなったらとても面倒。論文のLaTeXのソースを提出するのとは次元が違う。
Coqで検証すればよかったんじゃないの？できないの？
いろいろな前提知識の無い無垢のソフトに全く隙のない形で
完璧に記号だけを使って記述し直すというのは、とても大変な
作業になるだろう。暗黙知、専門家の常識、そういうものを総動員して
それらも含めて検証にかけなければ、論理が飛んでいることになるから
だろう。
白黒はっきりつけるためにはした方が良さそうですね
おそろしく時間とお金（人件費）が掛かりそうですが…
という場合はあり得るのだろうか？
その証明が正しいならばコンピューターが理解できる形の形式的な証明に書き直せますよね？
非構成的な証明とかは、形式的な証明に落とし込めるのかなあ？
そのメタメタ数学を外から眺めているメタメタメタ数学、とどこまでいっても
その外側から眺めている数学があるのだとしたら。この宇宙も、メタ宇宙の中で
眺められ観察され実験されている存在なのじゃないかと思えてくる。
ある日、これじゃダメだな、やり直すかという声が聞こえてきて。。。
証明が正しい可能性が極めて高い、としか言えなくて
厳密に正しいとは確定していないように思うがどうだろう
smooth linear partial differential equation without solution
https://planetmath.org/smoothlinearpartialdifferentialequationwithoutsolution
解が存在しないことを証明できますか？
それから矛盾を出してやり、よって証明は存在する。
しかし具体的に証明を構成しない。
そういうやり方の「証明」はCoqで記述できるのかな？
ゲーデル数化とかガチで出来るんだね。すごいわ。
ゲーデルの不完全性定理の形式証明を読む
https://qiita.com/41semicolon/items/caceb8bc52172190902d
背理法を使わずに対偶で書き直せばできるのでは？
>ゲーデル数化とかガチで出来るんだね。すごいわ。
コード化は別に難しくない
証明可能性述語の記述のほうが面倒
まあでもやればできるだろうな
別に神秘的なことはやってない
>”クルト・ゲーデル 史上最もスキャンダラスな定理を証明した男”
タイトルが大袈裟すぎｗ
原題は"Journey to the Edge of Reason"
著者のStephen Budianskyは、別に数学者ではないらしい
ゲーデルの生涯に関心があるなら
Dawsonの"Logical Dilemma"を読むことを勧める
日本語訳もある
不完全性定理について知りたいなら
ホフスタッターのゲーデル・エッシャ―・バッハの
第１４章を読んだほうがいい
興味深い定理であることは確かだが
なんか持ち上げられすぎ
ゲーデル自身は理性の完全性を信じていたので
不完全性定理の結論は彼の願望とは必ずしも合致しない
://rio2016.5ch.net/test/read.cgi/lifesaloon/1662167492/l50
戦後まだGHQが日本を占領していた頃のことである。
都内は椎名町にあった帝国銀行に白衣を着た男がやって来て
保健所から来た。近所で赤痢（？）が発生した。だがこの
薬をのめば感染を防げると行内の客や行員に言って、
薬の飲み方を実演して見せて、そうして一人ずつ呑ませて
いった。呑んですぐには症状が出なかったので、みんな
おとなしく従って呑んだが、しばらくすると次々と倒れて、
その男は行内から手形だったか僅かな金を持って逃げた。
という事件だ。
これを今のコロナ騒動・ワクチンの話に照らして考えてみると
面白い。
遅効性の薬物（即座に効果が出ずに、ある程度時間が経ってから
効果を発揮する）は、それが毒作用を持つものであれば、後で
大量の薬害を生みかねない。日本向けに特別にカスタマズされた
ものだったりすると、日本民族全滅も可能。
https://pc.watch.impress.co.jp/docs/news/1477452.html
行政とIT企業との関係。住民の情報をどこかに
Coqに証明させようとすると、どうなるだろうか？
そういうことを考えると、脳外科が自分で自分の脳の手術
をするというような、なんだかとてもいやーぁな感じがする。
その部分の影響でCoqの検証系が正しく動作しないためであるのかどうかが
怪しくなる。
ソースコードから形式記述を作り出すところの正しさも証明しなければならない
はずだし。その形式記述を作り出すシステムの正しさも証明しなければならないが、
。。。。とやっていると、本当の正しさを証明するということは、無理じゃね？
という暗澹たる気持ちになる。結局は正しさというのは信仰の一種であるか、
何かを信じることで魂の安らかさを得る必要があり、心に不安があると
Gのようにキチガイになったりすると思う。
そうして論理は言葉（記号）によって書かれる。
現代の数学はユダヤ教の思考の派生品なのかもしれない。
下記のcase tacticでなぜ証明終わるでしょうか？
場合分けのためと理解しているので、なぜ終わるかわかりません。
Lemma f_test :forall A:Prop, A -> not A -> True.
Proof.
intros H H0 H1.
case (H1 H0).
Qed.
https://magicant.github.io/programmingmemo/coq/byhyp.html
ここに「前提が False の場合」の説明が載っている。
以下だと分かりやすいかも
Lemma f_test :forall A:Prop, A -> not A -> True.
Proof.
intros H H0 H1.
apply H1 in H0.
case H0.
Qed.
ありがとうございます。わかりました。
caseの対象がFalseになっていて、
コンストラクタがないため終了と。
■ このスレッドは過去ログ倉庫に格納されています
ニュース
- コロナワクチン接種後死亡で国を集団提訴 訴状では河野太郎大臣の「2億回打って死んでる人は1人もいない」発言に焦点 [Hitzeschleier★]
- 日経平均株価1200円安 イラン領内の爆発報道で急落… [BFU★]
- 【MLB】大谷翔平「英語力」格段向上の皮肉 水原容疑者の裏切りが副産物を生んだ [ネギうどん★]
- 水原一平容疑者、出身高校の『傑出した卒業生』から削除 [おっさん友の会★]
- コロナワクチン接種後死亡で国を集団提訴 訴状では河野太郎大臣の「2億回打って死んでる人は1人もいない」発言に焦点 ★2 [Hitzeschleier★]
- 早稲田大まで行ったのに 34歳で月収12万円の後悔 貯金もゼロで「自分は何をやってたんだ」 [PARADISE★]
- 【フジテレビ】2024 FORMULA 1【NEXT】Lap269
- とらせん
- 【DAZN】フォーミュラ 【F1 F2 F3 P】lap1430
- 【フジテレビ】2024 FORMULA 1【NEXT】Lap268
- 【DAZN】フォーミュラ 【F1 F2 F3 P】lap1429
- 【WOWOW】UEFAチャンピオンズリーグ・ヨーロッパリーグ 決勝トーナメント★22
- ○○マン←これに当てはまる言葉、タワマンしかない
- 【速報】自民党、Ｆａｃｅｂｏｏｋに全ての広告を停止するように命令 [207516352]
- 【悲報】いなり寿司誤認逮捕、闇が深すぎる… [207516352]
- 【悲報】大阪万博、ガス濃度測定を徹底しながら楽しまないといけない [115996789]
- 水原一平を非難しながら親の金でソシャゲのガチャ引いてるチー牛www
- ロードバイクが趣味