迷路の試験問題を解いてみた - にわとり小屋でのプログラミング

参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ

[dot_h2o2]

プログラミング,証明

[katzchang]

あとでみよう。

[agw]

これはすごい。

[tarao]

これが真のLv4 すばらしい！

[h-hirai]

はい、分かりません。