2011年7月12日のブログ記事一覧-ウィリアムのいたずらの、まちあるき、たべあるき

Coqのお勉強　その５

2011-07-12 16:24:31 | Twitter

今日は、NII　トップエスイー教育センターでCoqのお勉強。

その内容　その５


■証明の仕方？（自分勝手にまとめたもの）

・まずは、intros 
　　　forallに出てくる変数
・simplする
・前に定義・証明したものを適用するには、rewrite その定義・証明
・単純に同じものになったらreflexivity



■割とよく使うテクニック
・SearchPattern：指定の型
   coqideの「Queries」→「Check」でチェック用のダイアログを出して、
   SearchPatternでパターン検索できる。

・SearchRewrite:等式に関する定理検索
   coqideの「Queries」→「Check」でチェック用のダイアログを出して行う

・標準ライブラリ
   http://coq.inria.fr/stdlib/
   Arithなど

・locate "記号"　：　記号に関するものを検索
 　locate "+" など
   coqideの「Queries」→「Check」でチェック用のダイアログを出して行う

・関数の定義を展開するunfold（逆はfold)

・再帰関数
　Functionコマンドを使う
　　　→Fixpointで定義できないようなもの
　Recdefをインポートすること
　measure length xsなどmasureを入れる

ランキングに参加中。クリックして応援お願いします！

Coqのお勉強　その４

2011-07-12 15:01:56 | そのほか

今日は、NII　トップエスイー教育センターでCoqのお勉強。
その内容　その４
いよいよ、証明！

■仕様記述のための論理演算子

・かつ
・または
・ならば ->
　（型とおなじ。内部的に同じ）
・任意の forall
・が存在する exists



■プルーフエディティングモード
・タクティックが使える
・Theoremで入るQedでぬける
・右上

