天泣記

2024-03-22 (Fri)

#1 Coq/SSReflect の bigop とシグマ (Σ) について

Coq/SSReflect には bigop というライブラリが入っていて、 総和の Σ などを表現できる。

\big[add/u]_(a <= i < b | P i) F i と書くと、 a 以上 b 未満の i について、P i が真になるものに限定して、F i を add する (u は単位元で、b < a なら結果は u になる)

「P i が真になるものに限定して」という条件を無視すれば、 学校で習ったシグマと同じである。 TeX で書くと \sum_{i=a}^{b} Fi である。

関数型言語的な表現としては、foldr, map, filter, index_iota で記述できる。 \big[add/u]_(a <= i < b | P i) F i = foldr add u (map F (filter P (index_iota a b))) である。 (index_iota a b は、a 以上 b 未満の自然数のリストを返す)

From mathcomp Require Import all_ssreflect.

Goal forall (T : Type) (add : T -> T -> T) u a b P F,
  \big[add/u]_(a <= i < b | P i) F i =
  foldr add u (map F (filter P (index_iota a b))).
  (* foldr add u [seq F i | i <- index_iota a b & P i] *)
Proof.
  move=> T add u a b P F.
  by rewrite foldrE big_map_id big_filter.
Qed.

ちなみに、上記は右辺を左辺に (foldr ... を \big ... に) 書き換えて証明しているが、 逆に左辺を右辺に書き換えて証明することもできなくはない。

Goal forall (T : Type) (add : T -> T -> T) u a b P F,
  \big[add/u]_(a <= i < b | P i) F i =
  foldr add u (map F (filter P (index_iota a b))).
  (* foldr add u [seq F i | i <- index_iota a b & P i] *)
Proof.
  move=> T add u a b P F.
  rewrite -big_filter.
  change (fun i : nat => BigBody i add true (F i)) with
    (fun i : nat => BigBody i add (predT (F i)) (F i)).
  by rewrite -big_map_id -foldrE.
Qed.

ここで、big_map_id は条件のところが P (F i) という形でないと (右から左に) 書き換えられないので、ゴールを change で変形している。 これはかなり面倒くさいので、foldr 側に変形してから証明するのは厄介であり、 \big 側で証明するのが無難だと思った。

さて、範囲を a <= i < b という形式で与えたので、index_iota a b が使われているが、 かわりに任意のリストを与えることもできて、それは \big[add/u]_(i <- r | P i) F i と書く。

Goal forall (T : Type) (add : T -> T -> T) u (r : seq T) P F,
  \big[add/u]_(i <- r | P i) F i =
  foldr add u (map F (filter P r)).
  (* foldr add u [seq F i | i <- r & P i] *)
Proof.
  move=> T add u r P F.
  by rewrite foldrE big_map_id big_filter.
Qed.

こうすれば index_iota は使わないことができるが、map と filter (相当) の機能は残っている。 map は数学のシグマでも相当する機能があるのでそういうものだろうが、filter はどうなのだろうか。 もちろん、filter に与える述語として、常に真を返す述語を与えれば、filter は無視できるのだが、 リストを与える形式であれば利用者側で filter を呼び出せるので、そもそも不要ともいえる。 なんでそんな機能を組み込んだのだろうか。

というわけで疑問は、なんで「P i が真になるものに限定して」という filter の機能が入っているのだろうか、ということである。 学校で習ったシグマにはそういう機能はなかったと思うのだが。

検索すると、bigop の論文が見つかった: Canonical Big Operators

しかし、filter の機能をつけたということは書いてあるが、なぜつけたのかは書いていないようだ。 ただ、例として \big[addn/0]_(i <= n | even i) i^2 というのを書いてあるので、連続した範囲でないものを扱いたいのだろうという気はする。

数学では、そういう書き方をするのだろうか。 Wikipedia:Summation をみると、 「一般化された記法がよく使われる (Generalizations of this notation are often used)」 と書いてある。 シグマの下に 0<=k<100, x∈S, d|n と書く例が出ている。 0<=k<100 や x∈S は、よくある書き方だと思う。 最後の d|n は、d が n を割り切る (n が d の倍数) という条件である。 これはちょっと見慣れないが、シグマの下には任意の命題を記述できて、その命題を成り立たせる値それぞれについて加算すると思えば、0<=k<100 や x∈S と同種の書き方と考えられるか。

