天泣記

最近、Ltac, Ltac2, coq-elpi など、Coq の tactic 言語を調べていて、束縛変数を含んだ項のマッチについて調べ、 Ltac の挙動がかなり意外であることに気がついた。

ゴールに forall (a b : nat), a = b という項がある状態でいくつか match してみよう。なお、forall (a b : nat), a = b は forall (a : nat), forall (b : nat), a = b の略記である。

Lemma L : forall (a b : nat), a = b.

まず、以下のように、ゴール (の結論) に対して forall x, ?P というパターンでマッチを行うと、 idtac x で a が出力され、 idtac P で (forall b : nat, x = b) が出力される。つまり、forall (a : nat), forall (b : nat), a = b の外側の forall が取り除かれた、中身の forall (b : nat), a = b というが P に束縛されている。そして、その際に、取り除かれた forall (a : nat) の部分の束縛変数 a が、x という Ltac で記述した名前に変わっている。変数名が変わるというのはなかなか驚くところである。

match goal with
| [ |- forall x, ?P ] => idtac x; idtac P
end.
(*
a
(forall b : nat, x = b)
*)

そうやって取り出された項は、項の一部として利用できる。以下では、P として取り出した部分項を利用して fun (x : nat) => P という項を作っている。作ったものを観測するために、pose で p という名前で項を束縛している。 (また、pose が成功するということは、fun (x : nat) => P という項が型検査を通っていることも示している) ここでは、fun (x : nat) => P として作った項は、P が展開され、fun a : nat => forall b : nat, a = b になっている。

match goal with
| [ |- forall x, ?P ] => pose (p := fun (x : nat) => P)
end.
(* p := fun a : nat => forall b : nat, a = b : nat -> Prop *)
clear p.

match で取り出した項を match の外に返して、その後で利用することも可能である。以下のように match の外で fun (x : nat) => P と利用すると、fun x : nat => forall b : nat, x = b という項が生成されている。

let P := match goal with
         | [ |- forall x, ?P ] => P
         end
in
pose (p := fun (x : nat) => P).
(* p := fun x : nat => forall b : nat, x = b : nat -> Prop *)
clear p.

上記のふたつで、前者では fun a : nat => ... という項が生成されているが、後者では fun x : nat => ... という項が生成されている。この違いは、fun (x : nat) => P として項を生成したときに、前者では x に b という名前が束縛されていたが、後者では x が束縛されていないという違いが原因だろう。

まぁ、細かい話はともかく、上記のように、束縛変数を含む部分項を取り出して、その部分項を別の文脈に埋め込むことができる。

たださすがに、必要な変数がない文脈で使おうとした場合はエラーになる。

Fail match goal with
| [ |- forall x, ?P ] => pose (p := P)
end.
(* Ltac variable P depends on pattern variable name x which is not bound in current context. *)

もうちょっと複雑なことを試してみよう。

外側の forall ふたつをパターンに書くと、その内側の a = b が、 Ltac で書いた名前に変数名に変わって x = y となる。

match goal with
| [ |- forall x y, ?P ] => idtac x; idtac y; idtac P
end.
(*
a
b
(x = y)
*)

では、match を 2段階にわけてやるか、と試すと、以下のようにエラーになる。どうやら外側の変数束縛を取り除いた場合、その中の項からさらに変数束縛を取り除くことはできないらしい。

Fail match goal with
| [ |- forall x, ?P ] =>
    match P with
    | forall y, ?Q => idtac x; idtac y; idtac P
    end
end.
(*
Must evaluate to a closed term
offending expression:
P
this is an object of type constr_under_binders
*)

段階にわけて変数束縛を取り除くことができないということは、可変個の束縛をひとつずつ繰り返し (再帰的に) 取り除くことができないということで、ジェネリックな処理は無理そうである。

あと、エラーメッセージに constr_under_binders という型の名前が出ている。

これを探してみると、Coq の pretyping/ltac_pretype.mli にコメントが書いてある。起源を探すと 2010年の <URL:https://github.com/coq/coq/commit/c3d45696c271df086c39488d8a86fd2b60ec8132> のようである。

このコメントはなかなか興味深い。 non-linear なパターンでも使える、型は保存していないとか。

型を保存していないということは、その変数名を別の型として利用できるのだろうか、と思って以下のように試すと、できてしまった。なるほど。項を生成するために Ltac 変数 x, y を使って forall (x y : Prop), x /\ y と書いているが、生成された項は forall a b : Prop, a /\ b となっており、 match で取り出した変数名の a, b が使われている。元々のゴールの a, b は nat であるが、生成した項では Prop であり、型が異なる。

match goal with
| [ |- forall x y, ?P ] => pose (H := forall (x y : Prop), x /\ y)
end.
(* H := forall a b : Prop, a /\ b : Prop *)
clear H.
Abort.

あと、<URL:https://coq.discourse.group/t/gallina-function-application-in-ltac/316> にあったのだが、こうやって露出した束縛変数を置換するには以下のように match をすればよいようだ。そのための notation の定義が示されている。

Notation "'subst!' y 'for' x 'in' f" := (match y with x => f end) (at level 10).

以下では、match で取り出した x = y から、x と y を置換した項をいくつか作っている。

Lemma L : forall (a b : nat), a = b.
match goal with
| [ |- forall x y, ?P ] =>
    pose (H1 := forall (x : nat), (subst! 0 for y in P));
    pose (H2 := forall (y : nat), (subst! 1 for x in P));
    pose (H3 := subst! 2 for x in (subst! 3 for y in P))
end.
(*
H1 := forall a : nat, a = 0 : Prop
H2 := forall b : nat, 1 = b : Prop
H3 := 2 = 3 : Prop
*)
clear H1 H2 H3.
Abort.