Theorem first_theorem : forall p: Prop,p -> p.
Proof.
 intro p.  (* ｐという命題がある *)
 intro Hp. (* その命題は成り立っている *)
 apply Hp. (* そのHpを適用すると　：　右上のウィンドウで証明終わる）
Qed.       (* ぬける *)

とかやる
introとか、applyがタクティック
intros p Hp とかもできる



■等式の証明

relfexivity  右辺と左辺が同じ
rewrite　　　文字を書き換える
simpl　　　　計算する（simlpeではない。eがない）

【ここまでの例】

Theorem eql : forall x , 2 * x + 1 = 2 * x + 1.
Proof.
  intros x.
  reflexivity.
Qed.

Theorem eq2 : forall x y,(x=y)->(x+5=y+5).
Proof.
intros x y H.
rewrite H.
reflexivity.
Qed.

Theorem fact5 : fact 5 = 120.
Proof.
  simpl.
  reflexivity.
Qed.



■構造的帰納法

・inductionを使う

【例】

Theorem app_length : forall {A:Set} (xs ys : list A),
  length (xs ++ ys ) = length xs + length ys.
Proof.
  intros A xs ys.
  induction xs.
   simpl.
   reflexivity.

   simpl.
   rewrite IHxs.
   reflexivity.
Qed.

ランキングに参加中。クリックして応援お願いします！

Coqのお勉強　その３

2011-07-12 13:57:54 | そのほか

今日は、NII　トップエスイー教育センターでCoqのお勉強。
その内容　その３

■Inductiveデータ型
（ちょっと授業の内容だけだと難しいので、つけたし。

　整数って、
０，１，２，３，４，５・・・
ですよね。この定義として、

０は整数です。
add(0)は、１です。
add(add(0)は２です。
このように、addをかけていったものを整数と考える
こんな定義があります）

nat（整数）の型定義
Induction nat : Set :=
| O : nat
| S : nat -＞ nat.

こうすると、（ｓが上記のaddにあたる）表現できる

■再帰関数

・Definitionでなく、Fixpointを使う

Fixpoint fact n :=
match n with
|O => 1
|S n' => n * fact n'
end.


■list型を定義してみる・・・

Inductive list (A : Set) :=
| Nil : list A
| Cons : A -> list A -> list A.
 
とすると、Checkで
Cons nat 1(Cons nat 2(Cons nat 3(Nil nat)))

■Implicit Argument 
型引数の推定

Implicit Arguments Nil[A].
Implicit Arguments Cons[A].


とすると、Checkで

Cons 1(Cons 2(Cons 3(Nil)))

とかける

■中置演算子　：

Infix "::" := Cons(at level 60,right associativity).

とすると、Checkで

1::2::3::Nil

とかける

ランキングに参加中。クリックして応援お願いします！

Coqのお勉強　その２

2011-07-12 12:06:34 | そのほか

今日は、NII　トップエスイー教育センターでCoqのお勉強。
その内容　その２
いよいよ、いろいろ打っていきます。

■CoqIDE
・coqideを立ち上げる

・左側に書いていく。

　　(* コメントはこんなかんじ、括弧星で書く *)

　　Definition　変数 := 値とか、式とか.

　みたいなかんじで書く。最後にピリオド.が必要
　大文字で始まるのがVernacular（ばーなきゅらー）
　小文字はタクティック

・評価
　　↓　で一行１行評価していく。下の棒がついてる矢印で一気に評価


・計算してみたい
　　評価した後、メニューでQueries→Checkを選択すると、
　　下にウィンドウが出る。ここで以下のことなどができる
	Check
		型のチェック
	Print
		変数の定義を参照
	Eval compute in
		計算させる




■Extraction(CocIDE→coqc)

	Extraction Language Haskell.
	Extraction foo.

で右側のウィンドウにHaskellのコードがでる。
では、ファイルに保存するには？coq.ideではできない。
coqcを使う。

	Extraction Language Ocaml.
	Extraction "coq.ml" foo.

のように、"coq.ml"と指定。このファイルを保存する
保存したファイルをa.vとすると
(coqの拡張子は.vにするみたい）

今度、端末にいって、

coqc a.v

とうつと、coq.mlができる。

■coqtop
coqtop
と端末から打つと、インタラクティブ、IDEでやったことができる。
quit.
でぬける。保存はできない。



■４つの分類
　型
　プログラム
　命題
　証明：タクティックを使う

■Inductiveな型
・型か命題しか作れない

ランキングに参加中。クリックして応援お願いします！

Coqのお勉強　その１

2011-07-12 10:50:13 | そのほか

今日は、NII　トップエスイー教育センターでCoqのお勉強。
その内容　その１


■定理証明器
	１．自動定理証明器
		自動的に証明
		証明できる幅が狭い

	２．対話的定理証明器
		高階論理が扱える－強力
		でも人が証明する
		プログラムと連携：動作保障
		有名なもの（３つ？）：
			・Coq（こっく）
				タクティックに特徴
				Extractionによってプログラムに
			・Agda（あぐだ）
			・Isabelle（いざべる）
				コードジェネレーション

■Coq
	http://coq.inria.fr/
	プログラミング言語ではない
		関数を内部で記述→extractionでプログラム
		チューリング完全ではない
			停止しない関数を構築できない
			それ以外は関数型言語みたい
	最新は8.3pl2
		コア部分は変わっていないが
		インターフェースは変わってる

	Coqが使われているところ
		Java Card
		コンパイラの検証
		暗号アルゴリズム・通信プロトコル
		HadoopのMapReduceの検証
		IZE（あいず）Smart Desktop
		Webアプリの安全性
			SQLインジェクション
		twitterクライアント
		電卓アプリ
			http://proofcafe.co.cc/calcoq/

	テスト
		テストしたことしか保障しない

	Extractionの拡張
		Rubyやjavascriptとか
		Coq to Ruby,Coq to Scala

ランキングに参加中。クリックして応援お願いします！

Rで線形回帰分析

2011-07-12 06:34:45 | そのほか

方法

１．データを作成する
　　CSVファイルでデータをつくっておく

２．「ファイル」→「ディレクトリ変更」でCSVファイルのある
　　フォルダ（ディレクトリ）を指定

３．データを読み込む

　　データ＜-read.csv("読み込むCSVファイル",header=T)

(ヘッダがあるとき。＜は、本当は半角。以下同じ）

４．線形回帰分析　

　　結果＜－lm(目的変数~説明変数,data=３のデータ)

※重回帰分析で、説明変数がいくつもあるときは、
　　目的変数~説明変数１+説明変数２
　と足していく

５．結果表示
　　（１）内容を表示する
　　　　　summary(結果）

　　（２）散布図を描く
　　　　　plot(３のデータ$項目１,３のデータ$項目２）

　　（３）回帰直線
　　　　　abline（結果）

　　（４）残差分析
　　　　　plot（結果）

ランキングに参加中。クリックして応援お願いします！

記事一覧 | 画像一覧 | フォロワー一覧 | フォトチャンネル一覧