証明の場合分けが不必要に多かったので減らしてみた。 (他にもいくらか調整した。)
From mathcomp Require Import all_ssreflect.
Section amida_kuji.
Variable segment : eqType.
Definition path := seq segment.
(* amida-kuji has determinstic function to obtain next segment *)
Variable next : segment -> option segment.
Definition valid_path (seg : segment) (p : path) : bool :=
all id (pairmap (fun x y => next x == Some y) seg p).
Lemma valid_path_cons (seg0 seg1 : segment) (p : path) :
valid_path seg0 (seg1 :: p) -> next seg0 = Some seg1 /\ valid_path seg1 p.
Proof.
by rewrite /valid_path /= => /andP [] => /eqP Hn Hv.
Qed.
Lemma next_nth (dummy seg x y : segment) (p : path) (i : nat):
valid_path seg p -> i < size p -> next x = Some y ->
nth dummy (seg :: p) i = x -> nth dummy (seg :: p) i.+1 = y.
Proof.
move=> Hv Hi Hxy Hni.
move: Hv => /all_nthP.
rewrite size_pairmap => /(_ true i Hi).
rewrite (nth_pairmap dummy); last by [].
by rewrite Hni Hxy => /eqP [] ->.
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.
move: (valid_path_cons seg0 seg1 p Hv) => [] Hns0 {}Hv.
specialize (IH seg1 Hv Hnl).
rewrite cons_uniq IH andbT.
apply/negP => Hin.
move: (seg1) => dummy.
move/nthP: Hin => /(_ dummy) [] i /=.
rewrite leq_eqVlt => /orP [].
rewrite eqSS => /eqP Hi.
rewrite Hi nth_last /= => Hl.
rewrite /= Hl in Hnl.
suff: None = Some seg1; first by [].
by rewrite -Hns0 -Hnl.
change (size p).+1 with (size (seg1 :: p)).
move=> Hi2 Hsi.
suff: 0 == i.+1; first by [].
have Hi1 : 0 < size (seg1 :: p).
by [].
rewrite -(nth_uniq dummy Hi1 Hi2 IH).
rewrite (next_nth dummy seg1 seg0 seg1 p i Hv Hi2 Hns0 Hsi) /=.
by rewrite eq_refl.
Qed.
End amida_kuji.@mame さんが PPL であみだくじの証明について問いかけていた。
| あみだくじの停止性を証明してください。 | | つまり、あみだくじの上端のどれかから、あみだくじのルールで辿っていったら、必ず下端のどれかにたどり着くこと（無限ループに陥ってしまわないこと）を証明してください。 | | 斜めの枝や、枝と枝の交差は認めるものとします。他の条件は、常識的な感じで。
無限ループにならないのは、以下のように説明できる。
一般に、決定的な状態遷移機械で、行き止まりに到達する状態遷移列は、同じ状態を含まない。 これは、同じ状態を 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)) ということを示している。
なお、最初は、あみだくじを構築していく (横線をひとつずつ加えていく) ときにパスがどう変化するかぜんぶ書くという 地道な方法で挑戦したのだが、あまりに面倒なのであきらめてしまった。
ちょっと深さ優先探索と幅優先探索を両方やる機会があって思ったのだが、 幅優先探索は遅いのは、幅がすごく大きくなるからかな
昨日の my_vector_caseS で Hn を noconf_nat_inv Hn noconf_nat に置き換えるのに noconf_natK という補題を使った。 そのために no confusion という準備が必要だった。
さらに置き換えた後に noconf_nat_inv Hn noconf_nat を展開して noconf_nat (f_equal predn Hn) にした。
でも、ここで Hn は n.+1 = n'.+1 という型なので、 両辺の先頭が S なのはすでに判明している。 なので、もっと直接的に noconf_nat (f_equal predn Hn) = Hn という補題を作れないだろうか。
もちろんこれは noconf_natK を等式の両辺が S のときの場合に限った命題なので、noconf_natK を使って簡単に証明できる。
Lemma eqprK_nat_S {m n : nat} (Hn : m.+1 = n.+1) : @noconf_nat m.+1 n.+1 (f_equal predn Hn) = Hn.
Proof.
change (noconf_nat_inv Hn noconf_nat = Hn).
by apply noconf_natK.
Defined.
ただ、noconf_natK を使わないで、直接的に証明できないだろうか。
ここで、この場合 (両辺が S の場合) noconf_nat は等式の両辺に S を適用するので、 結局 f_equal succn (f_equal predn H) = H となる。 これを証明できないか考えよう。
これが証明できれば、証明のときに Hn を noconf_nat_inv Hn noconf_nat にしてから展開するとか no confusion とか CPS を持ち出す必要もなくなる。
というわけで挑戦してみよう。
From mathcomp Require Import all_ssreflect.
Lemma eqprK_nat_S {m n : nat} (H : m.+1 = n.+1) :
@f_equal nat nat succn m.+1.-1 n.+1.-1 (@f_equal nat nat predn m.+1 n.+1 H) = H.
Proof.
ここで、H を場合分けして erefl に具体化できれば、証明は完了するはずであるが、以下のように destruct H は失敗する。
Fail destruct H. (* Abstracting over the terms "n0" and "H" leads to a term fun (n1 : nat) (H0 : m.+1 = n1) => @f_equal nat nat succn m.+1.-1 n1.-1 (@f_equal nat nat predn m.+1 n1 H0) = H0 which is ill-typed. Reason is: Illegal application: The term "@eq" of type "forall A : Type, A -> A -> Prop" cannot be applied to the terms "m.+1.-1.+1 = n1.-1.+1" : "Prop" "@f_equal nat nat succn m.+1.-1 n1.-1 (@f_equal nat nat predn m.+1 n1 H0)" : "m.+1.-1.+1 = n1.-1.+1" "H0" : "m.+1 = n1" The 3rd term has type "m.+1 = n1" which should be a subtype of "m.+1.-1.+1 = n1.-1.+1". *)
依存型エラーのときはだいたいそうだが、どういう項が作られてなぜエラーになっているのかわからない。 なので、自分で match を書いてやってみよう。
Fail refine
(match H as H' in _ = x return
@f_equal nat nat succn m.+1.-1 x.-1 (@f_equal nat nat predn m.+1 x H') = H'
with
| erefl => _
end).
(*
The command has indeed failed with message:
In environment
m, n : nat
H : m.+1 = n.+1
x : nat
H' : m.+1 = x
The term "H'" has type "m.+1 = x" while it is expected to have type "m.+1.-1.+1 = x.-1.+1".
*)
上のエラーでは "m.+1 = n1" と "m.+1.-1.+1 = n1.-1.+1" が異なる、というものだったが、 今回は "m.+1 = x" と "m.+1.-1.+1 = x.-1.+1" が異なる、となっていて、変数の名前は違うだけなので、たぶん destruct はこういう項を作っているのだろう。
これをみて考えると、return 節では n.+1 を x に置き換えているので、もともとは S n という形 (つまり 1 以上の自然数) の場合だけに限定されていた命題が 任意の自然数についての命題に変わっていて、0 の場合に型が壊れているのが問題と理解できる。
とすると、0 の場合も含めて型がつく命題である必要があるのではないか。 そして、no confusion はまさに 0 の場合も扱っているので、それで証明できるのだということがわかる。
しかしここでは no confusion を導入せずに証明したい。
ここでアイデアが思い浮かんだ。 0 の場合は扱っていないので、0 の場合は自明な命題になるようにしてしまえばいいのではないか。 ということで、以下のように変形する。 0 の場合は True にしてしまうのである。(ちなみに型がつけばなんでもよく、False でもよい)
refine
(match H as H' in _ = x return
match x with
| 0 => fun=> True
| n'.+1 => fun H' => @f_equal nat nat succn m.+1.-1 n'.+1.-1 (@f_equal nat nat predn m.+1 n'.+1 H') = H'
end H'
with
| erefl => _
end).
こうすると、ゴールは @f_equal nat nat succn m.+1.-1 m.+1.-1 (@f_equal nat nat predn m.+1 m.+1 erefl) = erefl になった。 H が erefl になったのでこれは計算を進められるようになり、reflexivity で証明できる。
ただ、refine を使う必要は無くて、ゴールをその形にしておけばよい。 (destruct はそのときのゴールを return 節にするため。)
change (match n.+1 with | 0 => fun=> True | n'.+1 => fun H => @f_equal nat nat succn m n' (@f_equal nat nat predn m.+1 n'.+1 H) = H end H).
これで destruct H が通って証明できた。
by destruct H.
試行錯誤を除いた最終的な証明を示しておく。 (あと、命題のところで .+1.-1 が出てくるのは無駄なので消しておいた。)
Lemma eqprK_nat_S {m n : nat} (H : m.+1 = n.+1) :
@f_equal nat nat succn m n (@f_equal nat nat predn m.+1 n.+1 H) = H.
Proof.
change
(match n.+1 with
| 0 => fun=> True
| n'.+1 => fun H => @f_equal nat nat succn m n' (@f_equal nat nat predn m.+1 n'.+1 H) = H
end H).
by destruct H.
Defined.