あと、Wikipedia には、Concrete Mathematics: A Foundation for Computer Science に Chapter 2: Sums という章があるという脚注がある。 一章まるごと総和の話なのだろうか。

filter の機能が役に立つのか、ちょっと考えてみよう。 たとえば、同じ総和で、奇数という条件がついたものと、偶数という条件がついたものを加算すると、条件がついていない総和と等しくなるだろう。 証明してみよう。 なお、SSReflect が標準で提供しているのは偶数で真になる even じゃなくて、奇数で真になる odd なので、そっちを使う。

Goal forall a b F,
  \sum_(a <= i < b | odd i) F i +
  \sum_(a <= i < b | ~~ odd i) F i =
  \sum_(a <= i < b) F i.
Proof.
  move=> a b F.
  elim: b a.
    move=> a.
    by do 3 (rewrite big_geq; last by []).
  move=> b IH a.
  case: (boolP (a <= b)); last first.
    rewrite -ltnNge => ltn_ba.
    by do 3 (rewrite big_geq; last by []).
  move=> leq_ab.
  rewrite [\sum_(a <= i < b.+1 | odd i) F i](@big_cat_nat_idem _ _ _ _ _ _ b) => //; [|exact addnA|exact addnC].
  rewrite [in \sum_(b <= i < b.+1 | odd i) F i]/index_iota subSnn /=.
  rewrite [in \sum_(i <- [:: b] | odd i) F i]unlock /= addn0.
  rewrite [\sum_(a <= i < b.+1 | ~~ odd i) F i](@big_cat_nat_idem _ _ _ _ _ _ b) => //; [|exact addnA|exact addnC].
  rewrite [in \sum_(b <= i < b.+1 | ~~ odd i) F i]/index_iota subSnn /=.
  rewrite [in \sum_(i <- [:: b] | ~~ odd i) F i]unlock /= addn0.
  rewrite big_nat_recr /=; last by [].
  rewrite -IH.
  by case: (odd b) => /=; ring.
Qed.

うぅむ、予想外に面倒くさい。 そもそも、filter の条件の論理和に関する補題が見当たらないので、帰納法を使う必要があるし、IH を使えるようにする書き換えも面倒くさい。

でも、書き換えが面倒くさいのは、 a <= i < b という形で範囲を与えるからで、一般化してリストを与えればもっと簡単ではないか、ということでやりなおし。 (index_iota a b という特定の形のリストじゃなくて任意のリストを扱う、ということ)

Goal forall r F,
  \sum_(i <- r | odd i) F i +
  \sum_(i <- r | ~~ odd i) F i =
  \sum_(i <- r) F i.
Proof.
  move=> r F.
  elim: r.
    by rewrite 3!big_nil.
  move=> x r IH.
  rewrite 3!big_cons -IH.
  by case: (odd x) => /=; ring.
Qed.

お、簡単になった。

せっかくなので、対象を自然数に限定しない一般化をしてみよう。 fold に与える演算が associative, commutative でないといけないし、単位元も必要なので、 そういう証明がついている演算として、 T -> T -> T じゃなくて、Monoid.com_law idx を使う (idx が単位元である)

Goal forall (T : Type) (idx : T) (op : Monoid.com_law idx) (P : pred T) F r,
  op (\big[op/idx]_(j <- r | P j) F j)
     (\big[op/idx]_(j <- r | ~~ P j) F j) =
  \big[op/idx]_(j <- r) F j.
Proof.
  move=> T idx op P F.
  elim.
    rewrite 3!big_nil.
    by rewrite Monoid.mul1m.
  move=> x r IH.
  rewrite 3!big_cons -IH.
  case: (P x) => /=.
    by rewrite Monoid.mulmA.
  rewrite Monoid.mulmA.
  rewrite [op _ (F x)]Monoid.mulmC.
  by rewrite Monoid.mulmA.
Qed.

最後の部分は、ring を使えなくて、変形を自分でやる必要があった。 Monoid の場合の rewrite は Monoid.mulmA とかを使えるのだな。初めて使った。

P j と ~~ P j というのも具体的すぎるので、単に異なる述語 P, Q と一般化してみよう。 この場合、P j と Q j が両方とも真になると成り立たないので、 述語の intersection が空ということで、predI P Q =1 pred0 という前提を追加する。 これ以上の一般化は思いつかないので、big_filter_or と名前をつけることにする。

