ちょまど問題 https://twitter.com/chomado/status/479227070975725569 を形式化したけど間違ってるかも

chomado-problem.v

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype.
Require Import tuple finfun finset.

Definition answer := 10.-tuple 'I_ 4.

Definition compare(a0 a1 : answer) : nat :=
  count (fun x => fst x == snd x) (zip_tuple a0 a1).

CoInductive chomado :=
  | decided : answer -> chomado
  | ask : answer -> (nat -> chomado) -> chomado.

Definition run(a0:answer) :=
  fix run(c:chomado) (depth:nat) :=
  match c with
  | decided a1 => a0 == a1
  | ask a1 next =>
      if depth is depth'.+1 then
        run (next (compare a0 a1)) depth'
      else false
  end.

Definition success(c:chomado) (depth:nat) :=
  [forall a0, run a0 c depth].

(* 何らかの方法で実行可能 *)
Lemma solvable : exists c depth, success c depth.
Proof.
Abort.

(* 回数Nで実行可能 (例. N=20) *)
Lemma solvable20 : exists c, success c 20.
Proof.
Abort.

(* 最低回数はN (例. N=10) *)
Lemma min10 : forall n, (exists c, success c n) -> n <= 10.
Proof.
Abort.

(* 以下、4^{10}回でできることの証明 *)

Lemma same_compare10 : forall a, compare a a = 10.
Proof.
  rewrite /compare.
  move=> [a /=/eqP<-].
  elim: a; first done.
  move=> /= h l ->.
  by rewrite eq_refl.
Qed.

Lemma compare10_same : forall a0 a1, compare a0 a1 = 10 -> a0 = a1.
Proof.
  rewrite /compare.
  move=> [a0 H0] [a1 H1] /= H.
  suff: a0 = a1;
    first by
      move=> Heq; move: Heq H0 H1 => <- H0 H1;
      congr 1 Tuple;
      exact: bool_irrelevance.
  move: H0 H1 H => /eqP<- /eqP.
  elim: a0 a1; first by move=> a1 /size0nil-> _.
  move=> h0 t0 IH [|h1 t1] /=; first done.
  move=> [Hsz].
  case: (h0 =P h1).
  - move=> <- [Hih].
    by rewrite (IH _ Hsz Hih).
  - move=> _ /= H.
    change (count (fun x => x.1 == x.2) (zip t0 t1) = (size t0).+1) in H.
    have: count (fun x => x.1 == x.2) (zip t0 t1) <= size t0.
    - rewrite -(size1_zip(t:=t1)); last by rewrite Hsz.
      exact: count_size.
    - rewrite H.
      move=> /ltP Hlt.
      by case: (Lt.lt_irrefl _ Hlt).
Qed.

Definition something_to_say : answer := [tuple ord0 | _ < 10].

CoFixpoint chomado_simple' remaining :=
  if remaining is a0 :: remaining' then
    ask a0 (fun n =>
      if n == 10 then
        decided a0
      else
        chomado_simple' remaining'
    )
  else
    decided something_to_say.

Definition chomado_simple := chomado_simple' (enum [finType of answer]).

Definition chomado_simple_cost : nat := size (enum [finType of answer]).

Lemma chomado_simple_OK : success chomado_simple chomado_simple_cost.
Proof.
  rewrite /chomado_simple_cost /chomado_simple /success.
  apply/forallP => x.
  have: x \in enum [finType of answer].
  - by rewrite mem_enum.
  - elim: (enum [finType of answer]) => [|a0 remaining] /=; first done.
    rewrite in_cons => IH /orP[/eqP<- | H].
    - rewrite same_compare10 => /=.
      by case: (size remaining) => [|_] /=.
    - case: (compare x a0 =P 10).
      - move=> Heq; rewrite (compare10_same _ _ Heq).
        by case: (size remaining) => [|_] /=.
      - by move=> _; apply IH.
Qed.