天泣記

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 に説明がないのはそのへんが理由なのかもしれない。

2023-12-24 (Sun)

#1 Coq/SSReflect の multiple views について

SSReflect の view というものがある。 move/v とか apply/v というやつである

これの使い方は apply/andP の andP のように reflect lemma を使うのが有名であるが (SSReflect の名前が Small Scale Reflection というのはここから来ている)、 reflect lemma 以外に、iff (<->) や普通の関数も扱える。 というか、関数以外は関数に変換して扱うので、ここでは関数だけを考える。

この view は複数つけることができる。 move/v1/v2/v3 とか apply/v1/v2/v3 とかである。 manual でもMultiple viewsに説明されている。

基本的には、v1, v2, v3 という順に view が適用されるという話なのだが、 この説明がどうもよくわからないので試して調べてみようという気になった。

なお、apply/v1/v2 とふたつの場合で、ゴールが equivalence (LHS = RHS) の場合は Interpreting equivalencesにあるように、 v1 が LHS, v2 が RHS に適用されるという特別な動作になるが、今はこれは考えないことにする。

apply/v1/v2/v3. と apply/v1; apply/v2; apply/v3. の違いは、 前者で view が principal goal にしか適用されないが、 後者は各 view で生成されるすべての goal に適用されることだ、と manual に書いてある。

manual に例がなくてつらいので、試してみよう。 問題は、principal goal とはなにか、という点であるが、 すべてではないのだから、どうせ最初か最後のどちらかだろう。

From mathcomp Require Import all_ssreflect.

Section S1.
Variable P Q R A B : Prop.
Variable PQ2R : P -> Q -> R.
Variable A2P : A -> P.
Variable B2Q : B -> Q.

Goal R.
Fail apply/PQ2R/A2P. (* Cannot apply view A2P *)
Fail apply/PQ2R; apply/A2P. (* Cannot apply view A2P *)
Fail apply/PQ2R; apply/B2Q. (* Cannot apply view B2Q *)
apply/PQ2R/B2Q.
(*
______________________________________(1/2)
P
______________________________________(2/2)
B
*)
Abort.

End S1.

どうやら、生成される最後のゴールを principal goal といい、apply/v1/v2/v3 のように複数の view を apply につけると、 ある view で複数のゴールが生成されると、その最後のゴールが、後続の view で処理されるようだ。

上の例だと、ゴール R に対して view PQ2R を適用すると P と Q というゴールが生成され、 その最後のゴール (principal goal) は Q である。 なので、apply/PQ2R/B2Q. というように、PQ2R の後に B2Q を書くことで、 PQ2R で生成される最後のゴールの Q をさらに B2Q で処理することができる。 その結果、PQ2R で生成される最初のゴールの P と、B2Q が生成した B というゴールが最後に残っている。

apply/v1/v2/v3 についてはわかった。manual に例がないのはつらいが、試せばわかる程度には記述されていることがわかった。

さて、move/v1/v2/v3 と、move/v1; move/v2; move/v3 の違いはなんだろうか。 manual には、書いてないように思える。

move=> /v1; move=> /v2. と move=> /v1 - /v2. が同じである、とは書いてある。 同じにするために NO-OP intro pattern である - を使える、と書いてあるので、 使わなければ何か違うのだろう。

では、move=> /v1 - /v2. と move=> /v1 /v2. はどう違うのか、というと、これが書いてない。 また、move/v1/v2. とはどう違うのか、というもの書いてない。

書いてないだらけで manual の不備を疑うところであるが、 とりあえず試して探すと、以下の違いがあるようだ。(他に違いがないかどうかは知らない)

From mathcomp Require Import all_ssreflect.

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

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

Goal Q -> G.
Fail move/PQ2R/P2R2A.
(*
The command has indeed failed with message:
Illegal application (Non-functional construction):
The expression "P2R2A ?r" of type "A"
cannot be applied to the term
 "?y" : "?T"
*)

Fail move=> /PQ2R/P2R2A.
(*
The command has indeed failed with message:
Illegal application (Non-functional construction):
The expression "P2R2A ?r" of type "A"
cannot be applied to the term
 "?y" : "?T"
*)
move=> /PQ2R-/P2R2A. (* A -> G *)
exact A2G.
Qed.

End S2.

ここで、move/PQ2R/P2R2A. と move=> /PQ2R/P2R2A. は失敗するが、 move=> /PQ2R-/P2R2A. は成功している。 つまり、- の有無で失敗と成功の違いがある。

Q が top assumption のところに view PQ2R を使っているので、 P -> R が残って、P2R2A で P -> R が A に変わる、というのが期待した動作で、 move=> /PQ2R-/P2R2A. は実際にそう動いているが、 move/PQ2R/P2R2A. や move=> /PQ2R/P2R2A. はそうならずに失敗している。

ではなにが起きているかというと、後続の view は P -> R ではなく、R に対して動作するようだ。 move については、ここの R が principal goal ということだろうか。

From mathcomp Require Import all_ssreflect.

Section S3.
Variable P Q R A G : Prop.
Variable PQ2R : P -> Q -> R.

Variable R2A : R -> A.
Variable P2A2G : (P -> A) -> G.

Goal Q -> G.
move/PQ2R/R2A. (* (P -> A) -> G *)
Show Proof. (* (fun _view_subject_ : Q => ?Goal (fun p : P => R2A (PQ2R p _view_subject_))) *)
exact P2A2G.
Qed.

End S3.

top assumption に Q があるところで、move/PQ2R/R2A. とすると、 view PQ2R で top assumption の q : Q を PQ2R に与えるには、 第1引数の型は P で型があわないので仮の変数 p が導入され、 PQ2R p q : R という proof term ができ、 それに対して後続の view が動く、と理解した。 PQ2R p q の型は R なので、R2A : R -> A という view は適用できて R2A (PQ2R p q) となり、 そこで move/PQ2R/R2A. が終わるので仮の変数 p を受け取る関数でくるまれて (fun p : P => R2A (PQ2R p q)) となるということだろう。

そして、move=> /PQ2R-/P2R2A. と - をいれると、view P2R2A を適用する前にいったん終わって関数でくるまれるので P2R2A には P -> R の値が与えられて動作するということだろう。 たぶん。

% coqtop -v
The Coq Proof Assistant, version 8.17.0
compiled with OCaml 4.14.0


田中哲