Coqスレ

1 名前：デフォルトの名無しさん mailto:sage [2011/03/13(日) 21:05:23.37 ] こけこっこー coq.inria.fr/ 101 名前：デフォルトの名無しさん mailto:sage [2011/10/14(金) 23:09:59.10 ] >>githubの方は60さんに刺激を受けたfm forumの人がやってるやつで完全に二つは独立してるよ 102 名前：デフォルトの名無しさん [2011/10/15(土) 22:24:07.91 ] >>101 なるほど。ありがとうございます。見た感じ今はgithubの方が勢いがあるのかな？ 103 名前：デフォルトの名無しさん mailto:sage [2011/10/16(日) 10:55:36.52 ] >>101 実際は、60が10月から忙しくなったのでProofSummit で協力をよびかけて、賛同者の作業がやりやすいようGithubに移行したということです。60もGithubに参加しています。 104 名前：デフォルトの名無しさん mailto:sage [2011/10/16(日) 10:58:10.00 ] それは知らなかった説明ありがとう 105 名前：デフォルトの名無しさん mailto:さげ [2011/10/16(日) 12:24:15.43 ] >>103 うん？どういうこと？ 二つは独立しているのではなく、作業場所が変更したってこと？ 最新の作業情報はgithubのプロジェクトをみればよい？ 106 名前：60 mailto:sage [2011/10/16(日) 12:36:30.91 ] >>105 そういうことです。 Github のほうが真(新)です。 Wiki のほうは、その事がちゃんと分かるように直しておきます。 107 名前：デフォルトの名無しさん [2011/10/16(日) 22:06:31.22 ] >>106 わかりました。ありがとうございます。 108 名前：デフォルトの名無しさん mailto:sage [2011/10/17(月) 09:21:46.34 ] @n_k28 魔理沙気持ち悪かったです。もう二度とやらないで下さい＾＾ 109 名前：デフォルトの名無しさん mailto:sage [2011/10/27(木) 22:46:35.48 ] (P -> Q) -> (~P \/ Q) これの証明ができん。 110 名前：デフォルトの名無しさん mailto:sage [2011/10/27(木) 22:54:20.25 ] ああ ~~((P -> Q) -> (~P \/ Q)) なら証明できるのか。 直観主義論理がどうとか俺にはちんぷんかんぷんだ…。 111 名前：デフォルトの名無しさん mailto:sage [2011/10/30(日) 10:33:11.77 ] tauto.でおｋ 112 名前：デフォルトの名無しさん mailto:sage [2011/11/11(金) 16:16:46.14 ] Inductiveな型TからT_rectが生成される原理がどうしてもわからないなあ。 誰か教えてちょーだいな。 113 名前：デフォルトの名無しさん mailto:sage [2011/11/12(土) 05:51:58.15 ] #coq #inductive >>112 例えば nat_rectならFixpointでも定義できるよ。 Variable P : nat -> Type. Axiom fO : P O. Axiom fS : forall n, P n -> P (S n). Fixpoint nat_rect' n : P n := match n with | O => fO | S m => fS m (nat_rect' m) end. 114 名前：112 mailto:sage [2011/11/12(土) 12:04:00.72 ] nat_rectぐらいなら、数学的帰納法なんてなじみがあるからなんとなくわかるけど、 例えば Inductive sand (A B : Set) : Set := sconj : A -> B -> sand A B. から作られるsand_rectなんかは、 sand_rect = fun (A B : Set) (P : sand A B -> Type) (f : forall (a : A) (b : B), P (sconj A B a b)) (s : sand A B) => match s as s0 return (P s0) with | sconj x x0 => f x x0 end : forall (A B : Set) (P : sand A B -> Type), (forall (a : A) (b : B), P (sconj A B a b)) -> forall s : sand A B, P s となって、わかりそうなわからなそうな。上記のSetをPropにかえるともうお手上げ。 いったい何を理解すればいいのやら。どうか神様教えて。 115 名前：デフォルトの名無しさん mailto:sage [2011/11/12(土) 12:39:28.72 ] >>114 nat以外のものも構造的帰納法を表しているだけ。 X_rectのたぐいは自作する必要はないから、関数定義は理解できなくても 型だけわかれば、使えるからそれで いいと思う。 このX_rectがどのように自動生成されるか、Coqの内部のアルゴリズムが 知りたいならば少し勉強が必要かもしれないけれど、普通に使う分にはいらないでしょ。 116 名前：112 mailto:sage [2011/11/12(土) 16:10:50.99 ] >>115 ということは、構造的帰納法について、私が理解している以上に何か深いこと、 あるいは、もっと詳しいことがあるということでしょうか。論理式の定義に従って 帰納的に何かを証明するとか、そんなことは何の苦もなく理解してきましたけど、 上記>>114のsand_rectなんぞは、なぜそうなるのかいまひとつわからないのです。 また、sandの定義中のSetをPropにかえたものをpandとすると、pand_rectは sand_rectのSetをPropにかえただけのものとは異なります。ますますわかりません。 もし構造的帰納法について詳しく書かれた文献等あったらご紹介いただけないで しょうか。 117 名前：112 mailto:sage [2011/11/12(土) 20:54:41.74 ] 少しだけわかってきました。sand_rectの型の部分がそうなりそうな気もしてきました。 すると、本体（t:Tにおけるtのこと）がなぜそのように構成されるのか、という疑問に なりますが、それは半分は発見的経験的に考えないといけないのでしょうか。 また、pand_rectに関しては、sand_rectの(P : sand A B -> Type)の部分が なぜか(P : Type)になっている。つまりsand_rectにあるPはsand A Bを引数にとってたのに、 pand_rectにあるPはpand A Bを引数にとらなくなっている。 これさえ認めればsand_rectとpand_rectの違いは説明できます。これはなぜなんでしょう？ 118 名前：112 mailto:sage [2011/11/13(日) 09:55:45.41 ] 少しずつわかってくるにつれて、Coqとは直接関係ない気もしてきたのですが、 どなたか教えてくださるか、もしくは良い文献の紹介等していただけないで しょうか。 自然数の定義を例に話します。 （１）Oを自然数とする。 （２）nを自然数とするとき、S nも自然数とする。 （３）上記（１）（２）によって定められるもののみを自然数とする。 といった具合に自然数を定義することができますが、この（３）をどのように 形式的に表すかをもっと詳しく理解すれば、私の疑問が解けるような気がしてき ました。 どうか偉い方々、よろしくお願いいたします。 119 名前：デフォルトの名無しさん mailto:sage [2011/11/13(日) 15:44:37.16 ] Coq'Artの14章あたりにもある程度載ってるんだけども形式的な説明というわけでは無いね 論理や集合論の命題と型付きラムダ計算の式が1対1対応するっていう性質を使ってるってことは聞くけど 再帰型の定義が計算体系に及ぼす影響が対応する論理体系にどういう影響与えるかとか そういうのはよくわからない・・・ せいぜい構築子の無い型の値を仮定するのとFalseぶち込むのが対応してどちらも滅茶苦茶になるとか、そういうのぐらい ::=はiffに対応するとか|は排他論理和に対応するんだなぁというのは経験則でみえてくるけども 120 名前：デフォルトの名無しさん mailto:sage [2011/11/13(日) 19:01:45.89 ] ×型付きﾗﾑﾀﾞ計算の式 ○型付きﾗﾑﾀﾞ計算の型 121 名前：デフォルトの名無しさん mailto:sage [2011/11/19(土) 09:32:29.84 ] >>118 構造的帰納法に関しては俺はTAPLで勉強したな。あの本は丁寧で わかりやすい。 122 名前：112 mailto:sage [2011/11/21(月) 12:32:03.21 ] >>119-121 いろいろと情報提供ありがとうございます。いまはCoq'Artの14章で奮闘中です。もともと英語が苦手 なのですが、贅沢は言ってられません。TAPLって、Benjamin C. Pierceの「Types and Programming Languages」のことですよね。あたってみます。（砕けたりして。トホホ） 123 名前：デフォルトの名無しさん [2012/02/10(金) 07:07:56.25 ] proofcafe.org/sf/ に日本語訳を上げて下さっている方の書き込みがあったので、ここに書いておきます。 一部訳に打ち間違いがあります。どこに言ったら良いのかわからないので、ここに書いておきます。 proofcafe.org/sf/Poly_J.html の[マップ（Map）関数]のちょっと上に「理宇土」とあります多分「リスト」の誤変換だと思います。 この訳のお陰で大変楽して勉強できてます。ありがとうございます。 124 名前：デフォルトの名無しさん [2012/02/10(金) 09:10:05.55 ] proofcafe.org/sf/Poly_J.html の rememberタクティック のちょっと前に「なるべくintrosを使うタイミングを送らせ」の「送らせ」は「遅らせ」だと思います。 よろしくお願い致します。 訳ありがとうございます。 125 名前：デフォルトの名無しさん mailto:sage [2012/02/10(金) 09:35:05.24 ] 報告するならgithubのissue tracker https://github.com/sfja/sfja/issues か wikiの専用ページ www16.atwiki.jp/sf_j/pages/49.html でやるほうがいいと思うよ 126 名前：デフォルトの名無しさん [2012/02/10(金) 17:57:06.05 ] >125 ありがとうございます。そっちに書いときます。 127 名前：デフォルトの名無しさん mailto:sage [2012/02/11(土) 16:49:49.67 ] うわーはずかしいtypo。直しておきます。レポート感謝。 128 名前：デフォルトの名無しさん [2012/02/16(木) 10:19:23.91 ] 0 と 1 だけのタイプを作りたいと思い Inductive my : Type := O : my . my is defined my_rect is defined my_ind is defined my_rec is defined は上手く動作するのですが Coq < Reset my. Coq < Inductive my : Type := O : my | 1 : my . Toplevel input, characters 32-33: > Inductive my : Type := O : my | 1 : my . > ^ Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]). Coq < Inductive my : Type := O : my | (S O) : my . Toplevel input, characters 32-33: > Inductive my : Type := O : my | (S O) : my . > ^ Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]). となって上手く定義できません。どうやれば 0 と 1 だけのタイプを定義できるんでしょうか。 129 名前：デフォルトの名無しさん mailto:sage [2012/02/16(木) 13:24:10.57 ] Inductiveで列挙するのはコンストラクタの名前とその型。 値を並べられるわけではない。 130 名前：デフォルトの名無しさん mailto:sage [2012/02/16(木) 22:24:41.28 ] 1を名前に使えない Inductive my : Type := O : my | one : my . ならいい 131 名前：デフォルトの名無しさん mailto:sage [2012/02/18(土) 11:13:09.87 ] O(:nat)もコンストラクターなんじゃない？ 132 名前：デフォルトの名無しさん [2012/02/26(日) 23:56:37.37 ] なんか >>60 が変な扉を開いてしまったかもしれない。 「関数型ガール」 www16.atwiki.jp/sf_j/pages/56.html 133 名前：デフォルトの名無しさん [2012/03/09(金) 10:10:41.05 ] >129 >130 >131 >132 回答ありがとうございます。 134 名前：デフォルトの名無しさん [2012/03/09(金) 10:17:33.18 ] O を起点として O と (S O) だけの Typeとか O と (S O) と (S (S O)) だけの Type とか O と (S O) と (S (S O)) と (S (S (S O))) だけのTypeとか ... を作りたかったのですが、そうするにはどういうコマンド入れたら良いのでしょうか> レベル低い質問ですみません。 Inductive my : Type := O : my | S : my -> my. こうしちゃうと O と (S O)だけじゃなく (S (S O))も myタイプになってしまうのでどうしたらよいのかわかりません。 135 名前：デフォルトの名無しさん mailto:sage [2012/03/09(金) 10:57:54.37 ] >>134 証明を引数として取るコンストラクタを使うとか Require Import Arith. Inductive my (n:nat) : Set := | myO : my n | myS a : a <= n -> my n. Section my1. Let my1 := my 1. Definition my1_0 : my1 := myO 1. Program Definition my1_1 : my1 := myS _ 1 _. End my1. 136 名前：デフォルトの名無しさん mailto:sage [2012/03/09(金) 23:40:56.06 ] Inductive Fin : nat -> Type := | FinO n : Fin (S n) | FinS n : Fin n -> Fin (S n). というのをcoq-clubで見た。 137 名前：名無しさん [2012/03/15(木) 01:21:22.24 ] ネット務 138 名前：デフォルトの名無しさん [2012/03/20(火) 10:49:54.36 ] >>135 >>136 ありがとうございました。 またやってみます。 139 名前：デフォルトの名無しさん [2012/04/19(木) 09:20:01.83 ] Software Foumdationsの翻訳がとりあえず最後まで終わりました！ というわけでお願いなのですが、読んでください。 で、誤字脱字誤訳など指摘頂けると助かります。

---

---

[ 新着レスの取得/表示 (agate) ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef