Coq項のHOASについてのチュートリアル
Tutorial on the HOAS for Coq terms
著: Enrico Tassi
訳: @suharahiromichi
Elpi は、Coq などのホストアプリケーションに組み込まれるライブラリとして提供される拡張言語です。
Elpi は、制約が強化された λProlog の派生です。λProlog は、束縛子（バインダ）を含む抽象構文ツリーを簡単に操作できるように設計されたプログラミング言語です。Elpi は、メタ変数 (ユニフィケーション変数、または Coqの項(term)では evar とも呼ばれます) を含む抽象構文ツリーを簡単に操作できるように設計されたプログラミング構造で λProlog を拡張したものです。
このソフトウェア「coq-elpi」は、Elpi を組み込み、拡張言語 Coq 固有のデータ型 (項など) と API (新しい誘導型を宣言するためなど) に公開する Coq プラグインです。
VSCode を使用して適切な構文強調表示を取得するには、「gares.coq-elpi-lang」拡張機能をインストールしてください。CoqIDE では、[編集] -> [設定] -> [色] で "coq-elpi" を選択してください。
このチュートリアルでは、Coq 内での Elpi の統合に焦点を当てています。特に、Coqの項が Elpi プログラムに公開される方法と、Coq API を呼び出す方法について説明します。
このチュートリアルは、読者が Elpi と HOAS に精通していることを前提としています。そうでない場合は、Elpi チュートリアルをご覧ください。
https://lpcic.github.io/coq-elpi/tutorial_elpi_lang.html
HOAS for Gallina
From elpi Require Import elpi. (* .none *)
Elpi Command tutorial_HOAS. (* .none *)
Coqの項の完全な構文は、coq-builtin.elpiにあります。コンテキストのエンコーディングと、Coq との対話に使用できる API の詳細なドキュメントが付属しています。このチュートリアルと、コマンドとタクティクスに焦点を当てた残り2つのチュートリアルは、そのすべてを穏やかに紹介するものです。
https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi`_ にあります。
quotations と antiquotations : つまり、Coq のネイティブ構文で項を記述できる構文機能については、後回しにします。 ここでは、Coqの項の抽象構文木に注目します。
globalコンストラクタ Constructor global
大域参照(global reference)のためのgrefデータ型から始めましょう。
type const constant -> gref.
type indt inductive -> gref.
type indc constructor -> gref.
constant、 inductive および constructorは、Elpi に対して不透明(opaque)な Coq 固有のデータ型です。それでも、 gref データ型を使用すると、これらの名前が何を指しているのか (定数、帰納型、コンストラクタ) を確認できます。
coq.locate API は文字列を gref にします。
Elpi Query lp:{{
coq.locate "nat" GRnat,
coq.locate "S" GRs,
coq.locate "plus" GRplus
}}.
Query assignments:
GRnat = indt «nat»
GRplus = const «Nat.add»
GRs = indc «S»
訳注：
Elpiの組込述語coq.locateは、第1引数に、Coqの定数、帰納型、コンストラクタの「名前」を与えると、第2引数にElpiの変数に代入する。Elpiの変数なので大文字ならなんでもよく、節から抜けるとアンバインドされる。
Elpi には、以下のconst、indt、indcのコンストラクタが定義されていて、それぞれ、Coq項の定数、帰納型、コンストラクタを Elpi の gref に変換する。
Elpi Query lp:{{
coq.locate "I" X, /* X = indt «I» */
coq.say X
}}.
indc «I»
Query assignments:
X = indc «I»
ELPIからは、Coq項の実体を自分で«»を使って書くことはできない。しかし、出力ウィンドウにはX = indt «I»のように表示されるのでそれにならって記述する場合がある。
訳注終り。
coq.env.* ファミリの API を使用すると、グローバル名を持つ適切に型指定された Coq項の環境にアクセスできます。
訳注： src/coq-builtin.elpi を参照のこと。以下の term は、Coqの型を示すものである。
-
pred coq.env.typeof i:gref, o:term.
-
pred coq.env.const i:constant, o:option term, o:term.
Definition x := 2.
Check x : nat.
Elpi Query lp:{{
coq.locate "x" GR, /* GR = const «x» */
/* all global references have a type */
/* GR の型が Ty に設定される。 */
coq.env.typeof GR Ty, /* Ty = global (indt «nat») */
/* destruct GR to obtain its constant part C */
/* const «x» = const C から */
GR = const C, /* C = «x» */
/* constants may have a body, do have a type */
/* 定数 «x» の値 S(S(O)) を取得する。 */
coq.env.const C (some Bo) TyC
}}.
Query assignments:
Bo = app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]
C = «x»
GR = const «x»
Ty = global (indt «nat»)
TyC = global (indt «nat»)
idnt «nat» のような式は、Coq項ではありません。
global term コンストラクターは gref を実際の termに変換します。
type global gref -> term.
訳注：
| ELPIの値 | ELPIの型 |
|---|---|
| «nat» | inductive |
| indt «nat» | gref |
| global (indt «nat») | term |
であって、Coq項に対応するのは、global型である。なので、global (indt «nat»)のがたちで、ELPIからCoqの項を扱えることになる。訳注終り。
app と fun コンストラクタ Constructors app and fun
app term コンストラクタは、term のリストを取り、N引数 (n-ary) の関数適用を構築します。最初の項は頭部で、残りは引数です。
たとえば、 app [global (indc «S»), global (indc «O»)]は 1 の表現です。
type app list term -> term.
束縛子（バインダ）に移りましょう！
Definition f := fun x : nat => x.
Elpi Query lp:{{
coq.locate "f" (const C), /* C = «f» */
coq.env.const C (some Bo) _
% Bo = fun `x` (global (indt «nat»)) (c0 \ c0)
}}.
Query assignments:
Bo = fun `x` (global (indt «nat»)) c0 \ c0
C = «f»
fun コンストラクタは、以下の三つを引数にとります。
- 清書されたヒント
x - 束縛変数の型
nat - 本体を記述する関数
訳注： Boの値は、定数"f"の値で、λx.xである。次に説明があるように、コンストラクタfunの第3引数には、λPrologの関数c0 \ c0が渡される。
type fun name -> term -> (term -> term) -> term.
note: name は清書するためだけのものです:Coq の世界では値を持っていますが、Elpi には (unit型のように) 内容がありません。
name の Elpi 項は、 ````` (バッククォート) で囲まれた単なる識別子です。
次の例の foo と bar がそれにあたる。
Elpi Query lp:{{
fun `foo` T B = fun `bar` T B % names don't matter
}}.
Query assignments:
B = X0
T = X1
coq.name-suffix などの API を使用すると、1から始まる名前のファミリを作成できます。たとえば、coq.name-suffix `H` 1 Nは NにH1を設定します。
Elpi Query lp:{{
coq.name-suffix `H` 1 H
}}.
fixとmatch コンストラクタ
他のバインダ prod (Coq の forall、別名 Π) と let は似ています。ここではむしろ fix に焦点を当てましょう。
Elpi Query lp:{{
coq.locate "plus" (const C), /* C = «Nat.add» */
coq.env.const C (some Bo) _
}}.
Query assignments:
Bo = fix `add` 0
(prod `n` (global (indt «nat»)) c0 \
prod `m` (global (indt «nat»)) c1 \ global (indt «nat»)) c0 \
fun `n` (global (indt «nat»)) c1 \
fun `m` (global (indt «nat»)) c2 \
match c1 (fun `n` (global (indt «nat»)) c3 \ global (indt «nat»))
[c2,
fun `p` (global (indt «nat»)) c3 \
app [global (indc «S»), app [c0, c3, c2]]]
C = «Nat.add»
fixコンストラクタは引数に、清書されたヒント、再帰引数の番号 (0から始まる)、再帰関数の型、最後に再帰呼び出しがバインドされた変数を介して表される本体を取ります。
type fix name -> int -> term -> (term -> term) -> term.
matchコンストラクタは、検査される項、return節、および分岐のリストを引数にとります。各分岐は、対応するコンストラクタの引数を入力とする Coq 関数です。順序は帰納型宣言のコンストラクタの順序に従います。
type match term -> term -> list term -> term.
return節は、入力で帰納型のインデックス、検査された項、および、分岐の型を生成することを期待する Coq 関数として表されます。
訳注：returnの後には、matchの節の型を書く。matchの節の型が依存型であるなどして、coqが型推論で見抜けない場合に教えてあげるためにある。Definitionの2行目の x は、値2である。この2箇所の x を他の値にしても、通る。
Definition m (h : 0 = 1 ) P : P 0 -> P 1 :=
match h as e in eq _ x return P 0 -> P x with
| eq_refl => fun (p : P 0) => p
end.
Elpi Query lp:{{
coq.locate "m" (const C),
coq.env.const C (some (fun _ _ h\ fun _ _ p\ match _ (RT h p) _)) _,
coq.say "The return type of m is:" RT
}}.
Query assignments:
C = «m»
RT = c0 \ c1 \
fun `x` (global (indt «nat»)) c2 \
fun `e`
(app [global (indt «eq»), global (indt «nat»), global (indc «O»), c2])
c3 \ prod `_` (app [c1, global (indc «O»)]) c4 \ app [c1, c2]
コンストラクタ sort
議論する価値のある最後のコンストラクタは sort です。
type sort universe -> term.
type prop universe.
type typ univ -> universe.
不透明な型 univ はユニバース レベルの変数です。 Elpi はこれらの変数間の制約のストアを保持し、制約を課すために
coq.univ.* という名前の API を提供します。
訳注：
coq.univ.*というAPIは残っているが、<=、=、< は、
coq.univ.leq、coq.univ.eq、coq.univ.sup から、
coq.sort.leq、coq.sort.eq、coq.sort.sup に改称された。訳注終わり。
Elpi Query lp:{{
coq.sort.sup U U1,
coq.say U "<" U1,
/* This constraint can't be allowed in the store! */
not(coq.sort.leq U1 U)
}}.
Query assignments:
U = typ «tut.59»
U1 = typ «tut.60»
Universe constraints:
UNIVERSES:
{tut.60 tut.59} |= tut.59 < tut.60 これが制約である。
note: ユーザが手動でユニバース制約を宣言することは想定されていません
型チェックプリミティブは、制約のストアを自動的に更新し、Coq ユニバース変数を Elpi の統合変数 (U および V 以下)の代わりに配置します。
組込述語coq.typecheckAPI を使用して、ユニバースの制約をもう少し試してみましょう。
訳注： IDの型Tは、
T = prod `x` (sort (typ U)) (c0 \ sort (typ U))
sort (typ U)は、prop -> term型だが、ここでは、sort (type U)自体がxの型で、
xはU : propの実体と考えるべき。
prod はΠで、第2引数はxの型注釈であるから、
Π(x : U)U となる。この場合Πは単なる->であるから、T = U -> Uとなる。
Elpi Query lp:{{
ID = (fun `x` (sort (typ U)) x\ x),
coq.typecheck ID T ok
}}.
Query assignments:
ID = fun `x` (sort (typ «tut.19»)) c0 \ c0
T = prod `x` (sort (typ «tut.19»)) c0 \ sort (typ «tut.19»)
U = «tut.19»
| ELPIの値 | ELPIの型 |
|---|---|
| «tut.19» | univ |
| typ «tut.19» | universe |
| sort (type «tut.19») | term |
訳注終わり。
Elpi Query lp:{{
ID = (fun `x` (sort (typ U)) x\ x),
A = (sort (typ U)), /* the same U as before */
B = (sort (typ V)),
coq.say "(id b) is:" (app [ID, B]),
/* error, since U : U is not valid */
coq.typecheck (app [ID, A]) T (error ErrMsg),
coq.say "(id a) is illtyped:" ErrMsg,
/* ok, since V : U is possible */
coq.typecheck (app [ID, B]) T ok,
/* remark: U and V are now Coq's univ with constraints */
coq.say "after typing (id b) is:" (app [ID, B]) ":" T,
coq.univ.print
}}.
ID = fun `x` (sort (typ «tut.80»)) c0 \ c0
U = «tut.80»
V = «tut.81»
A = sort (typ «tut.80»)
B = sort (typ «tut.81»)
ErrMsg = Illegal application:
app [ID, B] の型Tは、T = sort (typ U)
訳注： Coqでいうと
Variable U : Type.
Variable V : U.
Definition id := fun x : U => x.
Fail Check id U.
Check id V.
訳注終わり。
diagnosticデータ型は、coq.typecheckによって使用され、項が適切に型付けされているかどうかを示します。コンストラクタokは成功を通知しますが、error はエラーメッセージを伝えます。成功した場合、ユニバースの制約がストアに追加されます。
引用と逆引用 Quotations and Antiquotations
これまでのようにGallina項を書くことは確かに可能ですが、非常に冗長で扱いにくいです。 Elpi は引用と逆引用のシステムを提供し、Coqパーサを利用して項を記述できるようにします。
Coq から Elpi までの引用は lp:{{ ... }} と書かれ、チュートリアルの最初からこれを使用しています。Elpi から Coq への引用は {{:coq ... }} または単に {{ ... }}と書きます。:coq がデフォルトの引用です(Coq は デフォルトの引用符がないため、常にlp:と記述する必要があります）。
Elpi Query lp:{{
/* the ":coq" flag is optional */
coq.say {{:coq 1 + 2 }} "=" {{ 1 + 2 }}
}}.
app
[global (const «Nat.add»),
app [global (indc «S»), global (indc «O»)],
app [global (indc «S»),
app [global (indc «S»),
global (indc «O»)]]]
=
app
[global (const «Nat.add»),
app [global (indc «S»), global (indc «O»)],
app [global (indc «S»),
app [global (indc «S»),
global (indc «O»)]]]
もちろん、引用はネストできます。
Elpi Query lp:{{
coq.locate "S" S,
coq.say {{ 1 + lp:{{ app [global S, {{ 0 }} ] }} }}
% elpi coq elpi coq elpi coq
}}.
app
[global (const «Nat.add»),
app [global (indc «S»), global (indc «O»)],
app [global (indc «S»), global (indc «O»)]]
Query assignments:
S = indc «S»
束縛変数を管理する1つのルールがある：
重要：
変数が Coq または Elpi の言語で束縛されている場合、変数はその言語でのみ参照できます (他の言語からは参照できません)。
次の例は恐ろしいものですが、この点を証明しています。実際のコードでは、不当な（視覚的な）衝突を避けて、変数に適切な名前を選択することをお勧めします。
Elpi Query lp:{{
coq.say (fun `x` {{nat}} x\ {{ fun x : nat => x + lp:{{ x }} }})
% e c c e
}}.
fun `x` (global (indt «nat»)) c0 \
fun `x` (global (indt «nat»)) c1 \
app [global (const «Nat.add»), c1, c0]
A commodity quotation without parentheses let's one quote identifiersomitting the curly braces.つまり lp:{{ ident }} は lp:ident だけで書けます。
Elpi Query lp:{{
coq.say (fun `x` {{nat}} x\ {{ fun x : nat => x + lp:x }})
% e c c e
}}.
fun `x` (global (indt «nat»)) c0 \
fun `x` (global (indt «nat»)) c1 \
app [global (const «Nat.add»), c1, c0]
Coq 変数を Elpi のユニフィケーション変数のスコープに入れることはよくあることですが、これは単に lp:{{ X {{ a }} {{ b }} }}の省略形である lp:(X a b) と書くだけで実行できます。
警告: lp:X a b (括弧なし) と書くと、Elpiの関数適用ではなく Coqの関数適用になります。
これらの省略形で少し遊んでみましょう。
訳注：以下は全て同じである。
Elpi Query lp:{{
coq.say {{ fun a b : nat => a + b }}
}}.
Elpi Query lp:{{
coq.say {{ fun a b : nat => lp:{{ {{a + b}} }} }}
}}.
Elpi Query lp:{{
coq.say {{ fun a b : nat => lp:{{ {{a + b}} }} }}
}}.
Elpi Query lp:{{
X = (x\ y\ {{ lp:y + lp:x }}),
coq.say {{ fun a b : nat => lp:{{X {{a}} {{b}}}} }}
}}.
Elpi Query lp:{{
X = (x\ y\ {{ lp:y + lp:x }}),
T = {{ fun a b : nat => lp:{{X {{a}} {{b}}}} }},
coq.say T
}}.
Elpi Query lp:{{
T = {{ fun a b : nat => a + b }},
coq.say T
}}.
Elpi Query lp:{{
T = {{ fun a : nat => fun b : nat => a + b }},
coq.say T
}}.
fun `a` (global (indt «nat»)) c0 \
fun `b` (global (indt «nat»)) c1 \
app [global (const «Nat.add»), c0, c1]
Elpi Query lp:{{
T = (fun `a` {{nat}} a \ (fun `b` {{nat}} b \ {{lp:a + lp:b}})),
coq.say T
}}.
Elpi Query lp:{{
T = (fun `a` {{nat}} a \ {{fun b : nat => lp:a + b }}),
coq.say T
}}.
Elpi Query lp:{{
T = {{ fun a : nat => lp:{{fun `b` {{nat}} b \ {{a + lp:b}} }} }},
coq.say T
}}.
訳注終わり。
Elpi Query lp:{{
X = (x\y\ {{ lp:y + lp:x }}), /* x and y live in Elpi */
coq.say {{ fun a b : nat => lp:(X a b) }} /* a and b live in Coq */
}}.
fun `a` (global (indt «nat»)) c0 \
fun `b` (global (indt «nat»)) c1 \
app [global (const «Nat.add»), c1, c0]
また別のクォーテーションでは、Coq 8.10 で導入された coqlib 機能にアクセスできます。Coqlib は、コードと定数の実際の名前との間の間接性を提供します。
Register Coq.Init.Datatypes.nat as my.N.
Register Coq.Init.Logic.eq as my.eq.
Elpi Query lp:{{
coq.say {{ fun a b : lib:my.N => lib:@my.eq lib:my.N a b }}
}}.
fun `a` (global (indt «nat»)) c0 \
fun `b` (global (indt «nat»)) c1 \
app [global (indt «eq»), global (indt «nat»), c0, c1]
note:: lib:@some.name の (オプションの) @ は、暗黙の引数を無効にします。
{{:gref .. }} 引用符により、項の代わりにgrefデータ型を構築できます。
lib:もサポートしています。
(*
Elpi Query lp:{{
coq.say {{:gref nat }},
coq.say {{:gref lib:my.N }}.
}}.
ProofGeneral では、うまくいかないが、
indt «nat»
indt «nat»
*)
訳注：
Elpi Query lp:{{
coq.say {{ nat }},
coq.say {{ lib:my.N }}
}}.
Coqとしての意味を持つのはtermであるので、コンストラクタglobalがつく。
global (indt «nat»)
global (indt «nat»)
Elpi Query lp:{{
coq.locate "nat" GRnat, coq.say GRnat,
coq.locate "lib:my.N" GRN, coq.say GRN
}}.
gref型で取り出したいときは、{{:gref ...}}を使うか、上のようにする。
indt «nat»
indt «nat»
引用符を使用する際に留意すべき最後のことは、(Coq の「Arguments」設定に従って) 暗黙の引数が挿入されますが、自動的に合成されないことです。
それらを合成するのは、タイプチェッカーまたはエラボレーターの仕事です。 これについては、Holesのセクションで詳しく見ていきます。
Elpi Query lp:{{
T = (fun `ax` {{nat}} a\ {{ fun b : nat => lp:a = b }}),
coq.say "before:" T,
coq.typecheck T _ ok,
coq.say "after:" T
}}.
typecheck によって、
Coqの ``eq`` の最初の引数（型の指定）が具体化される。
before:
fun `ax` (global (indt «nat»)) c0 \
fun `b` (global (indt «nat»)) c1 \
app [global (indt «eq»), X0 c1, c0, c1]
after:
fun `ax` (global (indt «nat»)) c0 \
fun `b` (global (indt «nat»)) c1 \
app [global (indt «eq»), global (indt «nat»), c0, c1]
コンテキスト The context
Elpi のコンテキスト (=> を経由してロードされたルールで構成される仮想プログラム)は、Coq API によって考慮されます。 特に、バインドされた変数が交差するたびに、プログラマーはその変数にタイプを関連付けるルールをコンテキストにロードする必要があります。それを行うための施設がいくつかありますが、まず忘れるとどうなるか見てみましょう。
The context of Elpi (the hypothetical program made of rules loadedvia :e:=>) is taken into account by the Coq APIs. In particular every timea bound variable is crossed, the programmer must load in the context arule attaching to that variable a type. There are a few facilities todo that, but let's first see what happens if one forgets it.
Elpi Query lp:{{
T = {{ fun x : nat => x + 1 }},
coq.typecheck T _ ok,
T = fun _ _ Bo
}}.
Bo = c0 \
app
[global (const «Nat.add»), c0,
app [global (indc «S»), global (indc «O»)]]
Fail Elpi Query lp:{{
T = {{ fun x : nat => x + 1 }},
coq.typecheck T _ ok,
T = fun _ _ Bo,
coq.typecheck (Bo x) _ _
}}. (* .fails *)
この致命的なエラーは、(Bo x) の x が Coq に認識されていないことを示しています。これは Elpi で想定されている変数ですが、型「nat」が失われました。
pi x\ を使用して変数xを定義してもよいが、
x の型をどこかに記録する必要があります。
Elpiの束縛子（バインダ）をCoqに並行移動（トラバース）する方法は、ある意味で Zipper に似ています。Elpiのコンテキストは、束縛子（バインダ）に関連する Zipper コンテキストの一部を記録する必要があります。
そのために、decl と def の 2 つの組込述語が使用されます。
pred decl i:term, o:name, o:term. % Var Name Ty
pred def i:term, o:name, o:term, o:term. % Var Name Ty Bo
Elpi Query lp:{{
T = {{ fun x : nat => x + 1 }},
coq.typecheck T _ ok,
T = fun N Ty Bo, /* T からラムダ変数の名前と型をとりだす */
pi x\
((decl x N Ty) => /* x の名前と型を与える */
(coq.typecheck (Bo x) _ ok)) /* 括弧を補足した */
}}.
N = `x`
Ty = global (indt «nat»)
この作業を容易にするために、Coq-Elpi は @pi-decl などのいくつかの汎用マクロを提供しています。
macro @pi-decl N T F :- pi x\ decl x N T => F x.
注:: ラムダ抽象化の優先度 x\ により、次のコードを F の括弧なしで記述できます。
Elpi Query lp:{{
T = {{ fun x : nat => x + 1 }},
coq.typecheck T _ ok,
T = fun N Ty Bo,
@pi-decl N Ty (x\ /* ここの括弧は省略できる */
coq.typecheck (Bo x) _ ok)
}}.
tip: @pi-decl N Ty x\ は、コンストラクタ fun と prod の同じ順序で引数を取りますが、 @pi-def N Ty Bo x\ は、コンストラクタ letと同じ順序で引数を取ります。
訳注: @pi-def の例
macro @pi-def N T B F :- pi x\ def x N T B => cache x B_ => F x.
次の例はCoqのletに相当する。
Check let x := 1 in x + 1.
Elpi Query lp:{{
T = {{ fun x : nat => x + 1 }},
coq.typecheck T _ ok,
T = fun N Ty Bo,
@pi-def N Ty {{1}} x\
coq.typecheck (Bo x) _ ok /* x\以降の括弧を省略している */
}}.
訳注終わり。
Holes (implicit arguments)
「Evar」（存在量化されたメタ変数の Coq スラング）は、Elpiのユニフィケーション変数と型制約として表されます。
Elpi Query lp:{{
T = {{ _ }},
coq.say "raw T =" T,
coq.sigma.print,
coq.say "--------------------------------",
coq.typecheck T {{ nat }} ok,
coq.sigma.print
}}.
組込述語coq.typecheck, coq.sigma.print の呼び出し前には、興味深いものは何も表示されません。
Coq-Elpi mapping:
RAW:
ELAB:
呼び出し後に次の構文制約も表示されます:
訳注： evar 述語が呼び出されたが、第1引数が変数であるため制約にかかり、evar述語の実行がサスペンドしている。訳注終わり。
evar (X1) (global (indt «nat»)) (X1) /* suspended on X1 */
これは、ホール X1 が Coqのevar にリンクされており、型が「nat」であると予想されることを示しています。
Coq evars から、Elpi のユニフィケーション変数へのマッピングはすでに空ではありません。
Coq-Elpi mapping:
RAW:
?X12 <-> X1
ELAB:
?X12 <-> X1
Note: Coq の evar 識別子の形式は「?X」ですが、Elpi のものには先頭に「?」がありません。Coq Evar マップは、?X12 が nat 型を持つことを示しています。
EVARS:
?X12==[ |- nat] (internal placeholder) {?elpi_evar}
?X11==[ |- nat => ?elpi_evar] (internal placeholder)
?X10==[ |- Type => nat] (internal placeholder)
SHELF:
FUTURE GOALS STACK:
?X12
直観的には、evar に型の判断を割り当てる Coq の Evar マップ(別名シグマまたは evd) は、同じ情報を運ぶ Elpi 制約で表されます。
rawの Elpi のユニフィケーション変数は、Coq の API に渡されると、Coq evar に自動的にリンクされます。「raw」と「elab」のユニフィケーション変数の違いの説明は、タクティクに関する章で説明します。ここでは、evar 制約の X1 の 2 番目のコピーは何の役割も果たしません。
では、型のコンテキストはどうでしょうか。
Elpi Query lp:{{
T = {{ fun x : nat => x + _ }},
coq.say "raw T =" T,
T = fun N Ty Bo,
@pi-decl N Ty x\
coq.typecheck (Bo x) {{ nat }} ok,
coq.sigma.print % ここに「.」があるとPGでうまくいかない。
}}.
raw T =
fun `x` (global (indt «nat»)) c0 \
app [global (const «Nat.add»), c0, X0 c0]
rawのT の値では、束縛子（バインダ）c0\ の下で生じる x + _ の穴が、Elpiのユニフィケーション変数
`X1 c0 によって表されていることがわかります。 つまり、X1`` が ``c0``を参照することを意味します (``c0`` は ``X1`` のスコープ内にあります)。
今回の制約はもう少し複雑です。 それを分析しましょう：
{c0 c1} : decl c1 `x` (global (indt «nat»))
?- evar (X1 c1) (global (indt «nat»)) (X1 c1) /* suspended on X1 */
ここで、{...}は制約で使用される名前の集合(必ずしも最小化される必要はありません)であり、?- は結論 (中断されたゴール)から仮定 (コンテキスト) を分離します。
CoqとElpiの間のマッピングは：
Coq-Elpi mapping:
RAW:
?X15 <-> X1
ELAB:
?X15 <-> X1
ここで、?X13は、Coqのシグマの中にあります。
EVARS:
?X15==[x |- nat] (internal placeholder) {?elpi_evar}
?X14==[x |- nat => ?elpi_evar] (internal placeholder)
?X13==[x |- Type => nat] (internal placeholder)
SHELF:
FUTURE GOALS STACK:
?X15
予想どおり、Elpi の制約と Coq の evar マップの両方が、Holeのスコープ内にある変数 x (nat 型) を使用してコンテキストを記録します。
タクティクを書いていない限り、Elpi の制約は evar マップを表すために使用されます。 termが変数に割り当てられると、対応する制約が削除されます。タクティクを書いているとき、evar を表す Elpi 変数にtermを割り当てると、そのtermが期待される型を持っていることを確認するために型チェックの目標が再開されるように、termが結び付けられます。これについては、タクティクに関するチュートリアルで詳しく説明します。
パターンの断片の外側 (Outside the pattern fragment)
evar のこのエンコーディングは、プログラマーがそれらについてあまり気にする必要がないようなものです: Evar マップのような代入/型付けマップを持ち歩く必要はなく、そこで新しい変数を宣言する必要もありません。Holeを含む Elpi 項を渡して Coq API を自由に呼び出すことができます。
ただし、1つの制限があります。このチュートリアルの残りの部分では、これについて説明し、それに対処するためのいくつかの API とオプションを紹介します。
制限は、自動宣言とマッピングがすべての状況で機能しないことです。特に、パターンの断片ある Elpi ユニフィケーション変数に対してのみ機能します。つまり、それらは個別の名前 (束縛された変数) にのみ適用されます。
これは、たとえば、引用符内に書かれたすべての{{ _ }}に当てはまりますが、この断片の外側にtermを作成することは難しくありません。 特に、Elpi の置換 (関数適用) を使用して、束縛された変数の代わりに任意のtermを配置できます。
Fail Elpi Query lp:{{
T = {{ fun x : nat => x + _ }},
% remark the hole sees x
T = fun N Ty Bo,
% 1 is the offending term we put in place of x
Bo1 = Bo {{ 1 }},
% Bo1 is outside the pattern fragment
coq.say "Bo1 (not in pattern fragment) =" Bo1,
% boom
coq.typecheck Bo1 {{ nat }} ok
}}. (* .fails *)
このスニペットは、次のメッセージを出して失敗します。
Flexible term outside pattern fragment:
X0 (app [global (indc «S»), global (indc «O»)])
実際、Bo1 には、パターンの断片の外側のterm、plus の第2引数が含まれています。これは、X0 c0 で c0 を {{ 1 }} に置き換えることによって得られます。 .
Elpi で Coq 拡張機能をプログラミングしているときに、Coq のterm (Holeのある) 構文木として使用したい場合があり、それに置換を適用する必要がありますが、Holeの範囲はあまり気にしません。これらのHoleを「{{ _ }}」のままにしておきたいと思います(束縛された変数のコンテキスト全体を見る新しいHole)。ある意味では、{{ _ }} を特別なダミー定数にして、必要に応じてオンザフライで実際の穴に変えたいと考えています。
この使用例は完全に正当であり、 マクロ@holes!のオプションのおかげで、入力で条件を受け取るすべての API でサポートされています。
Elpi Query lp:{{
T = {{ fun x : nat => x + _ }},
T = fun N Ty Bo,
Bo1 = Bo {{ 1 }},
coq.say "Bo1 before =" Bo1,
/* by loading this rule in the context, we set */
/* the option for the APIs called under it */
@holes! => coq.typecheck Bo1 {{ nat }} ok,
coq.say "Bo1 after =" Bo1
}}.
組込述語coq.typecheckへの呼び出しの後、X0 には _\ X1 というtermが割り当てられます。これは、問題のある引数が削除 (破棄) されたことを意味します。
注意: termを取るすべての API は マクロ@holes!のオプションをサポートします。
@holes!のオプションに加えて、パターンの断片の外のtermを処理できる API のクラスがあります。これらの API はterm skeleton を入力として受け取ります。組込述語coq.typecheckが最初の引数で行うように、スケルトンはその場で変更されませんが、それに関連するtermにかなり詳しくなります。
ある意味では、スケルトンを使用する API は、termの構造を変更できるため、より強力です。 強制を挿入しますが、入力termと出力termの間の関係が単純ではない (ユニフィケーションではない) という意味で、直截的ではありません。
Coercion nat2bool n := match n with O => false | _ => true end.
Open Scope bool_scope.
Elpi Query lp:{{
T = {{ fun x : nat => x && _ }},
T = fun N Ty Bo,
Bo1 = Bo {{ 1 }},
coq.elaborate-skeleton Bo1 {{ bool }} Bo2 ok
}}.
Query assignments:
Bo = c0 \app [global (const «andb»), c0, X0 c0]
Bo1 = app
[global (const «andb»),
app [global (indc «S»),
global (indc «O»)],
X0 (app [global (indc «S»),
global (indc «O»)])]
Bo2 = app
[global (const «andb»),
app [global (const «nat2bool»),
app [global (indc «S»),
global (indc «O»)]],
X1]
N = `x`
T = fun `x`
(global (indt «nat»))
c0 \ app [global (const «andb»), c0, X0 c0]
Ty = global (indt «nat»)
_uvk_31_ = X0
Syntactic constraints:
evar (X2) (global (indt «bool»)) X1 /* suspended on X2, X1 */
ここでBo2はBo1を取得し、すべてのユニフィケーション変数をHoleと見なし、すべての {{ Type }} レベルをフレッシュ (この例では何もありません) と見なし、Coq のエラボレータを実行して取得します。
結果は同様の構造 (スケルトン) を持つ用語ですが、x をブール値にするコアーションが挿入され、新しいHole X1 がtermの代わりに配置されます。
X0 (app [global (indc «S»), global (indc «O»)]) はそのままです。
スケルトンとその API については、コマンドのチュートリアルで詳しく説明されています。
このチュートリアルは以上です。
コマンドまたはタクティクに関するチュートリアルを読んで続けることができます。
https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_command.html
https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_tactic.html