Hatena::ブログ(Diary)

菊やんの雑記帳

2011-05-15 Google Code Jam 2011予選

[] A問題をやっと解けた。一週間もかかったよ 04:42  A問題をやっと解けた。一週間もかかったよ - 菊やんの雑記帳 を含むブックマーク

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 => Orange
| Orange => Blue
end.

移動命令の定義。ボタンを押すを移動から分離した。さらにどっちのロボットへの命令なのかを型にいれることにした。

Inductive Move (robo: Robo) : Set := Left | Right | Stay.
Inductive Moves : Set :=
| moves : Move Blue -> Move Orange -> Moves
| pushmove (roboPush: Robo) : Move (robo_inv roboPush) -> Moves.

型「Move Blue」は青ロボットの移動を値として持つ。各ロボットへの命令の組は両方移動するか、片方がボタンを押して残りが移動するだけなので、上の2つだけにした。pushmoveにボタンを押すロボットを指定すると移動するほうのロボットの移動しか渡せなくなるように型を付ける。

ロボットの座標の組の定義

Record ZZ : Set := zz {
  pB : Z;
  pO : Z
}.

(* 略 *)

Definition do_move (r: Robo) (m: Move r) (p: ZZ) :=
match m with
| Left  => paddz r p (-1)
| Stay  => p
| Right => paddz r p 1
end.

これによって、Move Blue型の値をdo_moveに渡すとBlueの座標が変化する。引数rは暗黙引数にできる。

ふたつのロボットを同時に動かす場合はこんな感じ。

Definition do_moves (mb: Move Blue) (mo: Move Orange) (p: ZZ) :=
  do_move mb (do_move mo p).

移動命令のリストが指令のリストに正しく則っているかの述語。「Correct pfrom pto os ms」は位置pfromから命令列msロボットを動かすと、指令列osの順にボタンを押して、最終的に位置ptoにくるという述語。

Inductive Correct (pfrom: ZZ) : ZZ -> list Order -> list Moves -> Prop :=
| c_nil:
    Correct pfrom pfrom nil nil
| c_moves (mb : Move Blue) (mo : Move Orange) os ms pto:
  Correct (do_moves mb mo pfrom) pto os ms ->
    Correct pfrom pto os (moves mb mo::ms)
| c_pushmove (r : Robo) (mv: Move (robo_inv r)) os ms pto:
  Correct (do_move mv pfrom) pto os ms ->
    Correct pfrom pto (order r (pfrom r)::os) (pushmove mv::ms).

この述語が真に成るのは次の場合のみ

  • ms=nilのときは、pfrom=ptoos=nilのとき
  • ms=moves mb mo::ms'のときは、pfromをmbとmoで動かした結果をpfrom'とすると、Correct pfrom' pto m's osが成立するとき
  • ms=pushmove r mv::ms'のときは、pfromをmvで動かした結果をpfrom'とする。さらにos=o::os'で、oはロボットrがpfrom rでボタンを押す命令であり、Correct pfrom' pto ms' os'も成立するとき

というように問題を整理しなおしたので、多少は証明が簡単にはなって、このあと700行ぐらいがんばった結果

minimum_moves : list Order -> list Moves.

という最小の移動リストを返す関数が完成して、

Example sample_2 :=
  order Orange 2::
  order Blue 1::
  order Blue 2::
  order Orange 4::
  nil.

Eval vm_compute in (minimum_moves  sample_2).

の結果

     = moves (Stay Blue) (Right Orange)
       :: pushmove (roboPush:=Orange) (Stay (robo_inv Orange))
          :: pushmove (roboPush:=Blue) (Right (robo_inv Blue))
             :: moves (Right Blue) (Right Orange)
                :: pushmove (roboPush:=Blue) (Stay (robo_inv Blue))
                   :: pushmove (roboPush:=Orange) (Stay (robo_inv Orange))
                      :: nil
     : list Moves

と、実際に動くプログラムが完成して、しかもこれが最短であることも証明できた。

2011-05-14 Coqで有理数 with Leibniz equality

[] 標準ライブラリ有理数って、Leibniz equalityじゃないから 05:05  標準ライブラリの有理数って、Leibniz equalityじゃないから - 菊やんの雑記帳 を含むブックマーク

微妙に使いにくいじゃないですか。ssreflectを読んでたら、こういうのを簡単に Leibniz equality にする方法が分かったので書いてみた。

https://gist.github.com/971135

まず、ZP = Z * positive の上に普通に同値関係を定義する ZP_eq : ZP -> ZP -> Prop。

次に、この同値関係で割ったときの代表元を返す関数を作る。canceled: ZP -> ZP。普通に約分しつくした形を代表元にする。

そして、魔法のような eq_irrelevance を証明する。

