Coq においてゴール (サブゴールを含む) とは証明項の中の穴であり、証明を進めるというのはその穴を埋めていくことである。
という素朴な理解でいままで済ましていたのだが、 Ltac2 でサブゴールを作るのにはこの理解では足りなくて、 いろいろ調べた。
やりたいのは、Ltac2 で証明項を作る際に、その中にはサブゴールを入れて、 そのサブゴールにはコンテキストとして可変個の仮定を提供したい、ということである。 とくに今回は、相互再帰の fix 項をつくって、その再帰関数 (相互再帰なので複数ある) を仮定として提供するということをしたかった。 そして、相互再帰関数が何個の関数から構成されているかは事前にはわからない、という状況である。
サブゴールは証明項においては evar (existential variable) である。 また、コンテキストに入っている仮定は、evar をスコープに含む束縛変数である。 という、このくらいのことは知っている。
ただ、証明項は変わらないのにゴールが変わることがある。 change tactic を使えば証明項は変わらないのにゴールの結論 (evar の型) を変えられる。 clear tactic を使えばコンテキストから仮定を消せる。 rename tactic で仮定の名前を変えることもできる。
このへんの話があるので、ゴールというのは evar に加えていろいろ情報が加えてあるのだろうな、とは思っていた。
というのが今回の前に知っていたことである。
Ltac2 でサブゴールを作る方法は、Ltac2のマニュアルには説明がないと思う。
でもまぁ、evar を作ればいいんだろう、ということでやってみると、 open_constr を使って以下のようにすればサブゴール (を含む証明項) を作れる。 アンダースコア (_) の部分が evar になる。 evar の外側で変数 n を束縛しているので、コンテキストには n が追加されている。よしよし。
From Ltac2 Require Import Ltac2. Goal False. refine (open_constr:((fun (n:nat) => _) 0)). (* 1 goal n : nat ______________________________________(1/1) False *) Show Proof. (* ((fun n : nat => ?Goal) 0) *) Abort.
コンテキストには、assumption と definition を入れられる。 definition はコンテキストに変数の内容も含めるもので、証明項では let で束縛された変数に対応する。 assumption は変数の内容がないもので、証明項では let 以外 (fun, match, fix) で束縛された変数に対応する。
以下のように、let を含む証明項で、let の束縛変数のスコープの中に evar を入れると、 コンテキストには definition が出てくる。よしよし。
Goal False. refine (open_constr:(let n := 0 in _)). (* 1 goal n := 0 : nat ______________________________________(1/1) False *) Show Proof. (* (let n := 0 in ?Goal) *) Abort.
さて、やりたいのは、可変個の仮定をコンテキストに入れることである。 open_constr 一回で証明項を生成する限り、固定個の変数しか作れないので、 束縛変数の導入と、evar の生成をわけて行ってみよう。 (ここでは、証明項のわかりやすさを考えて let を使っているが、fun でもよい。) しかし、こうすると、なぜかコンテキストに n が出てこない。
Goal False. refine (let t := open_constr:(_) in open_constr:(let n := 0 in $t)). (* 1 goal ______________________________________(1/1) False *) Show Proof. (* (let n := 0 in ?Goal) *) Abort.
証明項は上とまったく同じなので、なにがうまくないのかわからない。
いろいろ調べた結果、けっきょく、ゴールの情報は型検査の際に生成され、あとでその evar を他の項に埋め込んでもゴールの情報は更新されないという理解に至った。 ゴールの情報は、evar という項と、sigma (OCaml レベルでは Evd.evar_map 型) の両方にまたがって管理されており、型検査の際にゴールの情報が生成されるのだ。 Ltac2 で sigma は明示的には扱わないが、暗黙に存在する。 (Ltac2 では env も明示的には扱わないのと同じ。)
open_constr:(_) という式が評価されると、その時点で型検査が行われ、項が生成される。 その際に evar の外側には変数の束縛が存在しないので、そのゴールには仮定は追加されない。
その後で open_constr:(let n := 0 in ltac2:(exact $t)) として evar を他の項に埋め込んでも、 ゴールの内容は変わらないため、ゴールのコンテキストに n は追加されない。
どうにかできないか、といろいろ悩んだ結果、preterm を使うと可能ということがわかった。 preterm というのは型検査を後で行う項を生成する記法である。 以下では、preterm の形で let 式の中に evar を埋め込んだ後に Constr.Pretype.pretype で型検査を行って constr を生成している。 このようにすると、サブゴールのコンテキストに n が出てくる。
Goal False.
refine (let t := preterm:(_) in
let t := preterm:(let n := 0 in $preterm:t) in
Constr.Pretype.pretype
Constr.Pretype.Flags.open_constr_flags_no_tc
Constr.Pretype.expected_without_type_constraint
t).
(*
1 goal
n := 0 : nat
______________________________________(1/1)
False
*)
Show Proof.
(* (let n := 0 in ?Goal) *)
Abort.
このように、evar の生成と束縛変数の導入を別々に行えるので、繰り返し束縛変数を導入すれば、コンテキストに可変個の仮定を入れることができる。
なお、Constr.Pretype.pretype の引数で、対象の項の型を指定することができる。 今回は、let n := 0 in _ という項なので、この項の型を指定することは、evar の型を指定することになる。 evar の型はサブゴールの結論なので、以下のように id False を指定すると、サブゴールの結論が id False になる。
Goal False.
refine (let t := preterm:(_) in
let t := preterm:(let n := 0 in $preterm:t) in
Constr.Pretype.pretype
Constr.Pretype.Flags.open_constr_flags_no_tc
(Constr.Pretype.expected_oftype constr:(id False))
t).
(*
1 goal
n := 0 : nat
______________________________________(1/1)
id False
*)
Show Proof.
(* (let n := 0 in ?Goal) *)
Abort.
まぁ、これはコンテキストに入れるものが definition だから簡単なのであって、 assumption を入れる場合は証明項の型がそのまま evar の型にはならないため、 Constr.Pretype.expected_oftype で簡単に evar の型を指定することはできない。
上記では let で definition を追加したサブゴールを生成した。 let のかわりに fun を使えば assumption を追加したサブゴールを生成できる。
さて、こうやってコンテキストに必要な仮定があるゴールを表現した evar を生成することができたが、 得られた項は evar が let や fun にくくられている。
作りたい証明項がその (let や fun にくくられた) 形であればこれでいいのだが、 そうでない形にしたい場合には、evar だけの項がほしい。
今回は fix で束縛された再帰関数を仮定としてコンテキストに入れたかったので、 fun が邪魔だったのだが、これは Constr.Unsafe.kind で項を分解して evar を取り出せばよい。
もちろん、そうやって取り出した evar は、de Bruijn index で束縛変数を参照しているため、 証明項に埋め込む際には、その参照が壊れないようにする必要がある。 fix の場合は、fix 直下であれば de Bruijn index も一致するのだが、 埋め込みたいのは、再帰関数の引数を受け取る fun の内側なので、引数の数だけ de Bruijn index をずらす必要があり、 これは Constr.Unsafe.liftn で可能。
あと、Constr.Pretype.expected_oftype を使わずに evar の型を指定するには、 evar の型を Constr.type で取り出して (これは別の evar になる)、 Unification.unify_with_current_ts で期待する型と unify すればよい。
ということで、なんとかなった。
なお、Elpi だと、このへんのことは Tutorial on Coq tactics: The proof engine に説明されているようで、 説明がない Ltac2 に比べるとやりやすいかもしれない。
[latest]