Hatena::ブログ(Diary)

 

2013-12-21

TPPmark 2013 の SSReflect による解答例と C85 新刊の宣伝

Theorem Prover Advent Calendar 2013 の21日目の記事です。

先月、信州大学TPP 2013 という定理証明器ユーザの集会がありました。TPP では毎回証明の問題が事前に出題され、参加者の一部がこれを解いてきて発表するようになっています。これが TPPmark です。この記事は、TPPmark 2013 の SSReflect による解答例とその解説です。問題はhttp://shirodanuki.cs.shinshu-u.ac.jp/TPP/TPPmark2013_Jap.pdfを参照してください。

これ以降の証明では以下のモジュールを使います。

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype path fingraph
               finset fingroup perm.

15パズルの形式化をしましょう。ボード上に配置されるコマは空白部分含め4*4=16通りで、ボードはそのコマの上の置換で表せます。

Definition elemt : finType :=
  prod_finType (ordinal_finType 4) (ordinal_finType 4).
Definition board : baseFinGroupType := perm_of_finGroupType elemt.

空白部分はボードの4隅であればどこでも良いはずです。元の問題との対応関係を考えると x, y の組で表せるコマに対して y*4+x+1 をその数と思いたいので、3, 3を空白部分としましょう。

Definition empty_space : elemt := (@Ordinal 4 3 erefl, @Ordinal 4 3 erefl).

次に、15パズルのボードを取って次の状態として正しいボードの集合を計算する関数 puzzle_next を書きます。

Definition truncord {m} n : 'I_m.+1 :=
  @Ordinal m.+1 (minn m n) (eq_ind_r _ (geq_minl m n) (ltnS (minn m n) m)).

Definition puzzle_next (b : board) : {set board} :=
  let (ex, ey) := b^-1%g empty_space in
  [set (tperm npos (ex, ey) * b)%g |
    npos : elemt &
    (npos \in [:: (truncord ex.-1, ey); (truncord ex.+1, ey);
                  (ex, truncord ey.-1); (ex, truncord ey.+1)]) &&
    (npos != (ex, ey))].

_^-1%g は群の逆元を意味します。b empty_space と書くと「置換 b の empty_space の位置に何があるか」の意味になりますが、b^-1%g empty_space と書くと「置換 b のどこに empty_space があるか」の意味になります。なぜそうなるかはここでは説明しません。let の後では、上下左右の4つの移動を列挙して次の状態の集合を作っています。

上の定義と fingraph.connect を使うと、到達可能性の定義は簡単です。

Definition reachable := connect (fun b1 b2 => b2 \in puzzle_next b1).

これで目的の定理のステートメントを記述するのに必要な定義は揃いました。すぐに証明を始めたいところですが、証明は状態遷移が何かしらの不変量を保存することの証明から始まります。なので先に不変量を定義しましょう。

Definition invariant (b : board) : bool :=
  let (ex, ey) := b^-1%g empty_space in odd_perm b (+) odd ex (+) odd ey.

状態遷移が不変量を保存することを証明してみましょう。

Lemma next_invariant b1 b2 :
  b2 \in puzzle_next b1 -> invariant b1 = invariant b2.
Proof.
  rewrite /puzzle_next /invariant.
1 subgoals, subgoal 1 (ID 87)
  
  b1 : board
  b2 : board
  ============================
   b2
     \in (let (ex, ey) := (b1^-1)%g empty_space in
          [set (tperm npos (ex, ey) * b1)%g
             | npos in [set npos in [:: (truncord ex.-1, ey);
                                        (truncord ex.+1, ey);
                                        (ex, truncord ey.-1);
                                        (ex, truncord ey.+1)] | 
           npos != (ex, ey)]]) ->
   (let (ex, ey) := (b1^-1)%g empty_space in b1 (+) odd ex (+) odd ey) =
   (let (ex, ey) := (b2^-1)%g empty_space in b2 (+) odd ex (+) odd ey)

imsetP と inE を使いたいところですが let が邪魔でできません。まずはこの let を消しましょう。

  move: {1 3 4}((b1^-1)%g _) (erefl ((b1^-1)%g empty_space)) => /= [b1x b1y] Hb.
1 subgoals, subgoal 1 (ID 106)
  
  b1 : board
  b2 : board
  b1x : 'I_4
  b1y : 'I_4
  Hb : (b1x, b1y) = (b1^-1)%g empty_space
  ============================
   b2
     \in [set (tperm npos (b1x, b1y) * b1)%g
            | npos in [set npos in [:: (truncord b1x.-1, b1y);
                                       (truncord b1x.+1, b1y);
                                       (b1x, truncord b1y.-1);
                                       (b1x, truncord b1y.+1)] | 
          npos != (b1x, b1y)]] ->
   b1 (+) odd b1x (+) odd b1y =
   (let (ex, ey) := (b2^-1)%g empty_space in b2 (+) odd ex (+) odd ey)