#3 Coq の Ltac2 における、束縛変数を含んだ項のマッチ

Ltac のマニュアルによると、Ltac は discouraged で他のものを使うのが勧められている。公式な代替は Ltac2 であり、Coq に標準添付されている。

なお、Ltac2 と明確に区別するために、いままでの Ltac を Ltac1 と呼ぶことがある。

Ltac2 で束縛変数を含んだ項のマッチができるのか調べると、これはできないようである。 Ltac2 のマニュアルに Unlike Ltac1, Ltac2 ?id metavariables only match closed terms. と書いてあるし、試してみてもマッチしない。

ではどうするかというと、ライブラリに Constr.Unsafe というというのがあって、これを使うと可能である。

以下に例を示す。

From Ltac2 Require Import Ltac2.
From Ltac2 Require Import Message.

Lemma L : forall (a b : nat), a = b.
Proof.
let g := Control.goal () in
match Constr.Unsafe.kind g with
| Constr.Unsafe.Prod b e =>
    match Constr.Binder.name b with
    | Some id => print (of_ident id)
    | None => ()
    end;
    print (of_constr (Constr.Binder.type b));
    print (of_constr e)
| _ => ()
end.
(*
a
nat
(forall b : nat, _UNBOUND_REL_2 = b)
*)

Coq plugin で (OCaml レベルの Constr.t 型や EConstr.t 型の) Gallina 項をいじったことのあるひとなら即座にわかると思うのだが、まぁそれそのものなのだと思う。

とくに束縛変数は de Bruijn index であり、内側から数えた番号で表現される。そのため、かなり注意して扱う必要がある。

残念なことに、Coq plugin なら、項から取り除いた束縛の情報で環境を拡張すれば、取り出した部分項に対応した環境を作れるのだが、どうも Ltac2 の環境は暗黙に存在するもので、そういう拡張を明示的に行うことはできないようである。

そのため、上記の (forall b : nat, _UNBOUND_REL_2 = b) という表示では、等式の左辺は項の中で束縛されていない変数であり、 (暗黙の環境を使って表示されるため) _UNBOUND_REL_2 という、de Bruijn index が 2 の変数という意味の表示になっている。

#4 coq-elpi における、束縛変数を含んだ項のマッチ

Ltac2 以外に有望な tactic 言語として、Elpi がある。 Elpi は、mathcomp2 が依存しているので、mathcomp2 を使うなら常に利用可能と想定できる。

なお、Elpi は λProlog という言語の実装 (のひとつ) である。

Elpi では、項は HOAS (Higher-Order Abstract Syntax) で表現される。 (Elpi における項の表現は Tutorial on the HOAS for Coq terms に説明されているが、HOAS というテクニックは Elpi 独自ではなく、以前から存在する)

なので、変数束縛を行う項 (forall, fun, let など) は、ボディを表現する項は Elpi の関数で表現される。中身を得たければ、なにかを渡してその関数を呼び出さなければならない。その関数は呼び出されると、その束縛変数の出現を、渡された引数に置き換えた項を返す。

というわけで、Elpi は最初から束縛変数を簡単に扱えるようデザインされている。 (この「簡単」というのは、ラムダ計算の変数置換で名前の衝突を避けるとか、de Bruijn index でやるよりは簡単、というくらいの意図である。)

試してみると以下のようになる。

From elpi Require Import elpi.

Elpi Tactic test.
Elpi Accumulate lp:{{
  solve (goal _Ctx _Trigger Type _Proof _) _ :-
    coq.say Type.
}}.
Elpi Typecheck.

Lemma L : forall (a b : nat), a = b.
elpi test.
(*
prod `a` (global (indt «nat»)) c0 \
 prod `b` (global (indt «nat»)) c1 \
  app [global (indt «eq»), global (indt «nat»), c0, c1]
*)
Abort.

表示された項の中で、c \ exp というのが、c を受け取って exp を返す無名関数の式である。いちばん外側は prod `a` (global (indt «nat»)) (c0 \ ...) という項なので、 (prod は依存積を意味して、つまり forall なので) forall (a : nat), ... という項を表現しており、body 部分は関数 c0 \ prod `b` ... で表現されている。

なお、Coq において HOAS はいくつか問題がある、という話が CPDT に載っている。 <URL:http://adam.chlipala.net/cpdt/html/Hoas.html>

問題が 3つあげられている:

positivity condition の条件により HOAS を帰納型で定義できない。
引数として渡された項の中身を調べて条件分岐するなどの関数を使えてしまい、それは項と対応しない。(そういうのを exotic term という)
関数を呼び出さないと中身を調べられない。とくに型安全な項 (項の型を、対象言語の型でインデックスされた型とするもの) とする場合、引数の型に合わせた項を用意する必要がある。

CPDT では、これらの問題を解決するために PHOAS (Parametric HOAS) を導入するのだが、 Elpi では HOAS のままである。

どうやって解決しているかというと、たぶん以下のようにしているのだと思う。

Elpi は Gallina とは別の言語で、positivity condition の制約はない
exotic term が存在できてしまうのはしょうがないとしてあきらめる
pi という機能で fresh な定数を生成することができるので、それを引数に渡して呼び出せば、問題なく中身を調べられる

Elpi の項の表現はなかなか強力で、weak head normal form を求める機構がライブラリとして実装されていたりする: elpi-reduction.elpi

ただ、現時点では相互再帰をサポートしていないようで、そこが残念ではある。 (README の Supported features of Gallina (core calculus of Coq) のところで mutual Inductive and CoInductive types と mutual fixpoints はチェックが入っていないし、試すとエラーになる)

天泣記

2024-10-30 (Wed)