一週間かかりました。
この問題は本当に難しいです。場合分けが多いし、リストの反転は難しいし、最小値であることの証明は当然大変です。
- bool のリスト ps が与えられる
- 以下の操作を繰り返す
- ps を任意の位置で前半の qs と後半 rs に分割して
- qs の true/false を反転して
- qs の逆順にして
- qs と rs を連結して新しい ps とする
- ps がすべて true になるまでに必要な最小操作回数を計算せよ
(*
* 問題の定義
*)
Definition happiest (ps : list bool) : bool :=
forallb id ps.
Definition flip (ps : list bool) (n : nat) : list bool :=
let h := firstn n ps in
let t := skipn n ps in
rev (map negb h) ++ t.
Definition flips (ps : list bool) (ns : list nat) : list bool :=
fold_left flip ns ps.
Definition make_happiest (ps : list bool) (ns : list nat) : bool :=
happiest (flips ps ns).
Definition answer_spec (answer : list bool -> nat) :=
forall (ps : list bool),
(exists moves : list nat, make_happiest ps moves /\ length moves = answer ps) /\
(forall moves : list nat, make_happiest ps moves -> length moves >= answer ps).問題を定義するだけなら簡単ですね。
answer_spec answer を満たす answer 関数を頑張って作りましょう！
Fixpoint best_move (ps : list bool) : nat :=
match ps with
| nil => 0
| p :: ps =>
match ps with
| nil => 1
| q :: _ =>
if bool_dec_negb p q then
1 + best_move ps
else
1
end
end.これで最良の手が計算できます。リスト ps に対して、前半の長さが best_move ps になるように分割するのが最良です。
計算例は次のようになります。簡単ですね。
best_move [] = 0
best_move [true] = 1
best_move [false] = 1
best_move [true; true; ps] = 1 + best_move [true; ps]
best_move [false; false; ps] = 1 + best_move [false; ps]
best_move [true; false; ps] = 1
best_move [false; true; ps] = 1
最初の2つは実際には起きないので、都合のいい値を割り当てておきます。
残りの場合は、true/false が反転する位置を返します。
最小の操作数も計算します。
Fixpoint count (ps : list bool) : nat :=
match ps with
| nil => 0
| p :: ps =>
match ps with
| nil => 1
| q :: qs =>
if bool_dec_negb q p then
count ps
else
1 + count ps
end
end.
Definition answer (ps : list bool) : nat :=
count (ps ++ true :: nil) - 1.分岐の構造はさっきのと同じです。計算例は
count [] = 0
count [true] = 1
count [false] = 1
count [true; true; ps] = count [true; ps]
count [false; false; ps] = count [false; ps]
count [true; false; ps] = 1 + count [false; ps]
count [false; true; ps] = 1 + count [true; ps]
こっちは同じ bool 値が隣り合ってるところを1つに潰して、長さを計算するだけです。
最終的な答えは、後ろに true を付けてから、count を計算して、1を引きます。
countはanswerより性質がよいです。証明したい性質は
当たり前だ。
count ps = count (map negb ps)
当たり前だ？これは難しいぞ！
count ps = count (rev ps)
たまに結果が1ずれるよ！
count ps + count qs = count (ps ++ qs)
または
count ps + count qs = 1 + count (ps ++ qs)
ずれるのは、リストが両方とも非空で、psの末尾とqsの先頭が一致するときですね。
それに比べてcount (rev ps)はちょっとめんどくさいです。と思わせておいて、簡単な方法があります。
revと++をまとめて証明すると簡単になります。count (rev_append ps qs)を使いましょう。
rev_append ps qs = rev ps ++ qs
なので、たまに結果が1ずれます。ずれる条件は
Definition rev_app_decr (ps qs : list bool) : bool :=
match ps with
| nil => false
| p :: ps =>
match qs with
| nil => false
| q :: qs =>
if bool_dec_negb q p then
true
else
false
end
end.がtrueになる場合ですね。要するに、psとqsが両方とも非空で、先頭が一致するときです。
証明したいことは
Lemma rev_app_count:
forall (ps qs : list bool),
count ps + count qs =
if rev_app_decr ps qs then
1 + count (rev_append ps qs)
else
count (rev_append ps qs).になります。これはpsについての帰納法で簡単にできます。なぜかというと、psがp :: psの場合は
count (rev_append (p :: ps) qs) = count (rev_append ps (p :: qs))
になるので、帰納法の仮定が簡単に使えるからです。
一回の操作では、rev_append (map negb ps) qs)が行われるので、countはたまに1ずれます。ずれる条件は
Definition decr (ps qs : list bool) : Prop :=
match ps with
| nil => False
| p :: _ =>
match rev ps with
| nil => False
| q :: _ =>
match qs with
| nil => False
| r :: _ =>
p = q /\ p <> r
end
end
end.になります。両方が非空で、psの先頭と末尾が一致していて、qsの先頭と不一致の場合です。
というわけで、
Lemma decr_count:
forall ps qs,
decr ps qs ->
count (ps ++ qs) = 1 + count (rev_append (map negb ps) qs).answer psがゼロの場合は、psはすでにすべてtrueです。逆も成り立ちます。
Lemma answer_zero_happiest :
forall (ps : list bool),
answer ps = 0 <-> happiest ps.当たり前ですね。
一回の操作でanswerが2以上減ることはありません。
Lemma flip_answer_le:
forall (ps : list bool) (n : nat),
answer ps <= 1 + answer (flip ps n).これらにより、最小手数がanswerを下回ることはないことが分かります。
best_moveを行うと、answerがちょうど1減ります。
Lemma best_move_answer:
forall (ps : list bool),
happiest ps \/ answer ps - 1 = answer (flip ps (best_move ps)).この証明が一番難しいです。頑張りました。
あとはやるだけです。
Theorem answer_is_correct: answer_spec answer.