あと、何回も Monoid. と書くのは面倒くさいので Import しよう。

Import Monoid.

Lemma big_filter_or (T : Type) (idx : T) (op : Monoid.com_law idx) (P Q : pred T) F r:
  predI P Q =1 pred0 ->
  op (\big[op/idx]_(j <- r | P j) F j)
     (\big[op/idx]_(j <- r | Q j) F j) =
  \big[op/idx]_(j <- r | predU P Q j) F j.
Proof.
  move=> PQ0.
  elim: r.
    rewrite 3!big_nil.
    by rewrite mul1m.
  move=> x r IH.
  rewrite 3!big_cons -IH.
  move: (PQ0 x) => /=.
  case: (P x); case: (Q x) => //= _.
    by rewrite mulmA.
  by rewrite mulmA [op _ (F x)]mulmC mulmA.
Qed.

まぁ、ほぼ同じくらいの証明になった。Import したぶん短くなっているかな。

最後の部分は、P x と Q x の両方で場合分けするので、4種類になるのだが、 2種類は自明に証明されるので、手動でやらないといけないのは残り 2つで、 それらは P j と ~~ P j のときと同じ形だった。

big_filter_or を使って、最初の、奇数限定と偶数限定を足すと無条件になる、というのを証明してみる。

Goal forall a b F,
  \sum_(a <= i < b | odd i) F i +
  \sum_(a <= i < b | ~~ odd i) F i =
  \sum_(a <= i < b) F i.
Proof.
  move=> a b F.
  rewrite big_filter_or /=.
    under eq_bigl => x.
      rewrite orbN.
      over.
    by [].
  move=> x /=.
  by rewrite andbN.
Qed.

うまく証明できた。

証明の中で、 \sum_(a <= j < b | odd j || ~~ odd j) F j の中の odd j || ~~ odd j を書き換えるのに under tactic を使っている。

odd j || ~~ odd j を true に書き換えるのは orbN でいいのだが、 j はゴールの中で束縛されているので、そのままでは書き換えられない。

この場合は、under tactic を使うと 中身を書き換えられる。 (補題が必要になるので、ここでは eq_bigl を使っている) under tactic はサブゴールを作ってくれて、ユーザがサブゴールを書き換えた後に over とすると、書き換えた結果を元のゴールに反映してくれる。 サブゴールは証明しないというのがなかなか奇妙というか面白い。

under tactic には Interactive mode と One-liner mode があって、上は変形を見ながらやりたかったので Interactive mode を使っているが、 まぁ、変形は rewrite orbN だけなので、One-liner mode で十分で、そうすると以下のように書ける。

Goal forall a b F,
  \sum_(a <= i < b | odd i) F i +
  \sum_(a <= i < b | ~~ odd i) F i =
  \sum_(a <= i < b) F i.
Proof.
  move=> a b F.
  rewrite big_filter_or /=.
    by under eq_bigl => x do rewrite orbN.
  move=> x /=.
  by rewrite andbN.
Qed.

短くてよろしい。

なお、今回の場合は、under tactic を使わなくても、apply eq_bigl だけでも十分ではあった。

Goal forall a b F,
  \sum_(a <= i < b | odd i) F i +
  \sum_(a <= i < b | ~~ odd i) F i =
  \sum_(a <= i < b) F i.
Proof.
  move=> a b F.
  rewrite big_filter_or /=.
    apply eq_bigl => x /=.
    by rewrite orbN.
  move=> x /=.
  by rewrite andbN.
Qed.

under tactic が便利なのは、\sum みたいなのが、部分式に現れるときとか、 そのまま apply eq_bigl とはできないときかな。

Goal forall a b F,
  (\sum_(a <= i < b | odd i) F i +
   \sum_(a <= i < b | ~~ odd i) F i) + 3 =
  (\sum_(a <= i < b) F i) + 3.
Proof.
  move=> a b F.
  rewrite big_filter_or /=.
    by under eq_bigl => x do rewrite orbN.
  move=> x /=.
  by rewrite andbN.
Qed.

ここでは、+ 3 というのがついているので、apply eq_bigl はできなくて、 under eq_bigl を使っている。

