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

A. Flat CPO

Definition task :=
  forall (x y : option nat) (n : nat),
    x = Some n -> x = y \/ x = None -> x = y.

x = y \/ x = None について場合分けするのが簡単です。x = y の場合は自明で、x = None の場合はもう一つの仮定 x = Some n と合わせると矛盾が出ます。

Require Import Problem.

Theorem solution : task.
Proof.
  unfold task.
  intros x y n H [H' | H'].
  - exact H'.
  - rewrite H in H'; discriminate H'.
Qed.

x を destruct する方が素直に思いつく方法かもしれません。どちらでも使う tactic はだいたい同じです。

問題の由来

x <= y を x = y \/ x = None で定義すると option nat に順序が入ります。この順序構造は flat CPO と呼ばれるものです（プログラム意味論で出てきます）。この問題は、flat CPO の性質「x が最小元でないならその上界は x 自身に限る」を示せという問題でした。

B. If zero were not nat

Fixpoint plus n m :=
  match n with
  | O => S m                    (* O = One *)
  | S n' => S (plus n' m)
  end.

Definition task := forall x y, plus x y <> y.

nat のコンストラクタ O がもし 0 ではなく 1 (One) を表すとしたら、足し算に単位元がないことを示してくださいという問題です。

いくつか方針が考えられます。

forall x y, plus x (S y) = S (plus x y) を示しておくと、二重帰納法が回ります。
forall x y, plus x y = x + y + 1 のように標準の + を使った式に書き換える補題を用意すると、標準ライブラリの定理などが使えます。
主張を強めて forall x y, plus x y > y とすると、x についての帰納法が回ります。

最後の方針だと以下のように証明できます。

Require Import Problem Lia.

Theorem solution: task.
Proof.
  intros x y.
  cut (plus x y > y).
  - lia.
  - induction x.
    + auto.
    + simpl; auto.
Qed.

C. Perfect Square?

Definition task :=
  exists f : nat -> bool,
  forall n, (f n = true) <-> exists m, n = m * m.

与えられた自然数が平方数かどうかを判定する関数を書き、その正しさを証明してくださいという問題です。

計算量については何も要求がないので、m の候補を有限個に絞って全部試せばよいです。例えば n 以下の数をすべて調べれば十分です。以下、この方針での解法を説明します。（NArith を import して N.sqrt とかを使ったほうが楽かもしれません）

まず、一般に k 以下の自然数を全部試す関数は以下のように実装できます。

Require Import Arith.

Fixpoint check k n :=
  if k * k =? n then true else 
    match k with
    | 0 => false
    | S k' => check k' n
    end.

これに対して次の補題が証明できます。

Lemma check_spec :
  forall k n, check k n = true <-> exists m, m <= k /\ n = m * m.

次に task の証明を考えます。まず exists (fun n => check n n). としてから上の補題を使えば、証明すべきことは

(exists m, m <= n /\ n = m * m) <-> (exists m, n = m * m)

になります。これは自分で証明してもそんなに大変ではありませんが、firstorder nia とすると自動で証明してくれます。

D. Eat the Candies

Definition piles := (nat * nat * nat)%type.

Inductive take2 : piles -> piles -> Prop :=
| Take12 p q r : take2 (S p, S q, r) (p, q, r)
| Take13 p q r : take2 (S p, q, S r) (p, q, r)
| Take23 p q r : take2 (p, S q, S r) (p, q, r).

Inductive take_all : piles -> Prop :=
| Takeall_empty : take_all (0, 0, 0)
| Takeall_step c c' : take2 c c' -> take_all c' -> take_all c.

Definition task :=
  exists f : nat -> nat -> bool,
    forall p q r, f (p + q + r) (max p (max q r)) = true <-> take_all (p, q, r).

問題概要

飴の山が三つあります（山は空である場合もあります）。空でない山が二つ以上ある限り、次のことを何度でも行うことができます。

空でない山を二つ選び、それぞれから一つずつ飴を取って食べる。（同じ山から二つ取ることはできない）

山に含まれる飴の個数を p, q, r とします。全部の飴を食べることができるかどうかを判定する関数を書き、その正しさを証明してください。ただし、判定関数には p, q, r そのものではなく、それらの和と最大値のみが与えられます。（p, q, r そのものを与えると全探索で判定できてしまうのでこのような問題設定にしてみました）

必要十分条件

二つずつ食べるので、飴の合計数が偶数であることが必要です。また合計が偶数の場合をいくつか実際に試してみると、一つの山に飴が偏っていなければ可能であることが推測できます。これを手がかりにして、可能かどうかの境界がどうなっているかを調べれば必要十分条件を発見することができるでしょう。

とりあえず p, q, r がわかっているとすると、「p + q + r が偶数かつ p, q, r の最大値が残りの二数の和以下」が必要十分条件になります。後半を「最大値の二倍が全体の和以下」と言い換えることで和と最大値だけを用いて表せる条件になります。

まずはこの条件を判定して bool 型の値を返す関数を書く必要がありますが、これは Nat.even と Nat.leb を使えばできます。この条件を P と呼ぶことにします。

十分性

P が成り立っているときにすべての飴を食べきれる戦略を与えればよいです。戦略を与えるときには p, q, r がわかっているとしてよいことに注意してください。直感的には飴の個数の偏りが少ないほうが P が成り立ちやすいので、偏りを減らすように選ぶのが最適であると推測できます。

そこで、残っている飴の個数が多い山を優先的に選ぶ戦略を考えます。この戦略のもとで、初期状態が P を満たしていればその後も P が成り立ち続けることが示せます。飴の数は単調に減少するので、p + q + r についての帰納法で十分性が証明できます。

証明をする際には andb_true_iff, Nat.leb_le, Nat.even_spec などの補題と lia tactic が有用です。

必要性

take_all c の導出についての帰納法で示せます。一ステップ戻ったときに飴の数の総和は2増えるのに対して最大値は増えても1だけなので不等式が成り立ち続けることが（数学的には）証明の要点ですが、bool を Prop に変換してやればそのあたりはあまり自分で考えなくても lia で証明が終わると思います。