imsetP と inE を使います。

  case/imsetP => npos; rewrite !inE; case/andP.
1 subgoals, subgoal 1 (ID 322)
  
  b1 : board
  b2 : board
  b1x : 'I_4
  b1y : 'I_4
  Hb : (b1x, b1y) = (b1^-1)%g empty_space
  npos : elemt
  ============================
   [|| npos == (truncord b1x.-1, b1y), npos == (truncord b1x.+1, b1y),
       npos == (b1x, truncord b1y.-1)
     | npos == (b1x, truncord b1y.+1)] ->
   npos != (b1x, b1y) ->
   b2 = (tperm npos (b1x, b1y) * b1)%g ->
   b1 (+) odd b1x (+) odd b1y =
   (let (ex, ey) := (b2^-1)%g empty_space in b2 (+) odd ex (+) odd ey)

ここまでくればあとは場合分けと rewrite だけでできます。

  by do !case/orP;
    move/eqP => -> H ->; rewrite invMg tpermV permM -{}Hb tpermR odd_mul_tperm;
    move: H; rewrite !eqE /= eqxx 1?andbT /=;
    (move: b1x => [] [| [| [| []]]] //= _ _; [| |]) ||
    (move: b1y => [] [| [| [| []]]] //= _ _; [| |]); case: odd_perm; case: odd.
Qed.

次は、ボード b1 からボード b2 へ到達可能であれば不変量を保存することを証明しましょう。これは、connectP を使うと残りはパスに関する帰納法で証明できます。

Lemma reachable_invariant b1 b2 :
  reachable b1 b2 -> invariant b1 = invariant b2.
Proof.
  rewrite /reachable; case/connectP => ps H ?; subst b2.
  elim: ps b1 H => //= b2 ps IH b1;
    case/andP; move/next_invariant => ->; apply IH.
Qed.

最後に、14, 15を入れ替えただけのボードと全部のコマが整列したボードの間で上で定義した不変量が異なることを使って、一方からもう一方へ到達できないことを証明します。

Theorem tperm_unsolvable :
  ~~ reachable
    (tperm (@Ordinal 4 1 erefl, @Ordinal 4 3 erefl)
           (@Ordinal 4 2 erefl, @Ordinal 4 3 erefl)) 1%g.
Proof.
  apply/negP; move/reachable_invariant; move/eqP; apply/negP.
  by rewrite /invariant tpermV tpermD // odd_tperm invg1 perm1 odd_perm1.
Qed.

これで目的の定理が証明できました。この証明は合計53行で、TPP 当日までに出た解の中では最短でした。

ところで、この問題を見るとボードのサイズが4*4でない場合に対しても同じような性質を証明したくなるはずです。コミックマーケット85で Tsukuba Coq Users’ Group というサークルで頒布予定の「Coq による定理証明 2013.12」ではより一般的なケースに対する証明について解説しています。ここで詳細に解説しなかった事項についてもなるべく書くようにしているので、この記事を読んで良く分からなかったという方も是非読んでみてください。

2012-12-28

コミックマーケット83に参加します

サークル名
Stricter.org
日時・場所
3日目 東 Y-18a

Coq の本2種類と型推論の本を頒布します。

2012-08-08

コミックマーケット82に参加します

サークル名
Stricter.org
日時・場所
2日目 西 し-31a

Coq 本と型推論の本を頒布します。

2012-05-12

Git で .git ディレクトリ無しに特定のコミットの中身を展開する

git-archive コマンドで特定のコミットの tar ファイルを作れるので、それを展開すれば良いらしい。

2012-04-04

シェルスクリプトでSSHの接続を使い回す

完全なまとめがみつからなかったので、まとめておく。ControlMaster を使います。

REMHOST=localhost
ssh -S ~/.ssh/master-$$ $REMHOST -M -f -N 2>/dev/null 1>&2
ssh -S ~/.ssh/master-$$ $REMHOST hostname
ssh -S ~/.ssh/master-$$ $REMHOST uname
ssh -S ~/.ssh/master-$$ $REMHOST who
ssh -S ~/.ssh/master-$$ $REMHOST -O exit 1>/dev/null 2>/dev/null

こんな感じで書けます。最初のsshコマンドで接続を作って、最後ので破棄しています。

scpの呼び出しも、

scp -o ControlPath=~/.ssh/master-$$ file $REMHOST:.

という風に書けます。