最後に ZP の部分集合 { x | canceled x = x } をQとする。これはもちろん代表元全体の集合だ。

仕上げに魔法のように Q_eq_dec を ZP_eq_Q_eq を証明する。

2011-05-09 Google Code Jam 2011予選

[] A問題が如何に難しかったか 21:33  A問題が如何に難しかったか - 菊やんの雑記帳 を含むブックマーク

起きたらすでに残り14時間とかどこかおかしい。

A問題はこんなかんじ

青と橙のロボットがいます。ロボットを動かして指令通りの順番でボタンを押させます。

指令は「O 2, B 1, B 2, O 4」のようにどのロボットがどのボタンを押すかの列で与えられます。

ロボットは最初に1の位置にいて、各々1ターンに「左右に一歩移動」「ボタンを押す」「何もしない」の行動ができます。

指令通りのボタンを押し終えるまで最短で何ターンかかるでしょう?ただしボタンを同時に押してはいけません

はいはいグリーディー。貪欲にやれば正解です。こんなのグリーディーにやる以外にないし、あまりに自明すぎて証明する必要も感じられません。しかし、今回は最近話題のCoqで解くことにしたので、こんな当たり前のことでも証明しないといけないのです。証明すればバグに悩むこともありません。

とりあえず、ロボットenumを作りましょう。命令はロボットと位置を表す整数のペアです。

Inductive Robo : Set := Blue | Orange.
Inductive Order : Set := order : Robo -> Z -> Order.

で、list Orderを受け取って最短手数を返す関数を書けばいいんですよ

(* 距離を計算してゆとりポイントを負にならないように引く *)
Definition yutori_minus (x y z: Z) := Zmax 0 (Zabs (x - y) - z).

Fixpoint minimum_aux (bp op bx ox: Z) (os: list Order) :=
match os with
| nil => 0
| order Blue bp'::os' =>
    let n := yutori_minus bp' bp bx + 1 in
    n + minumum_aux bp' op 0 (ox + n) os'
| order Orange op'::os' =>
    let n := yutori_minus op' op ox + 1 in
    n + minumum_aux bp op' (bx + n) 0 os'
end.

Definition minimum (os: list Order) := minimum_aux 1 1 0 0 os.

開始地点とゆとり引数と命令列を引数にとって、次にボタンを押すロボットは全力で押しに行って、その間もう一個のロボットは何かする代わりにゆとりポイントを貯めて、次にそのロボットを動かすときはゆとりポイントを消費するようにすればできあがり。

あとはこれが最小値を返してることを証明すれば終わり!こんな綺麗な再起呼び出ししかしてない関数の証明なんて簡単です!

2010-11-27 あなぷる統計

[] 人気のtaciticが知りたいという要望がでたので 15:02  人気のtaciticが知りたいという要望がでたので - 菊やんの雑記帳 を含むブックマーク

メモ

sqlite3 /home/aps/aps/aps-server/db/production.sqlite3 'SELECT file FROM answers' | ruby -e 'puts $<.read.scan(/\w+/)' <ans.txt | sort | uniq -c | sort -nr

ここから手作業でtacticだけ選ぶ。あと面白そうなのも残す

   1506 apply
   1272 auto
   1116 rewrite
   1016 destruct
    881 intros
    756 omega
    541 assert
    488 intro
    452 simpl
    424 exists
    345 unfold
    283 replace
    267 induction
    211 ring
    150 split
    130 case
    110 left
    108 right
    102 elim
     98 clear
     90 inversion
     88 False_ind
     82 generalize
     71 reflexivity
     67 specialize
     66 double
     65 exact
     58 trivial
     56 set
     50 repeat
     49 tauto
     49 remember
     49 assumption
     44 congruence
     39 cut
     37 contradict
     34 cbv
     33 absurd
     33 I
     32 ring_simplify
     32 contradiction
     31 Ltac
     29 symmetry
     27 pose
     25 discriminate
     25 compute
     23 fold
     22 field
     19 try
     19 eapply
     18 do
     18 change
     17 revert
     17 erewrite
     13 intuition
     13 constructor
     12 dependent
     11 subst
     11 edestruct
     10 transitivity
     10 exist
     10 compose
     10 complete
      9 fix
      8 injection
      8 idtac
      8 eauto
      8 case_eq
      7 well_founded
      7 prove_sup
      7 pattern
      7 elimtype
      5 red
      5 lazy
      5 equality
      5 decide
      2 setoid_replace
      2 fourier
      2 cofix
      1 field_simplify_eq
      1 eexists
      1 econstructor
      1 cutrewrite

2010-08-07 anarchy proof

[] 作ってみた 06:52  作ってみた - 菊やんの雑記帳 を含むブックマーク

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のとこに書く。