2024-02-21 (Wed)

#1 Coq/SSReflect の eqP などの P の由来

SSReflect では、eqP, andP, leP, ifP とか、名前が P で終わる補題がいろいろ用意されている。 ifPn とか maxn_idPl とか、名前の途中に入っているものもあるが。

この P はなんの略なのか調べてみた。

mathcomp book には、 "The name of a reflection view always ends with a capital P." と書いてあるが、P がなんなのかはわからない。

まぁ、オリジナルを調べるか、ということで、 A computer-checked proof of the Four Color Theorem をみると、 "We prove such properties for all Boolean predicates that have a useful logical counterpart; for a predicate foob, the corresponding lemma is fooP." という記述が見つかった。

(SSReflect は、4色問題の証明を Coq で書く中で作られたライブラリが元になっているので、この論文の中で SSReflect の話が出てくるのである)

この記述からすると、properties の P かなぁ

bool を返す述語 foob に対して、その性質 (properties) を示す補題 fooP があるということですかね。

しかし、bool を返す述語が foob という名前というのは SSReflect ぽくないな。 むしろ、vanilla Coq ぽい

nat の比較関数 (nat -> nat -> bool) は vanilla Coq だと Nat.eqb で、 SSReflect だと eqn となっている。 (そして eqn に対応して eqnP がある)

4色問題の証明は GitHub に公開されているのでちょっとみてみるが、bool な述語が b で終わっている感じではない。 cfcontract.v だと、 contract_ctree に対して contract_ctreeP がある

foob というのは説明で bool を返すニュアンスを出したかったんですかね

2024-02-15 (Thu)

#1 Coq/SSReflect の reflection の利点

SSReflect では、Coq の述語 (命題を返す関数) と bool を返す判定関数を相互に変換する small scale reflection が多用される。 そもそも SSReflect という名前がこの機能に由来している。

で、この機能の利点をいろいろな文献がどう説明しているのか調べてみた。 Mathematical Components: Documentation からいろいろな文献がたどれるので、 SSReflect の紹介ぽいところで reflection の利点を述べているところを探してみた。 この機能は SSReflect の目玉機能なので、SSReflect の紹介をするところでなんらかの説明があるのである。

で、以下のような話が見つかった。

ポアンカレ原理というのは、ポアンカレがリーズニングよりも計算を用いるほうが証明が簡略化される、ということを言及していたらしい。 (1902年ということなので、たぶん「科学と仮説」だと思うけれど、確認していない。)

2024-02-12 (Mon)

#2 Coq の帰納型 (と余帰納型)

代数的データ型というのは ML や Haskell にあるやつで、型があって、コンストラクタがいくつかあって、というものだが、 よく似ているものとして、Coq の 帰納型 (Inductive type)余帰納型 (Coinductive type) がある。

帰納型と余帰納型はどちらも、型があって、コンストラクタがいくつかあって、というもので、 代数的データ型と同じなのだが、なにが違うのだろうか。 あるいは同じなのだろうか。

まぁ、帰納型と余帰納型というふたつがあるということで、 それぞれが代数的データ型のサブセットだろう、とは想像がつく

たぶん、帰納型は帰納法が使えるもので、余帰納型は余帰納法が使えるものなんじゃないかな、おそらく。 名前からしても。

帰納型は帰納法を使えるように、Positivity Condition とか条件がついているわけだし。

逆に、Miranda の代数的データ型は、(Miranda は Haskell と同じく lazy なので) big = Node 1 big big みたいな無限構造を作れるため、 帰納法はいつも使えるとは限らない。 (big の例は Miranda: A non-strict functional language with polymorphic types からとってきた)

#1 代数的データ型の「代数的」の由来

Wikipedia: Algebraic data typeには、 Algebraic data types were introduced in Hope, a small functional programming language developed in the 1970s at the University of Edinburgh. とある。 Hope という言語で導入されたようだ

しかし、Hope を調べても、データ構造のところで algebraic という語は出てこない

では、Haskell からたどるか

では Mirandaか、ということで以下を見ると、これっぽいな

Algebraic data types というのが出てきて、free algebra を宣言する機能とある。 free algebra というのは、law がなく、同じように作られたものだけが等しいということのようだ。 以下のように書いてある。

