TopProver Sprint Round 10 - 論理とか計算機とか数学とか

A. Swap Twice

Definition swap (t : nat * nat) :=
  match t with (a, b) => (b, a) end.

Definition task := forall t, swap (swap t) = t.

組を左右を入れ替える関数 swap が定義されていて、それを二回やると元に戻ることを示せという問題です。

t が必ず (a, b) の形に書けることを考えるとあたりまえっぽくて、t を (a, b) の形に分解してやればよいです（そのままですが）。これは destruct でできます。

Require Import Problem.

Theorem solution : task.
Proof.
  unfold task.
  intro t.
  destruct t.
  simpl.
  reflexivity.
Qed.

intro してから destruct してますが、intros (a, b) と書いてもいいです。

B. Drinker paradox?

Definition task :=
  forall P : bool -> bool, exists a, P a = true -> forall x, P x = true.

古典一階述語論理で証明できるけど直感に反する論理式として知られているものです。一般の形では Coq で証明できませんが、P : bool -> bool にしてあるので証明できます。

P のありうる値は 4 通りあります（厳密には外延的に等価なものを除いて 4 通りですが、この問題では気にしなくていいです）。P true = true かつ P false = false のときは a = false であればよく、それ以外のときは a = true であればよいです。

あとは場合分けをするだけですが、単純に destruct (P true) などとするとうまくいきません。対処方法はいくつかありますが、分かりやすいのは

forall b : bool, b = true \/ b = false.

のような補題を証明して、これを利用して場合分けをする方針でしょう。

他には destruct eqn を使う手もあります。以下にこちらを使った例を示します。

Theorem solution : task.
Proof.
  unfold task.
  intro P.
  destruct (P true) eqn: Pt.
  - destruct (P false) eqn: Pf.
    + exists true.
      intros _.
      intro b; destruct b.
      * assumption.
      * assumption.
    + exists false.
      rewrite Pf.
      intro f_eq_t.
      discriminate f_eq_t.
  - exists true.
    rewrite Pt.
    intro f_eq_t.
    discriminate f_eq_t.
Qed.

C. Upper triangular (soundness)

(*
                       j
   -------------------->
  | 0  1  3  6  10  ...
  |    2  4  7  11  ...
  |       5  8  12  ...
  |          9  13  ...
  |             14  ...
  |
i V

*)

Inductive visit : nat -> nat -> Prop :=
| visit_first : visit 0 0
| visit_down : forall i j, i < j -> visit i j -> visit (S i) j
| visit_right : forall i j, i >= j -> visit i j -> visit 0 (S j).

Definition task := forall i j, visit i j -> i <= j.

図のような順にマスを踏んでいくとき、(i, j) が踏まれることと i <= j が同値になりますが、次の問題と合わせてこれを証明します。(i, j) が踏まれるなら i <= j を示すのがこちらの問題です。

visit i j についての帰納法を使い、残った細かい不等式などの証明を lia で処理するのが一番簡単です。

Require Import Problem Lia.

Theorem solution : task.
Proof.
  unfold task.
  intros i j H.
  induction H.
  - auto.
  - auto.
  - lia.
Qed.

i か j についての帰納法でもできます。その場合には途中で inversion が必要です。

D. Upper triangular (completeness)

Inductive visit : nat -> nat -> Prop :=
| visit_first : visit 0 0
| visit_down : forall i j, i < j -> visit i j -> visit (S i) j
| visit_right : forall i j, i >= j -> visit i j -> visit 0 (S j).

Definition task := forall i j, i <= j -> visit i j.

C の逆です。こちらはよく考えないと帰納法が回らなくて難しいです。

結論から言うと、変数の順番を入れ替えて j, i の順で二重帰納法をするとうまくいきます。これは各マスがどの順番で踏まれるかを考えると納得しやすいでしょう。図を見れば「j の小さいものが先に踏まれる」「j が同じ二つのマスは i の小さいものが先に踏まれる」ということがわかります。このことから (i, j) たちは j を優先する辞書式順序で小さい順に踏まれるのだから、これに合った帰納法を使えば証明できそうだと予想できます。つまり、外側で j についての帰納法、内側で i についての帰納法をすればよいということです。

順番を入れ替えるには一旦 intro してから revert で内側にしたい変数を戻します。

Require Import Problem Lia.

Theorem solution : task.
Proof.
  intros i j.
  revert i.
  induction j.
  - induction i.
    + constructor.
    + lia.
  - induction i.
    + econstructor; eauto.
    + constructor; [ easy | ].
      apply IHi; lia.
Qed.

E. Infinite duplication

Require Import Arith.

CoInductive stream :=
| SCons : nat -> stream -> stream.

CoFixpoint gen m n :=
  SCons m (if m <? n then gen (S m) n else gen 0 (S n)).

Fixpoint Snth n s :=
  match n with
  | 0 => match s with SCons h _ => h end
  | S n' => match s with SCons _ s' => Snth n' s' end
  end.

(* Show that each natural number occurs infinitely often in [gen 0 0]. *)
Definition task :=
  forall x, forall y, exists z, y <= z /\ Snth z (gen 0 0) = x.

C, D と同じ状況で踏んだマスの i 座標を順番に並べた無限列を考え、すべての自然数が無限回現れることを示せという問題です。gen i j はマス (i, j) から始めたときにできる無限列になります。

C, D で出てきた visit に何ステップ目で踏むかを表す引数を追加したものを考えます。マス (i, j) に k が書き込まれていることと visit i j k が成り立つことが同値です。

Inductive visit : nat -> nat -> nat -> Prop :=
| visit_first : visit 0 0 0
| visit_right : forall i j, i < j -> forall k, visit i j k -> visit (S i) j (S k)
| visit_down : forall i j, i >= j -> forall k, visit i j k -> visit 0 (S j) (S k).

D とほぼ同様にして次のような補題が証明できます。

Lemma le_visit : forall i j, i <= j -> exists k, visit i j k.

そうすると、直観的には visit i j k のとき gen 0 0 の先頭 k 個を取り除いた列が gen i j になりそうです。それを表すために、指定した個数の要素を取り除く関数を書きます。

Fixpoint Sskipn n s :=
  match n with
  | 0 => s
  | S n' => match s with SCons _ s' => Sskipn n' s' end
  end.

ちょっとした補題を準備すると次のことが証明できます。

Lemma visit_skip : forall i j k, visit i j k -> Sskipn k (gen 0 0) = gen i j.

これを使って task が証明できます。与えられた x, y に対し visit x (x + y) z となる z の存在が le_visit からいえて、この z に対して y <= z /\ Snth z (gen 0 0) = x であることが示せます。y <= z を示すには一般に visit i j k -> j <= k であることをいっておけばよく、これは難しくありません。

writer 解はこちらにあります。gen の定義に CoInductive が使われてますが、有限個の要素しか見ていないので残念ながら余帰納法の出番はありません。