発表スライド: Coq ユーザが Lean を調べてみた
Debian で、昔ながらの (network-manager を使わない) ネットワークの設定は /etc/network/interfaces にいろいろ書くのだが、 その形式は manpage として interfaces(5) に書いてある。
が、OPTIONS PROVIDED BY OTHER PACKAGES のところに記載があるように、ifupdown ではない他のパッケージによって提供されているオプションもあって、そういうのはこのマニュアルには書いていない。
ここで、wpasupplicant が提供しているものを調べようと思って、マニュアルを眺めてみたが見つからず、 (Debian パッケージの) ソースをとってきたら wpasupplicant.README.Debian というファイルがあってそこに書いてあった。
/etc/network/interfaces に wpasupplicant の設定を行うのは Debian 独自のやりかたなのかな。
証明の場合分けが不必要に多かったので減らしてみた。 (他にもいくらか調整した。)
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.