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
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 に説明がないのはそのへんが理由なのかもしれない。
仮の変数をいれる、と何回か書いたが、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 が挿入されているが、これは変数ではない。
[latest]