We call it a free algebra, because there are no associated laws, such as a law equating a tree with its mirror image.
Two trees are equal only if they are constructed in exactly the same way.

そして、Unfree algebras というのがその次に出てきて、free algebra に law を追加できるという機能が述べられている。 しかし、An Overview of Miranda によると、 この機能は初期のMirnadaにあったが、あまり使われず消されたとのこと。

2024-01-30 (Tue)

#1 UML state machine

Wikipedia の UML state machineには、 Extended statesという項目があって、 図で表現されない状態を変数として扱える、という話が書いてある

まぁ、素直な話だと思う。名前がついているのは良いですね、うん

UML 仕様を眺めてみる

おや、extended states という語は出てこない?

Extended finite-state machine という話があるようだ。 ここから来ているのかな。

2023-12-28 (Thu)

#1 Coq/SSReflect の multiple views について (補遺2)

仮の変数をいれる、と何回か書いたが、manual には top assumption が top のときに move/term が作る proof term は (term term1 ... termn top) と generalize される、 と書いてあって、挿入される term1 ... termn は必ずしも変数とは限らないようである。

変数でないものが入るのはどういうときか考えると、 何を入れるかという情報がどこかにないといけないので、 依存型とかだろうか。

PQ2R : P -> Q -> R の第1引数 P と第2引数 Q は対称、と書いたが、 第2引数の型 Q の中で第1引数を使うときは対称とはいえない。

たとえば、任意の型の値を受け取る foo : forall (T : Type), T -> P を考えて、これを view として使ってみよう。 (まぁ、これだと依存型とまではいえなくて、パラメタ型だけど。でも第2引数の型が第1引数の値なので、第1引数と第2引数は対称ではない。)

From mathcomp Require Import all_ssreflect.

Section S5.
Variable P G : Prop.
Variable foo : forall (T : Type), T -> P.
Variable P2G : P -> G.

Goal nat -> G.
move/foo.
Show Proof.
(* (fun _view_subject_ : nat => ?Goal (foo nat _view_subject_)) *)
exact P2G.
Qed.

End S5.

試してみると、foo nat _view_subject_ に foo nat _view_subject_ という部分ができていて、 top assumption の _view_subject_ が foo の第2引数に渡され、 その型の nat が第1引数に渡されていることがわかる。 つまり、nat が挿入されているが、これは変数ではない。

2023-12-27 (Wed)

#1 Coq/SSReflect の multiple views について (補遺)

top assumption として Q があるところに PQ2R : P -> Q -> R で move/PQ2R とするときに 仮の引数が導入されるのは PQ2R の第1引数が P であって、top assumption の Q とは型が異なるからである。 仮の引数が導入されると、それを受け取る関数抽象が必要になる。 関数抽象を作るというフェーズがあるので、後続の view をその前にやるか後にやるかという違いが出てくる。

では、top assumption が P ならどうか。 この場合は P が PQ2R の第1引数なので、そのまま関数適用でき、仮の引数を導入する必要は無く、関数抽象も必要ない。 後続の view を関数抽象を作る前後どちらにやるかという選択肢はそもそも存在しない。

From mathcomp Require Import all_ssreflect.

Section S4.
Variable P Q R A G : Prop.
Variable PQ2R : P -> Q -> R.
Variable P2R2A : (P -> R) -> A.
Variable Q2R2A : (Q -> R) -> A.
Variable R2A : R -> A.
Variable A2G : A -> G.

Goal P -> G.
move/PQ2R. (* (Q -> R) -> G *)
Abort.

Goal P -> G.
move/PQ2R/Q2R2A. (* A -> G *)
exact A2G.
Qed.

Goal P -> G.
move/PQ2R/R2A.
(*
Illegal application (Non-functional construction):
The expression "R2A ?r" of type "A" cannot be applied to the term
 "?y" : "?T"
*)

End S4.

というわけで、move/PQ2R/Q2R2A. がそのまま動く。

しかし、move/PQ2R/R2A. は逆に動かない。

PQ2R の principal goal は R である、といえるわけではないようだ。

しかし、PQ2R : P -> Q -> R の第1引数 P と第2引数 Q は対称というか、立ち位置としてたいして違いがあるものではないので、 これらの違いで動いたり動かなかったりというのは、よい挙動ではないように思える。 manual に説明がないのはそのへんが理由なのかもしれない。



田中哲