https://gist.github.com/971586色々と工夫してみた。ロボットと指令の定義。これは前と同じ。 Inductive Robo : Set := Blue | Orange. Inductive Order : Set := order : Robo -> Z -> Order. Definition robo_inv (robo: Robo) := match robo with | Blue…

微妙に使いにくいじゃないですか。ssreflectを読んでたら、こういうのを簡単に Leibniz equality にする方法が分かったので書いてみた。https://gist.github.com/971135まず、ZP = Z * positive の上に普通に同値関係を定義する ZP_eq : ZP -> ZP -> Prop。…

起きたらすでに残り14時間とかどこかおかしい。A問題はこんなかんじ 青と橙のロボットがいます。ロボットを動かして指令通りの順番でボタンを押させます。指令は「O 2, B 1, B 2, O 4」のようにどのロボットがどのボタンを押すかの列で与えられます。各ロボ…

メモ sqlite3 /home/aps/aps/aps-server/db/production.sqlite3 'SELECT file FROM answers' | ruby -e 'puts $<.read.scan(/\w+/)'

http://as305.dyndns.org/aps/ サブミットのしかた。 DefinitionsがあるときはDefinitions.vに保存してコンパイルTheoremをTheorems.vに保存。Proof.〜Admitted.の間を埋めて証明できたら、Admitted. をQed. にしてファイルを送信 問題の作成 http://as305.d…

ちまちまと進めてたんだけど、だいたいきれいになってきたので公開http://github.com/kik/TaraiTermination元にした証明は http://d.hatena.ne.jp/kururu_goedel/20100719Coq庵 http://atnd.org/events/6022 でちょっと解説する予定。参考資料 http://www.km…

下に書いたのから、よく考えたらおかしいところを直して、option Z とかいらないじゃんとか思い直した。ここに最新のが置いてある。http://github.com/kik/sandbox/blob/master/coq/tarai.v

http://d.hatena.ne.jp/kururu_goedel/20100702これを見て、とりあえず綺麗に書き直そうとしてみたら一日かかった。 しかし、これで一般たらいまわしへの道も見えてきたかも？ここに置いた。http://github.com/kik/sandbox/blob/master/coq/tarai.v多少、解…

http://d.hatena.ne.jp/m-hiyama/20100629/1277774676 を証明してみた。とりあえず、問題設定 Axiom A : Set. Axiom A_eq_dec: forall a b: A, { a = b } + { a <> b }. Axiom A_mul : A -> A -> A. Axiom A_zero: A. Axiom A_one: A. Infix "*" := A_mul. N…

はhttp://github.com/kik/sandbox/blob/f41bc1346d4491f937b3fb78da38a07c746acf1c/coq/ivt.vにあります。試すにはcoqを適当にインストールしてcoqideを起動して、このファイルを開く。 あとはツールバーから適当に下に進むボタンを押してれば証明の様子が分…

久しぶりにCoqで遊ぼうかと思って、いい問題はないかと考えたところ、ハノイの塔あたりが面白いんじゃなかろうかということで証明してみた。証明したいことはハノイの塔を完成させる最短手数は2^n-1であること…と思って少し書いてみたんだけど、これはかなり…

Require Import ZArith. Open Scope Z_scope. Goal forall t:Z, t = 1 + t^2 -> t^7 = t. intros. ring [H].終わらない…

http://as305.dyndns.org/wiki/index.php?Coq

なんかいろんな言語で FizzBuzz が書かれているようなので、Coq でも書いてみる。Coq の FizzBuzz は他のとは一味違う！なんとプログラムが正しく動くことが証明できるのだ！とりあえず、書いたプログラム Require Import Arith. Require Import List. (* Fi…

δ-reduction δ-reduction は変数をその定義で置き換える。まず何か定義して、 Coq < Definition hoge := fun x:nat => 2+x. hoge is definedcbvを実行してみる。 Coq < Eval cbv delta [hoge] in (hoge 3). = (fun x : nat => 2 + x) 3 : natこの場合は「hog…

change term ゴールとtermが変換可能なときに、ゴールをtermで置き換える tacic。simpl とかを適当に使った結果、やりすぎていらんとこまで置き換えてしまった場合とか、逆に何をどう使えばもっと簡単に置き換えることができるのか分からない場合に使うとよ…

assert form ゴールを直接の証明が簡単には書けないので、とりあえず簡単に証明できる中間結果を教えるtactic。 ringとかomegaで一発で証明するには複雑すぎるときに、問題を二つに分けるとよいことがある。中間結果 form を指定すると、サブゴールにformが…

Coq in a Hurryの練習問題の一番最後。 とすると であるから、となる正の整数の組のなかで、最小のをとってくる。 すると、であるから。これは矛盾であり２の平方根が有理数でないことの証明になっている。 この証明をCoqを使って書け。 これはとてつもなく…

assumption この tactic は忘れてもよい。仮定の中に結論と一致しているものがある場合に使うと一発で証明が終わる。でも、auto を使えば同じことができる。 intro この tactic はチュートリアルで普通に理解できる以上の機能はない。 結論が「forall x:T, U…

Coqでの証明はtacticと呼ばれるコマンドを並べて次々に実行ことによって行われる。 このtacticの語彙が多いほど証明の記述は楽になる。 しかし、語彙を増やすようなドキュメントはオンラインに見つからないので、書きやすいところから書いてみる。 exact ter…

Coqにおける等号は「Leibniz Equality」というもので、 (forall P: Prop, P x -> P y) <-> x = y.つまり「任意の命題に関して、同じ結論を与えるなら二つは等しい」というのが等しいの定義らしい。等しくないことを示すにはどうすればよいかというと、結果が…

メイドさんに教わったCoqというものをマニュアルと格闘しながら理解したつもり。 Variables A B : PropA と B は命題だよ。 Theorem mp : (A->B)->A->B. auto. Qed.modus ponens ぐらいは自動で証明できるよ。 Variable p : A->B. Variable a : A.なぜか知ら…