【Coq】コンピューターで証明しよう【コック】©2ch.net at MATH【Coq】コンピューターで証明しよう【コック】©2ch.net - 暇つぶし2ch■コピペモード□スレを通常表示□オプションモード□このｽﾚｯﾄﾞのURL■項目テキスト33:片山博文MZ ◆T6xkBnTXz7B0 15/01/27 20:27:34.17 SJxzPcnV >>24 聞いた覚えはないな 34:片山博文MZ ◆T6xkBnTXz7B0 15/01/27 20:35:45.19 SJxzPcnV >>30 「xは３の倍数である」 ⇔ ∃y∈Ｚに対して「x＝3y」、 だな。１階述語とexistsを使って解いてくれ。 35:片山博文MZ ◆T6xkBnTXz7B0 15/01/27 20:59:02.99 SJxzPcnV 例えば、 Definition trimul (n:nat) := exists m:nat, n = 3*m. と定義すればtrimul(0)は次のように証明できる。 Theorem tmzero: trimul(0). unfold trimul. exists 0. auto. Qed. 36:片山博文MZ ◆T6xkBnTXz7B0 15/01/27 21:17:44.23 SJxzPcnV >>30 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. 37:片山博文MZ ◆T6xkBnTXz7B0 15/01/27 21:25:18.31 SJxzPcnV 「Reset Initial.」コマンドでCoqを初期状態へ戻すことができる。 「unfold x.」はゴールにあるxをその定義に展開するタクティクだ。 「destruct H.」はHを崩すタクティク。 次ページ最新レス表示レスジャンプ類似スレ一覧スレッドの検索話題のニュースおまかせリストオプションしおりを挟むスレッドに書込スレッドの一覧暇つぶし2ch