天泣記

| あみだくじの停止性を証明してください。
|
| つまり、あみだくじの上端のどれかから、あみだくじのルールで辿っていったら、必ず下端のどれかにたどり着くこと（無限ループに陥ってしまわないこと）を証明してください。
|
| 斜めの枝や、枝と枝の交差は認めるものとします。他の条件は、常識的な感じで。

無限ループにならないのは、以下のように説明できる。

一般に、決定的な状態遷移機械で、行き止まりに到達する状態遷移列は、同じ状態を含まない。これは、同じ状態を 2つ以上含む状態遷移列はその部分を繰り返すため、行き止まりに到達しないからである。

あみだくじをたどる規則を考えると、あみだくじを逆にたどることは決定的に可能である。なので、あみだくじを逆にたどる決定的な状態遷移機械を考える。そうすると、そのような状態遷移機械が行き止まりに到達する (上端に到達する) のであれば、その状態遷移列は同じ状態を複数含むことはなく、無限ループにはならない。

というわけで、上端から (順方向に) たどれる経路は、無限ループを含まない。

せっかくなので、「決定的な状態遷移機械で、行き止まりに到達する状態遷移列は、同じ状態を含まない」ということを Coq で証明してみた。 (あみだくじがもとになっているので、いろいろとあみだくじっぽい名前を使っているが、面倒なのでそのまま)

From mathcomp Require Import all_ssreflect.

Section amida_kuji.

Variable segment : eqType.

Definition path := seq segment.

(* 次の状態を求める関数。関数なので決定的。next x の返値が Some y というのが x から y に遷移することを表現する。None は行き止まり。 *)
Variable next : segment -> option segment.

(* 状態列で、隣り合う要素 x, y が next x = Some y になっているという述語。空の場合はどちらでもいいはずだが、とりあえず valid としている。たぶんこっちのほうが証明の手間が少し減る。 *)
Definition valid_path (p : path) : bool :=
  match p with
  | nil => true
  | seg1 :: rest =>
      all id (pairmap (fun x y => next x == Some y) seg1 rest)
  end.

Lemma valid_path_cons (seg : segment) (p : path) : valid_path (seg :: p) -> valid_path p.
Proof.
  case: p.
    by [].
  simpl.
  by move=> seg2 p /andP [].
Qed.

Lemma no_cycle seg0 p : valid_path (seg0 :: p) -> next (last seg0 p) = None -> uniq (seg0 :: p).
Proof.
  elim: p seg0.
    by [].
  move=> seg1 p IH seg0 Hv Hnl.
  specialize (IH seg1 (valid_path_cons _ _ Hv) Hnl).
  rewrite cons_uniq IH andbT.
  apply/negP => Hin.
  move: Hv => /= /andP [/eqP Hns0 Hv].
  move: Hin; rewrite in_cons => /orP [/eqP H01|].
    subst seg0.
    case: p => [|seg2 p] in Hnl IH Hv Hns0.
      suff: None = Some seg1; first by [].
      by rewrite -Hnl -Hns0.
    have {Hv Hns0 Hnl} H12: seg1 = seg2.
      move: Hv => /= /andP [] Hns1 _.
      move: Hns1.
      by rewrite Hns0 => /eqP [].
    subst seg2.
    by rewrite /= mem_head in IH.
  move: (seg1) => dummy.
  move/nthP => /(_ dummy) [] i.
  change (i < size p) with (i.+1 < size (seg1 ::  p)).
  change (nth dummy p i = seg0) with (nth dummy (seg1 :: p) i.+1 = seg0).
  rewrite leq_eqVlt => /orP [/eqP [Hi] Hns1|Hi2 Hsi1 {Hnl}].
    suff: None = Some seg1; first by [].
    by rewrite -{}Hnl -{}Hns0 -[in RHS]Hns1 Hi nth_last.
  have {Hsi1 Hv} Hsi2 : nth dummy (seg1 :: p) i.+2 = seg1.
    rewrite /= ltnS in Hi2.
    move: Hv => /all_nthP.
    rewrite size_pairmap => /(_ true i.+1 Hi2).
    rewrite (nth_pairmap dummy); last by [].
    by rewrite Hsi1 Hns0 => /eqP [] /= <-.
  have Hi1 : 0 < size (seg1 :: p).
    by [].
  move: (nth_uniq dummy Hi1 Hi2 IH).
  rewrite Hsi2 /=.
  by rewrite eq_refl.
Qed.

End amida_kuji.

About no_cycle.
(*
no_cycle :
forall (segment : eqType) (next : segment -> option segment) (seg0 : segment) (p : seq segment),
valid_path segment next (seg0 :: p) -> next (last seg0 p) = None -> uniq (seg0 :: p)
*)

no_cycle という定理がサイクルを期待される性質を証明したもので、

no_cycle seg0 p : valid_path (seg0 :: p) -> next (last seg0 p) = None -> uniq (seg0 :: p)

seg0 と p で要素が 1個以上の状態遷移列を表現している。最初の状態が seg0 で、以降の状態の列が p である。

その状態遷移列が valid である (隣り合う要素 x, y が next x = Some y となっている)、そして、最後の要素の次の要素がない (next (last seg0 p) = None) ならば、その状態列に同じ要素は含まれていない (uniq (seg0 :: p)) ということを示している。

なお、最初は、あみだくじを構築していく (横線をひとつずつ加えていく) ときにパスがどう変化するかぜんぶ書くという地道な方法で挑戦したのだが、あまりに面倒なのであきらめてしまった。

天泣記

2025-03-05 (Wed)

2025-03-06 (Thu)

2025-03-07 (Fri)

2025-03-18 (Tue)

2025-03-20 (Thu)