作ってみた - 菊やんの雑記帳
http://as305.dyndns.org/aps/ サブミットのしかた。 DefinitionsがあるときはDefinitions.vに保存してコンパイル TheoremをTheorems.vに保存。Proof.〜Admitted.の間を埋めて証明できたら、Admitted. をQed. にしてファイルを送信 問題の作成 http://as305.dyndns.org/aps/problem_checker.tgz をダウンロード。exampleと同様にDefinisions.v, Theorem.v, Verify.v を作成。 check を実行して、成功したら各ファイルを送信。公理を足したいときは、checkの出力の最後の部分を少し編集して、Assumptionのとこに書く。
2010-07-04
http://d.hatena.ne.jp/kururu_goedel/20100702 これを見て、とりあえず綺麗に書き直そうとしてみたら一日かかった。 しかし、これで一般たらいまわしへの道も見えてきたかも？ ここに置いた。http://github.com/kik/sandbox/blob/master/coq/tarai.v 多少、解説 Fixpoint ntarai3 (n : nat) (a b c : option Z) := match a with | None => None | Some av => match b with | None => None | Some bv => if Z_le_dec av bv then b else match n with | 0%nat => None | S np => match c with | None => None
証明してみた。 - 菊やんの雑記帳
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. Notation "0" := A_zero. Notation "1" := A_one. Axiom A_mul_assoc: forall a b c, (a * b) * c = a * (b * c). Axiom A_mul_comm: forall a b, a * b = b * a. Axiom A_mul_1_r: forall a,
ハノイの塔 - 菊やんの雑記帳
久しぶりにCoqで遊ぼうかと思って、いい問題はないかと考えたところ、ハノイの塔あたりが面白いんじゃなかろうかということで証明してみた。 証明したいことはハノイの塔を完成させる最短手数は2^n-1であること… と思って少し書いてみたんだけど、これはかなり大変だということになって、ハノイの塔の解等を計算する関数が正しく解になっていることを証明することを最初の目標としてみた。 問題設定は以下の通り Inductive pos : Set := pos1 | pos2 | pos3. Inductive move : Set := | from_to (from to: pos): move. Definition tower := list pos. Definition moves := list move. Fixpoint single_tower (t: tower) (p: pos)
■ - 菊やんの雑記帳
δ-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この場合は「hoge」だけを展開する。 さらに「plus」も展開してみる。 Coq < Eval cbv delta [hoge plus] in (hoge 3). = (fun x : nat => (fix plus (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (p + m) end) 2 x) 3 : nat全部の定義
菊やんの雑記帳
TLE 2015 だった。 最初は 2/7 にやるよ！って書いてあったような気がするんだけど、いつのまにか 2/11 → 2/12 → 2/27 → 2/28 にどんどん延期されていってやばかった。そのせいか参加者少なすぎ。 問題一覧はここを見るとよい http://d.hatena.ne.jp/ku-ma-me/20150302 提出したコードはここ https://gist.github.com/kik/ba7f3ba6699932539913 Distinct Substrings やるだけ。どうやったら点数が変わるのか分からなかったので通しただけだったけど、98点あったので放置。どうやったら点数が減るのかが逆にわからない。たぶん、点数を最大化する方法をkinabaさんが解説してくれるんじゃないかな。 Find the GCD 5人しか通せてない。見たところみんなやり方が違って面白い
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
