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つあげられている:
CPDT では、これらの問題を解決するために PHOAS (Parametric HOAS) を導入するのだが、 Elpi では HOAS のままである。
どうやって解決しているかというと、たぶん以下のようにしているのだと思う。
Elpi の項の表現はなかなか強力で、weak head normal form を求める機構がライブラリとして実装されていたりする: elpi-reduction.elpi
ただ、現時点では相互再帰をサポートしていないようで、そこが残念ではある。 (README の Supported features of Gallina (core calculus of Coq) のところで mutual Inductive and CoInductive types と mutual fixpoints はチェックが入っていないし、試すとエラーになる)
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 の変数という意味の表示になっている。
最近、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 *)
SSReflect でも同じ方法で出現の番号を削れるだろう、ということでやってみた。
From mathcomp Require Import all_ssreflect.
Inductive TestNat01 : nat -> nat -> Type := C : TestNat01 0 1.
Lemma L a (H : TestNat01 a a) : False.
Proof.
(*
1 goal
a : nat
H : TestNat01 a a
______________________________________(1/1)
False
*)
set i1 := {1}a in H.
set i2 := {1}a in H.
(*
1 goal
a : nat
i1, i2 := a : nat
H : TestNat01 i1 i2
______________________________________(1/1)
False
*)
move: (erefl : i1 = a) (erefl : i2 = a).
(*
1 goal
a : nat
i1, i2 := a : nat
H : TestNat01 i1 i2
______________________________________(1/1)
i1 = a -> i2 = a -> False
*)
case: H.
(*
1 goal
a : nat
i1, i2 := a : nat
______________________________________(1/1)
0 = a -> 1 = a -> False
*)
move=> H1 H2.
by subst a.
Qed.
まぁ、出現の番号を (あまり) 書かずに済むのはいいな。 あと、vanilla Coq の set と違って、H を context に置いたままで set できるのもいい。 ただ、それでも行数は増える。
ついでに、H と C の等式も作ってみるか。
Lemma L2 a (H : TestNat01 a a) : False.
Proof.
(*
1 goal
a : nat
H : TestNat01 a a
______________________________________(1/1)
False
*)
set i1 := {1}a in H.
set i2 := {1}a in H.
pose H' := H.
(*
1 goal
a : nat
i1, i2 := a : nat
H : TestNat01 i1 i2
H' := H : TestNat01 i1 i2
______________________________________(1/1)
False
*)
move: (erefl : i1 = a) (erefl : i2 = a)
(erefl : existT (fun j1 => sigT (TestNat01 j1)) i1 (existT (TestNat01 i1) i2 H') =
existT (fun j1 => sigT (TestNat01 j1)) a (existT (TestNat01 a) a H )).
(*
1 goal
a : nat
i1, i2 := a : nat
H : TestNat01 i1 i2
H' := H : TestNat01 i1 i2
______________________________________(1/1)
i1 = a ->
i2 = a ->
existT (fun j1 : nat => {x : nat & TestNat01 j1 x}) i1 (existT (TestNat01 i1) i2 H') =
existT (fun j1 : nat => {x : nat & TestNat01 j1 x}) a (existT (TestNat01 a) a H) -> False
*)
case: H'.
(*
1 goal
a : nat
i1, i2 := a : nat
H : TestNat01 i1 i2
______________________________________(1/1)
0 = a ->
1 = a ->
existT (fun j1 : nat => {x : nat & TestNat01 j1 x}) 0 (existT (TestNat01 0) 1 C) =
existT (fun j1 : nat => {x : nat & TestNat01 j1 x}) a (existT (TestNat01 a) a H) -> False
*)
subst i1 i2.
(*
1 goal
a : nat
H : TestNat01 a a
______________________________________(1/1)
0 = a ->
1 = a ->
existT (fun j1 : nat => {x : nat & TestNat01 j1 x}) 0 (existT (TestNat01 0) 1 C) =
existT (fun j1 : nat => {x : nat & TestNat01 j1 x}) a (existT (TestNat01 a) a H) -> False
*)
move=> H1 H2 H3.
subst a.
move: (Eqdep_dec.inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ H3) => H4.
(*
1 goal
H : TestNat01 0 0
H3 : existT (fun j1 : nat => {x : nat & TestNat01 j1 x}) 0 (existT (TestNat01 0) 1 C) =
existT (fun j1 : nat => {x : nat & TestNat01 j1 x}) 0 (existT (TestNat01 0) 0 H)
H2 : 1 = 0
H4 : existT (TestNat01 0) 1 C = existT (TestNat01 0) 0 H
______________________________________(1/1)
False
*)
Abort.
existT の等式の中での出現の番号を書かなくていいのはよい。
あぁ、TestNat01 a a には要素がないから、C = H の等式は作れないのだな。 existT _ 1 C = existT _ 0 H という形になって行き詰まった。
ふむ、これは subst a が H1 : 0 = a を使って a を 0 にしたために外側の existT では両辺のインデックスが 0 になって一致したから 外側を Eqdep_dec.inj_pair2_eq_dec で外せたのであって、 もし H2 : 1 = a を使っていたなら、外側が外せなくて行き詰まるのだろう、な。
それはそれとして existT の等式を自分で書くのは面倒くさい。
出現の番号を書きたくないよなぁ、としばらく考えて、eq_refl に cast で型を付記すればいいんじゃないのか、と思いついて以下を書いた。
Inductive TestNat01 : nat -> nat -> Type := C : TestNat01 0 1.
Lemma L a (H : TestNat01 a a) : False.
Proof.
revert H.
(*
1 goal
a : nat
______________________________________(1/1)
TestNat01 a a -> False
*)
set (i1 := a) at 1.
set (i2 := a) at 1.
intros H.
(*
1 goal
a : nat
i1, i2 := a : nat
H : TestNat01 i1 i2
______________________________________(1/1)
False
*)
generalize (eq_refl : i1 = a), (eq_refl : i2 = a).
(*
1 goal
a : nat
i1, i2 := a : nat
H : TestNat01 i1 i2
______________________________________(1/1)
i1 = a -> i2 = a -> False
*)
case H.
(*
1 goal
a : nat
i1, i2 := a : nat
H : TestNat01 i1 i2
______________________________________(1/1)
0 = a -> 1 = a -> False
*)
Show Proof.
(*
(fun (a : nat) (H : TestNat01 a a) =>
(let i1 := a in
let i2 := a in
fun H0 : TestNat01 i1 i2 =>
match H0 in (TestNat01 n n0) return (n = a -> n0 = a -> False) with
| C => ?Goal@{H:=H0}
end (eq_refl : i1 = a) (eq_refl : i2 = a)) H)
*)
intros H1 H2.
subst a.
discriminate.
Qed.
出現番号を書くのは、最初に TestNat01 a a を set (i1 := a) at 1 と set (i2 := a) at 1 で TestNat01 i1 i2 にしているところだけで済んでいる。
なお、上記の場合は i1 と i2 は両方 at 1 で済んでいるが、帰納型にパラメータがあって、パラメータ部分にインデックスの項が含まれていると、指定する出現番号は 2以上にしないといけないかもしれない。
これならそんなに面倒ではない気がする。
よく考えたら、return 節には任意の項が記述できるわけで、 それをどんなものでも生成できるかといえばそれはできない。
たとえば、コンストラクタによって条件分岐して別の conclusion を生成することもできるが、 そういうのを生成できないのは当然だし、そもそもそんなことは期待していない。
ここで考えているのは、conclusion の一部を as, in で束縛した変数に置き換えただけの項を return 節に与えるときに、 どんな置き換え方をしたものでも生成できるか、という話である。
帰納型の場合分け tactic の違いをまとめると以下のようになる。
SSReflect でも、inversion に相当する match 式を生成することは可能である。 インデックス毎に等式を生成してから場合分けして左辺だけを置換すればいい。 この方法を拡張して、場合分けの対象の等式も生成することができ、場合分けで判明するすべての情報を得ることができる。 (これを自動的にやってくれる tactic があるといいんだけど。)
SSReflect に inversion 相当の tactic がない理由を説明しているメールを紹介した。 そこで述べられている方法も、inversion のかわりに使える。
case (SSReflect) と case (vanilla Coq) では、任意の match 式を構築できる。 (ただし case (vanilla Coq) で置換対象を制御するのはかなり面倒くさい) なので上記の、場合分けの対象の等式を生成するのは、vanilla Coq の case でも可能なはずである。
vanilla Coq では (場合分けの tactic で) どんな match 式でも生成できるだろうか。 どの場合分け tactic もインデックスの置換の場所を指定することはできないので、簡単ではなさそうである。
SSReflect では可能だった TestNat01 について試してみよう。
Inductive TestNat01 : nat -> nat -> Type := C : TestNat01 0 1. Lemma L a (H : TestNat01 a a) : False. Proof.
SSReflect では move: (erefl a) (erefl a) として a = a という等式をふたつ作ったが、vanilla Coq ではこれを generalize で行える。
generalize (eq_refl a), (eq_refl a). (* 1 goal a : nat H : TestNat01 a a ______________________________________(1/1) a = a -> a = a -> False *)
問題はここからである。 vanilla Coq の場合分け tactic はインデックスの置換を無差別に行うので、これをどうにかして制御する必要がある。 ひとつの方法は、case は conclusion しか置換しないので、置換したくないものは set tactic で context に移してしまうという方法が考えられる。 ただ、ふたつのインデックスが同じく a なので、これらを区別できるようにしなければならない。 ということで、各インデックスを別の変数に置き換える。 また、インデックスといっしょに置き換えたいものもその変数に置き換えておくことにする。 (なお、destruct は context 内も置換するため、この方法に destruct は使えない。)
まず H を conclusion に動かす。
revert H. (* 1 goal a : nat ______________________________________(1/1) TestNat01 a a -> a = a -> a = a -> False *)
そして、1,3番目の a を a1 という新しい変数に置換し、 2,5番目の a を a2 という新しい変数に置換する。
TestNat01 a a -> a = a -> a = a -> False
1 2 3 4 5 6
set (a1 := a) at 1 3.
set (a2 := a) at 1 3.
(*
1 goal
a : nat
a1, a2 := a : nat
______________________________________(1/1)
TestNat01 a1 a2 -> a1 = a -> a2 = a -> False
*)
なお、a2 で at 2 5 ではなく at 1 3 になっているのは、a1 の置換により、以下のように番号がずれるためである。
TestNat01 a1 a -> a1 = a -> a = a -> False
1 2 3 4
ということで、set (a1 := a) at 1 3 と set (a2 := a) at 1 3 としている
ここでの新しい変数の導入には set tactic を使っている。 set は証明項として let-in を構築する。 let-in で束縛された変数は context においては a1, a2 := a : nat の ":= a" のように定義の形になり、 型検査において定義を展開できるため、変数の導入前と同じく型検査できる。 つまり、型は壊れない。
case で場合分けをするには対象が context になければならないので H を context に動かす。
intros H. (* 1 goal a : nat a1, a2 := a : nat H : TestNat01 a1 a2 ______________________________________(1/1) a1 = a -> a2 = a -> False *)
で、case H すると、期待通りに 0 = a, 1 = a になっている。
case H. (* 1 goal a : nat a1, a2 := a : nat H : TestNat01 a1 a2 ______________________________________(1/1) 0 = a -> 1 = a -> False *)
証明項は以下のようになっっていて、期待通りに match H0 in (TestNat01 n n0) return (n = a -> n0 = a -> False) with となっている。 また、a1, a2 が let-in で束縛されていることもわかる。
Show Proof.
(*
(fun (a : nat) (H : TestNat01 a a) =>
(let a1 := a in
let a2 := a in
fun H0 : TestNat01 a1 a2 =>
match H0 in (TestNat01 n n0) return (n = a -> n0 = a -> False) with
| C => ?Goal@{H:=H0}
end) H eq_refl eq_refl)
*)
あとは、0 = a, 1 = a を context に動かして、a を subst で除去すると 1 = 0 が残るので discriminate で証明が完了する。
intros H1 H2. subst a. discriminate. Qed.
というわけで、set tactic で各インデックスに別の変数をわりあてれば、 vanilla Coq の case でも所望の match 式を生成できた。
この置換したいところだけ別の変数に変えておくというやりかたを使えば、 インデックスの置換を完全に制御できて、 任意の match 式を生成できると思う。 (必要ならインデックスだけでなく、場合分けの対象の置換も同様に制御できると思う)
もちろん、この場合には inversion や refine をつかえばもっと簡単に所望の match 式を生成できる。
simple inversion を使えば以下の等式を生成できるし、inversion ならいきなり証明が終わる。
H0 : 0 = a H1 : 1 = a
refine なら、以下のように直接 match 式を記述することもできる。
refine (match H in TestNat01 x y return x = a -> y = a -> False with C => _ end). (* 1 goal a : nat H : TestNat01 a a ______________________________________(1/1) 0 = a -> 1 = a -> False *)
なのでわざわざ case でやる必要はないのだが、case でも可能である、ということがわかった。 inversion では作ってくれない等式を生成するときなどには使えるかもしれない。 まぁ、refine で match 式を直接書いた方が簡単な気はするけれど。
SSReflect の case では、インデックスについてもどの出現を置換するかを指定できるので、任意の match 式を生成できそうである。
ただ、ひとつ気になるところとして、場合分け対象のインデックスが複数あり、それらが同じ項だった場合にちゃんと制御できるのか、という点がある。 結論からいうと、これは可能である。
From mathcomp Require Import all_ssreflect.
以下の帰納型 TestNat01 を考える。 これにはインデックスがふたつあり、コンストラクタ C でのみ値が生成され、そのときのインデックスは 0 と 1 である。
Inductive TestNat01 : nat -> nat -> Type := C : TestNat01 0 1.
そして、(H : TestNat01 a a) を前提とした証明を考えよう。 ふたつのインデックスはどちらも a となっているが、1番目のインデックスは 0 でなければならず、2番目のインデックスは 1 でなければならないので、TestNat01 a a には要素はなく、 ありえない前提が与えられていることになる。 この矛盾を (inversion を使わずに) 取り出してみよう。
Lemma L a (H : TestNat01 a a) : False. Proof.
ふたつのインデックスそれぞれに等式が欲しいので、a = a という等式をふたつ作る。
move: (erefl a) (erefl a). (* 1 goal a : nat H : TestNat01 a a ______________________________________(1/1) a = a -> a = a -> False *)
そして、H で場合分けするのだが、その際に a = a -> a = a -> の中の、1番目の a を 1番目のインデックスで置換し、3番目の a を 2番目のインデックスで置換する。 そうすると、0 = a と 1 = a という等式が得られる。
case: {1}_ {3}_ / H.
(*
1 goal
a : nat
______________________________________(1/1)
0 = a -> 1 = a -> False
*)
以下のように、証明項では return 節に (beta reduction すると) n = a -> n0 = a -> False という項が与えられていて、 期待通りに置換する指定にできている。
Show Proof. (* (fun (a : nat) (H : TestNat01 a a) => (fun _evar_0_ : (fun n n0 : nat => fun=> n = a -> n0 = a -> False) 0 1 C => match H as t in (TestNat01 n n0) return ((fun n1 n2 : nat => fun=> n1 = a -> n2 = a -> False) n n0 t) with | C => _evar_0_ end) ?Goal (erefl a) (erefl a)) *)
top assumption の 0 = a を使って 1 = a の a を 0 に書き換えれば 1 = 0 となって矛盾となるので証明は成功する。
by move=> <-. Qed.
というわけで、たぶん、SSReflect の case はどんな match 式でも生成できると思う。
項 t の型がインデックス付き帰納型だったとしよう。
inversion t ではインデックスの等式が得られるが、t がどんなコンストラクタで作られたかの情報はわからない。
dependent inversion t では、インデックスの等式が得られ、さらに t がコンストラクタで作られる項に置換される。
なので、dependent inversion は場合分けによって得られるすべての情報が得られて素晴らしい、 と言いたいところだが、残念ながら t の置換はうまくいかないことが多い。 というのは、インデックス付き帰納型の場合、t とコンストラクタで作られる項は型が違う (convertible でない) ため、 置換でしばしば型が壊れるからである。
そこで、場合分けの対象も等式で表現することを考える。 対象がインデックス付き帰納型の場合、この等式は型を合わせるために existT の等式としなければならない。
たとえば、le の定義は次であった。
Print le. (* Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m. *)
ここで、H : le a b を inversion したとき、 H が le_n で作られた場合は a = b という等式が得られ、 le_S で作られた場合は S m = b という等式が得られる。
さらに、 H が le_n で作られた場合は le_n a = H という等式、 le_S で作られた場合は le_S a m = H という等式が欲しい。
しかしこれは型があわないので、 existT (le a) a (le_n a) = existT (le a) b H と existT (le a) (S m) (le_S a m H') = existT (le a) b H という等式とする。
そして、conclusion に含まれる H は置換したくない。 どうせそのまま置換すると型が壊れるので、上の等式で後から書き換えればいい。
これを行うには、以下のようにすればよい。
From mathcomp Require Import all_ssreflect.
Lemma L (a b : nat) (H : le a b) : H = H.
Proof.
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
H = H
*)
move: (erefl (existT (le a) b H)).
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
existT (le a) b H = existT (le a) b H -> H = H
*)
case: {1}_ / {1}H.
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/2)
existT (le a) a (le_n a) = existT (le a) b H -> H = H
______________________________________(2/2)
forall (m : nat) (l : (a <= m)%coq_nat), existT (le a) m.+1 (le_S a m l) = existT (le a) b H -> H = H
*)
Abort.
ここでは、move: (erefl (existT (le a) b H)) として existT (le a) b H = existT (le a) b H という等式を生成し、その左辺の b, H を case: {1}_ / {1}H で置換している。
その結果、ふたつのサブゴール (le_n の場合と le_S の場合) ができていて、 それぞれで existT (le a) a (le_n a) = existT (le a) b H と existT (le a) m.+1 (le_S a m l) = existT (le a) b H という等式が得られている。
ここではインデックスについての等式 a = b と S m = b は生成していない。 これは existT の等式から EqdepFacts.eq_sig_fst で得られるからである。
生成したければ以下のようにすればよい。 ただし、出現の番号については conclusion を (notation を抑制し、implicit arguments を表示し) 確認して調べる必要がある。
move: (erefl b) (erefl (existT (le a) b H)).
case: {1 3}_ / {1}H.
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/2)
a = b -> existT (le a) a (le_n a) = existT (le a) b H -> H = H
______________________________________(2/2)
forall (m : nat) (l : (a <= m)%coq_nat), m.+1 = b -> existT (le a) m.+1 (le_S a m l) = existT (le a) b H -> H = H
*)
これを自動的にやってくれる tactic があればいいんだけど、どうかなぁ。 simple inversion の拡張とかどうかな。
case (SSReflect) は (次に述べるようにどんな match 式でも生成できるので) プリミティブとしてはよいのだが、 インデックス付き帰納型の場合分けを常に失敗せずに進められる tactic があればそれはそれでよいことだと思う。 (既存の tactic は失敗したり、必要な情報を得られないこともあるので、常に成功する、場合分けで得られる情報がすべて入手できる tactic があってもいいではないか。)
SSReflect では、「move: (erefl b) で b = b という等式を生成し、case: {1}b / {-}H でその等式の左辺の b だけを置換する」ということで inversion と同じ等式を生成できたが、 上のメールをみると、違う機能が示されているので、もしかしたら、そっちを使った方が簡単かもしれない。 というわけで試してみた。
試してみると、対象が H : le a b の場合、simple inversion H に相当する動作は case E: {-}_ / {-}H => [|m H'] で可能なようだ。
From mathcomp Require Import all_ssreflect.
Lemma L (a b : nat) (H : le a b) : H = H.
Proof.
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
H = H
*)
Show Proof.
(*
(fun (a b : nat) (H : (a <= b)%coq_nat) => ?Goal)
*)
case E: {-}_ / {-}H => [|m H'].
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
E : b = a
______________________________________(1/2)
H = H
______________________________________(2/2)
H = H
*)
Show 2.
(*
goal 2 is:
a, b : nat
H : (a <= b)%coq_nat
m : nat
H' : (a <= m)%coq_nat
E : b = m.+1
============================
H = H
*)
Show Proof.
(*
(fun (a b : nat) (H : (a <= b)%coq_nat) =>
(fun (_evar_0_ : (fun n : nat => fun=> protect_term (b = n) -> H = H) a (le_n a))
(_evar_0_0 : forall (m : nat) (l : (a <= m)%coq_nat),
(fun n : nat => fun=> protect_term (b = n) -> H = H) m.+1 (le_S a m l)) =>
match H as l in (_ <= n0)%coq_nat return ((fun n : nat => fun=> protect_term (b = n) -> H = H) n0 l) with
| @le_n _ => _evar_0_
| @le_S _ m l => _evar_0_0 m l
end) ((fun E : b = a => ?Goal) : protect_term (b = a) -> H = H)
(fun (m : nat) (H' : (a <= m)%coq_nat) => (fun E : b = m.+1 => ?Goal0) : protect_term (b = m.+1) -> H = H)
(erefl b))
*)
Abort.
ふたつのサブゴールにそれぞれ E : b = a と E : b = m.+1 が得られているので、simple inversion と同じ等式が前提として得られている。(左右は逆だけど)
証明項の match 式は match H as l in (_ <= n0)%coq_nat return ((fun n : nat => fun=> protect_term (b = n) -> H = H) n0 l) with となっている。 protect_term というのが入っているが、これは id と同じようなので、期待した match 式が生成されている。
ただ、等式を複数作る場合については、うまくいかなかった。 以下のように試したのだが、move Eb: b => ib として等式を作ると conclusion 内の b が ib に変わる。 そして H : TestNat2 a ib について場合分けを行うと、ib が置換されて b = 2 が得られるのだが、 H の型は TestNat2 a ib なので、b = 2 が得られても、H との関係が消えている。
From mathcomp Require Import all_ssreflect.
Inductive TestNat2 : nat -> nat -> Type := C2 : TestNat2 1 2.
Lemma L (a b : nat) (H : TestNat2 a b) : H = H.
Proof.
(*
1 goal
a, b : nat
H : TestNat2 a b
______________________________________(1/1)
H = H
*)
Show Proof.
(*
(fun (a b : nat) (H : TestNat2 a b) => ?Goal)
*)
move: H.
move Eb: b => ib.
move=> H.
case Ea: {-}_ {1}_ / {-}H Eb => Eb.
(*
1 goal
a, b, ib : nat
H : TestNat2 a ib
Ea : a = 1
Eb : b = 2
______________________________________(1/1)
H = H
*)
Show Proof.
(*
(fun a b : nat =>
[eta (fun (ib : nat) (Eb : b = ib) (H0 : TestNat2 a ib) =>
(fun _evar_0_ : (fun n n0 : nat => fun=> protect_term (a = n) -> b = n0 -> H0 = H0) 1 2 C2 =>
match
H0 as t in (TestNat2 n n0)
return ((fun n1 n2 : nat => fun=> protect_term (a = n1) -> b = n2 -> H0 = H0) n n0 t)
with
| C2 => _evar_0_
end) ((fun (Ea : a = 1) (Eb0 : b = 2) => ?Goal@{H:=H0; Eb:=Eb0}) : protect_term (a = 1) -> b = 2 -> H0 = H0)
(erefl a) Eb) b (erefl b)])
*)
Abort.
H と b の関係に興味が無いのであれば、これでいいのかもしれない。
H と b の関係が必要ならば b = ib という等式をコピーして残しておけば可能である。 これは以下のように move: (Eb) => Eb' とすればできる。
move: H.
move Eb: b => ib.
move: (Eb) => Eb'.
move=> H.
case Ea: {-}_ {1}_ / {-}H Eb => Eb.
(*
1 goal
a, b, ib : nat
Eb' : b = ib
H : TestNat2 a ib
Ea : a = 1
Eb : b = 2
______________________________________(1/1)
H = H
*)
subst ib.
(*
1 goal
a, b : nat
H : TestNat2 a b
Ea : a = 1
Eb : b = 2
______________________________________(1/1)
H = H
*)
しかし、こんな迂遠なことをするくらいなら、move: (erefl ...) で等式を作って場合分けしたほうが簡単だと思う。 そうすれば 2行で済む。
あと、結局 case Ea: {-}_ {1}_ / {-}H Eb => Eb のところでは出現の番号をひとつ書く必要があって、 出現番号が不要になってないし。
でも考えてみると、{1}_ と書かないといけないのは、H = H が @eq (TestNat2 a ib) H H であるために ib が conclusion に出現しているからで、 場合分けの対象が conclusion に含まれていなければ、出現の番号を書かなくてもいい気はする。
件のメールは inversion 相当のことをする方法という話だったら、 インデックスについての等式さえ得られればいい、という想定だったのかもしれない。
上記のように、inversion 相当の動作を SSReflect で行うことは可能である。 また、SSReflect を使っていても、vanilla Coq の tactic が技術的に禁止されているわけではないので inversion 自体を使うことはできる。
しかし、SSReflect の流儀 (自動的に変数名をつけないとか) にしたがった動作をする tactic がない、という点について戸惑うユーザは少なくないと思う。 この理由について、以下のメールで説明がされている。
inversion と同等の機能実現する部品を用意している、という主張のようだ。
ではどうするか、というと、以下のように可能、と書いてある
このようにすることで手間は増えるけれど、変数の名前や、どんな等式を作るか、また不要な等式を作らない、などといった細い制御が可能になる、というのが利点。
そして帰納型の定義のところで、そもそもインデックス付き帰納型でなく、各コンストラクタに等式の証明をつけるのを容易にする記法 (of/&) も提供している。 (この部分は、そもそもインデックス付き帰納型を使わないほうがいい、という話だろう)
というように書いてある。
SSReflect には inversion 相当の tactic がないのだが、要するにインデックスに対応する等式を作って、場合分けで等式の左辺だけ置換すればいい、 と理解してしまえば、以下のようにすればよいことがわかる
From mathcomp Require Import all_ssreflect. Lemma L (a b : nat) (H : le a b) : H = H /\ b = b. Proof. (* 1 goal a, b : nat H : (a <= b)%coq_nat ______________________________________(1/1) H = H /\ b = b *) Show Proof. (* (fun (a b : nat) (H : (a <= b)%coq_nat) => ?Goal) *)
まず、simple inversion でどういうサブゴールが生成されるかを確認する。 もともとの conclusion の H = H /\ b = b はそのままなので、simple inversion は等式を加えるだけで、もともとの conclusion 内の置換は行わないことがわかる。
simple inversion H.
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
H0 : a = b
______________________________________(1/2)
H = H /\ b = b
______________________________________(2/2)
(a <= m)%coq_nat -> H = H /\ b = b
*)
Show 2.
(*
goal 2 is:
a, b : nat
H : (a <= b)%coq_nat
m : nat
H1 : m.+1 = b
============================
(a <= m)%coq_nat -> H = H /\ b = b
*)
Show Proof.
(*
(fun (a b : nat) (H : (a <= b)%coq_nat) =>
let H0 : (fun n : nat => n = b -> H = H /\ b = b) b :=
match H as _ in (_ <= n)%coq_nat return (n = b -> H = H /\ b = b) with
| @le_n _ => fun H0 : a = b => ?Goal
| @le_S _ m x => (fun (m0 : nat) (H0 : (a <= m0)%coq_nat) (H1 : m0.+1 = b) => ?Goal0@{m:=m0} H0) m x
end in
H0 (erefl b))
*)
Undo.
最初のサブゴール (le_n の場合) では H0 : a = b、後のサブゴール (le_S の場合) では H1 : m.+1 = b という前提が得られている。
Undo で simple inversion の前に戻ってから、 move: (erefl b) で b = b という等式を生成し、 case: {1}b / {-}H でその等式の左辺の b だけを置換する。
move: (erefl b).
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
b = b -> H = H /\ b = b
*)
case: {1}b / {-}H.
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/2)
a = b -> H = H /\ b = b
______________________________________(2/2)
forall m : nat, (a <= m)%coq_nat -> m.+1 = b -> H = H /\ b = b
*)
Show Proof.
(*
(fun (a b : nat) (H : (a <= b)%coq_nat) =>
(fun (_evar_0_ : (fun n : nat => fun=> n = b -> H = H /\ b = b) a (le_n a))
(_evar_0_0 : forall (m : nat) (l : (a <= m)%coq_nat),
(fun n : nat => fun=> n = b -> H = H /\ b = b) m.+1 (le_S a m l)) =>
match H as l in (_ <= n0)%coq_nat return ((fun n : nat => fun=> n = b -> H = H /\ b = b) n0 l) with
| @le_n _ => _evar_0_
| @le_S _ m l => _evar_0_0 m l
end) ?a ?a0 (erefl b))
*)
Abort.
simple inversion とこちらを比較すると、生成された等式が context に出てくるか、conclusion の assumption に出てくるか、 という違いはあるが、同じ前提が得られている。
また、証明項の match 式をみると、以下のように始まっている。
match H as _ in (_ <= n)%coq_nat return (n = b -> H = H /\ b = b) with match H as l in (_ <= n0)%coq_nat return ((fun n : nat => fun=> n = b -> H = H /\ b = b) n0 l) with
SSReflect のほうはちょっと複雑だが、beta reduction すると return n0 = b -> H = H /\ b = b となり、 (束縛変数の名前が n と n0 と違うのを無視すれば) どちらも同じ形となっている。 つまり、同じ場合分けをしているのである。
インデックスが複数あればその数だけ等式をつくり、 インデックスの中に依存があれば existT の等式にする必要があるが、 SSReflect で inversion と同様の場合分けを行うのはこうやって可能である。
ただ、出現の番号を記述する必要があるのは面倒くさいし、いくらか間違いやすいとは思う。
あと、inversion は等式を生成した後に等式を整理し、矛盾したサブゴールを解決してくれるが、上記の方法は 等式を生成するだけの simple inversion 相当の動作なので、そのへんは手動で行う必要がある。
インデックス付き帰納型を case (SSReflect) で場合分けしてみよう。 インデックス付き帰納型として、ここでは vanilla Coq の le (less than or equal) を使う。
From mathcomp Require Import all_ssreflect.
Lemma L (a b : nat) (E : b = b) (H : le a b) : H = H /\ a = b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : (a <= b)%coq_nat
______________________________________(1/1)
H = H /\ a = b
*)
Show Proof.
(* (fun (a b : nat) (E : b = b) (H : (a <= b)%coq_nat) => ?Goal) *)
case: H.
(*
2 goals
a, b : nat
E : b = b
______________________________________(1/2)
le_n a = le_n a /\ a = a
______________________________________(2/2)
forall (m : nat) (l : (a <= m)%coq_nat), le_S a m l = le_S a m l /\ a = m.+1
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : (a <= b)%coq_nat) =>
(fun (_evar_0_ : (fun (n : nat) (l : (a <= n)%coq_nat) => l = l /\ a = n) a (le_n a))
(_evar_0_0 : forall (m : nat) (l : (a <= m)%coq_nat),
(fun (n : nat) (l0 : (a <= n)%coq_nat) => l0 = l0 /\ a = n) m.+1 (le_S a m l)) =>
match H as l in (_ <= n0)%coq_nat return ((fun (n : nat) (l0 : (a <= n)%coq_nat) => l0 = l0 /\ a = n) n0 l) with
| @le_n _ => _evar_0_
| @le_S _ m l => _evar_0_0 m l
end) ?Goal ?Goal0)
*)
Abort.
場合分けの結果、conclusion にあった H はコンストラクタの形 (le_n と le_S) に置換され、 インデックス b は a と m.+1 に置換されている。
context の E : b = b の b は変わっておらず、context 内のインデックスは置換されないことがわかる。
証明項の match 式には (簡約すると) match H as l in (_ <= n0)%coq_nat return l = l /\ a = n0 with と記述されている。 つまり H で場合分けを行い、H = H /\ a = b の H と b が置換される。
なお、notation を外すと、 もとの conclusion は and (@eq (le a b) H H) (@eq nat a b) であり、 match には as l in (le _ n0) return and (@eq (le a n0) l l) (@eq nat a n0) と記述されている。
conclusion に、b と H の出現の番号を付記すると以下のようになる。 (eq の implicit argument の中に b が出現しているので、この番号を調べるには、notation を抑制し、implicit argument を表示する必要がある。)
and (@eq (le a b) H H) (@eq nat a b)
1 1 2 2
eq では第1引数が第2,3引数の型でなければならないので、 1番目の b と、1,2番目の H は、同時に置換しないと型があわなくなる。 しかし、2番目の b は、置換してもしなくても (型は nat のままなので) 型は壊れない。
1番目の b と 1,2番目の H だけを置換するには case: {1}b / {1 2}H とすればよい。 そうすると、構築される match 式は as l in (le _ n0) return and (@eq (le a n0) l l) (@eq nat a b) となって、最後の b は置換されなくなる。
逆に、2番目の b だけを置換するには case: {2}b / {-}H とすればよい。 そうすると、構築される match 式は as l in (le _ n0) return and (@eq (le a b) H H) (@eq nat a n0)) n0 l となって、最後の b だけが置換される。
どの出現も置換しないという occ_switch は {-} で指定可能なようだ。{} だと、(たぶん) clear_switch に解釈されて、ここでは受け付けられない。
あと、場合分けの対象の項がわかれば、その型からインデックスはわかるので、 case: {occurs_1}i1 ... {occurs_n}in / {occurs_t}term というのは case: {occurs_1}_ ... {occurs_n}_ / {occurs_t}term と書いても良い。
では、インデックスの項を明示的に記述できることに意味はないかというと、そうでもない。 この項は置換するところを探すというところで使われるが、型からわかるインデックスと convertible であるが、項としては異なる、というものを置換するときに利用できる。 以下の場合の b と 0 + b は convertible ではあるが、同じ項ではない。 H の型からインデックスは b とわかるが、あえて 0 + b を探させている。 そのため、H = H つまり @eq (le a b) H H の中に出現している b は置換されていない。 (implicit argument の中にあるので見えていないが、もし置換されていたら、型があわなくてエラーになっているはずである)
From mathcomp Require Import all_ssreflect.
Lemma L (a b : nat) (H : le a b) : H = H /\ a = (0 + b).
Proof.
Show Proof.
(* (fun (a b : nat) (H : (a <= b)%coq_nat) => ?Goal) *)
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
H = H /\ a = 0 + b
*)
case: (0 + b) / {-}H.
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/2)
H = H /\ a = a
______________________________________(2/2)
forall m : nat, (a <= m)%coq_nat -> H = H /\ a = m.+1
*)
Abort.まず、以下の状況で case (SSReflect) により case: n とした場合、n is used in hypothesis H. というエラーになる。 case (vanilla Coq) では、エラーにならずに場合分けしていたので、それとは挙動が異なる。
From mathcomp Require Import all_ssreflect. Lemma L (n : nat) (H : n = n) : n = n. Proof. (* 1 goal n : nat H : n = n ______________________________________(1/1) n = n *) case: n. (* n is used in hypothesis H. *)
これは case: n の ": n" の部分は discharge つまり case の前に context から conclusion に動かすという意味の指定であるが、 n を conclusion に単純に動かすと H : n = n の中で参照している n が使えなくなってしまうので、エラーになる。
ここで、ふたつの選択肢がある。
最初の「n に加えて H も discharge してから場合分けする」とするには case: n H とすればよい。
Lemma L (n : nat) (H : n = n) : n = n.
Proof.
Show Proof.
(* (fun (n : nat) (H : n = n) => ?Goal) *)
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
case: n H.
(*
2 goals
______________________________________(1/2)
0 = 0 -> 0 = 0
______________________________________(2/2)
forall n : nat, n.+1 = n.+1 -> n.+1 = n.+1
*)
Show Proof.
(*
(fun n : nat =>
[eta (fun (_evar_0_ : (fun n0 : nat => n0 = n0 -> n0 = n0) 0)
(_evar_0_0 : forall n0 : nat, (fun n1 : nat => n1 = n1 -> n1 = n1) n0.+1) =>
match n as n0 return ((fun n1 : nat => n1 = n1 -> n1 = n1) n0) with
| 0 => _evar_0_
| n0.+1 => _evar_0_0 n0
end) ?Goal ?Goal0])
*)
(*
(fun (n : nat) (H : eq n n) =>
(fun (_evar_0_ : (fun n0 : nat => forall _ : eq n0 n0, eq n0 n0) 0)
(_evar_0_0 : forall n0 : nat, (fun n1 : nat => forall _ : eq n1 n1, eq n1 n1) (S n0)) =>
match n as n0 return ((fun n1 : nat => forall _ : eq n1 n1, eq n1 n1) n0) with
| 0 => _evar_0_
| S n0 => _evar_0_0 n0
end) ?Goal ?Goal0 H)
*)
Abort.
case: n H とした後のゴールをみると、 0 = 0 -> 0 = 0 と forall n : nat, n.+1 = n.+1 -> n.+1 = n.+1 になっており、 H が conclusion に移動してから、H の中の n も含めて場合分けされていることがわかる。
証明項には、[eta ...] というのがあって項がどうなっているのかわかりにくいので notation を抑制して表示し直した結果もつけてある。 これを少し簡約して単純化すると、以下のようになっている。
(fun (n : nat) (H : eq n n) => match n as n0 return n0 = n0 -> n0 = n0 with | 0 => ?Goal | S n0 => ?Goal0 n0 end H)
これをみると、match ... end H というように関数適用の引数として H が出てきていて、discharge が行われているのがわかる。 これは destruct が context も含めて場合分けするのと同じである。
なお、destruct は場合分けした後で context に戻すが、case (SSReflect) ではそれは行わない。 それは、introduction tactical でユーザが記述できる。
また「n を discharge せずにそのまま場合分けする (case (vanilla Coq) のような動作)」を行うには、case に与える項を変数名でない項とすればよい。 具体的にはかっこでくって case: (n) とすればよい。
Lemma L (n : nat) (H : n = n) : n = n. Proof. Show Proof. (* (fun (n : nat) (H : n = n) => ?Goal) *) (* 1 goal n : nat H : n = n ______________________________________(1/1) n = n *) case: (n). (* 2 goals n : nat H : n = n ______________________________________(1/2) 0 = 0 ______________________________________(2/2) forall n0 : nat, n0.+1 = n0.+1 *) Show Proof. (* (fun (n : nat) (H : n = n) => (fun (_evar_0_ : (fun n0 : nat => n0 = n0) 0) (_evar_0_0 : forall n0 : nat, (fun n1 : nat => n1 = n1) n0.+1) => match n as n0 return ((fun n1 : nat => n1 = n1) n0) with | 0 => _evar_0_ | n0.+1 => _evar_0_0 n0 end) ?e ?e0) *) Abort.
discharge tactical を使った tactic: term というのは証明項として (_ term) を作るものである。 case: n と case: (n) はどちらも (_ n) という証明項をつくる。 ただ、discarge のときに context の変数名を記述した場合は context からその変数を取り除く、という動作が追加して発生する。 そのため、変数名を指定した場合は context から conclusion に移動したように見える。 また、context 内にその変数が使われていると、エラーにならざるを得ない。
というわけで、case: (n) とすれば、context から n を消さずに場合分けだけを行える。 これは、case (vanilla Coq) の動作に相当する。
SSReflect を使っていても vanilla Coq の case は利用可能である。
どう区別できるかというと、コロンがなく項がカンマ区切りでひとつ以上指定されているものが vanilla Coq で、 項がなにも指定されていないかコロンの後に指定されているものが SSReflect である。
(* vanilla Coq *) case term, ... (* SSReflect *) case case: term... case: term... / term... case E: term... => [...] 最後の case E: term... => [...] は、等式を生成する指定である。 context に E という名前で、(場合分け前の項) = (場合分け後の項) という等式の証明が追加される。 場合分け後の項はコンストラクタの形となるが、コンストラクタに引数があるなら、その名前を => [...] の部分で指定する。 たとえば、n の型が nat であれば、 case E: n => [|m]. は nat の場合分けを行ってふたつのゴールを生成するが、それぞれのゴールの context には E: n = 0 と E: n = m.+1 という等式が追加される。 (=> [...] の部分を省略すると、代わりにユーザが使えない変数が導入される) なお、conclusion の先頭の assumption を場合分けする場合は、等式を生成することはできないようだ。 まぁ、: term... の部分を消すと、case E => [...] になってしまうので、vanilla Coq の case に => をつけたものと区別できなくなるか。
SSReflect の case tactic は、以下の形式で利用できる。
case: {occurs_1}i1 ... {occurs_n}in / {occurs_t}term
この tactic は、帰納型の項 term を場合分けするが、 その帰納型のインデックス i1, ..., in については、 occurs_1, ..., occurs_n で指定される箇所を置換し、 term については occurs_t で指定される箇所を置換する。
また、場合分けで置換の対象になるのは conclusion のみである。
なお、SSReflect の : は discharge のための tactical (tactic を修飾するもの) であり、 tactic: term は tactic が動作する前に (_ term) という形の証明項を作る (term : T とすると、conclusion は T -> old_conclusion になる) という動作である、という説明がされることがある。 しかし、上記の {occurs_1}i1 ... {occurs_n}in / の部分を考えると、: と / のあいだの指示は、case が match 式を生成するのに必要な情報を提供していて、単純に case が動く前に discharge するというだけの tactical とはいえないと思う。 まぁ、/ 以降についてはそうなのだが。
dependent inversion という tactic がある。 inversion の同じく、これの match 式をつくる部分だけ動かす dependent simple inversion という tactic がある。
inversion はインデックスの等式を context に追加するが、 場合分けの対象がどのコンストラクタで生成されたのかという情報は残してくれない。
case は、場合分けの対象をコンストラクタの形に置換してくれるが、 インデックスの等式は作ってくれない。
dependent inversion はこの両方をしてくれる tactic である。
Lemma L (a b : nat) (H : a <= b) : H = H.
Proof.
(*
1 goal
a, b : nat
H : a <= b
______________________________________(1/1)
H = H
*)
Show Proof.
(*
(fun (a b : nat) (H : a <= b) => ?Goal)
*)
dependent simple inversion H.
(*
2 goals
a, b : nat
H : a <= b
H0 : a = b
______________________________________(1/2)
le_n a = le_n a
______________________________________(2/2)
le_S a m l = le_S a m l
*)
Show 2.
(*
goal 2 is:
a, b : nat
H : a <= b
m : nat
l : a <= m
H0 : S m = b
============================
le_S a m l = le_S a m l
*)
Show Proof.
(*
(fun (a b : nat) (H : a <= b) =>
let H0 : (fun (b0 : nat) (H0 : a <= b0) => b0 = b -> H0 = H0) b H :=
match H as l in (_ <= n) return (n = b -> l = l) with
| le_n _ => fun H0 : a = b => ?Goal
| le_S _ m l => (fun (m0 : nat) (l0 : a <= m0) (H0 : S m0 = b) => ?Goal0@{m:=m0; l:=l0}) m l
end in
H0 eq_refl)
*)
Abort.
inversion と異なり、conclusion 内の H が le_n a や le_S a m l に置換されている。
また、H = H は @eq (le a b) H H であり、 le_n a = le_n a は @eq (le a a) (le_n a) (le_n a) である。 implicit argument で隠れているが、第1引数の le a b が le a a に変化している。 つまり、conclusion 内の b が a に置換されている。 まぁ、置換しないと le_n a = le_n a という等式の型があわないので、置換しているのだろう。
生成された match 式をみると、as l in (_ <= n) return (n = b -> l = l) となっていて、as 節と in 節が両方指定されている。 in (_ <= n) で束縛された n を使って、n = b という等式が記述されているのは inversion と同じである。 そして、as l で束縛された l が、conclusion 内の H の代わりに記述されており、これは case と同じである。
というしかけで、インデックスの等式と、場合分け対象の置換が両方行われる。
マニュアルに inversion は Prop なインデックスの等式はデフォルトでは生成しないが、 Set Keep Proof Equalities と設定すると生成する、と書いてある。
これを確認してみよう。
まず、Prop な依存型 DP を定義する。 (上記の D と同じだが、sort が Prop になっている)
Inductive DP {T : Type} : T -> Prop := DPC : forall (x : T), DP x.
この DP をインデックスに使った帰納型を定義して simple inversion すると、 おや、existT の等式が生成されている。 生成しないんじゃなかったのか?
Inductive Test7 : forall (a : nat) (b : DP a), Type := C7 : Test7 0 (DPC 0). Lemma L a b (t : Test7 a b) : False. Proof. simple inversion t. (* 1 goal a : nat b : DP a t : Test7 a b H : 0 = a H0 : existT (fun a : nat => DP a) 0 (DPC 0) = existT (fun a : nat => DP a) a b ______________________________________(1/1) False *) Abort.
simple inversion じゃなくて inversion ならどうか、ということで試すと、こっちは生成されない。 なるほど。 証明項をみると、生成しないのではなく、内部的には生成しているようだ。 それを表示しないようにしているのだろう。
Lemma L a b (t : Test7 a b) : False.
Proof.
inversion t.
(*
1 goal
a : nat
b : DP a
t : Test7 a b
H, H1 : 0 = a
______________________________________(1/1)
False
*)
Show Proof.
(*
(fun (a : nat) (b : DP a) (t : Test7 a b) =>
let H :
(fun (a0 : nat) (b0 : DP a0) =>
a0 = a -> existT (fun a1 : nat => DP a1) a0 b0 = existT (fun a1 : nat => DP a1) a b -> False) a b :=
match
t in (Test7 a0 b0)
return (a0 = a -> existT (fun a1 : nat => DP a1) a0 b0 = existT (fun a1 : nat => DP a1) a b -> False)
with
| C7 =>
fun (H : 0 = a) (H0 : existT (fun a0 : nat => DP a0) 0 (DPC 0) = existT (fun a0 : nat => DP a0) a b) =>
(fun (H1 : 0 = a) (H2 : existT (fun a0 : nat => DP a0) 0 (DPC 0) = existT (fun a0 : nat => DP a0) a b) =>
let H3 : 0 = a := f_equal (fun e : {a0 : nat & DP a0} => let (x, _) := e in x) H2 in
(fun H4 : 0 = a => let H5 : 0 = a := H4 in eq_ind 0 (fun _ : nat => False) ?Goal@{H:=H1; H1:=H4} a H5) H3) H
H0
end in
H eq_refl eq_refl)
*)
Abort.
なんか、f_equal を使っているが、これはなにかというと、existT (fun a : nat => DP a) 0 (DPC 0) = existT (fun a : nat => DP a) a b の証明から 0 = a の証明を取り出しているようだな。 その取り出した結果が H1 になっているのか。 そして、eq_ind で a を 0 に書き換えているが、もともとの conclusion の False に a は含まれないので、そこで変化は起きない。
それはそれとして、Keep Proof Equalities してから inversion してみよう。 こちらでは existT の等式が残っている。
Set Keep Proof Equalities.
Lemma L a b (t : Test7 a b) : False.
Proof.
inversion t.
(*
1 goal
a : nat
b : DP a
t : Test7 a b
H, H1 : 0 = a
H2 : existT (fun x : nat => DP x) 0 (DPC 0) = existT (fun x : nat => DP x) a b
______________________________________(1/1)
False
*)
Show Proof.
(*
(fun (a : nat) (b : DP a) (t : Test7 a b) =>
let H :
(fun (a0 : nat) (b0 : DP a0) =>
a0 = a -> existT (fun a1 : nat => DP a1) a0 b0 = existT (fun a1 : nat => DP a1) a b -> False) a b :=
match
t in (Test7 a0 b0)
return (a0 = a -> existT (fun a1 : nat => DP a1) a0 b0 = existT (fun a1 : nat => DP a1) a b -> False)
with
| C7 =>
fun (H : 0 = a) (H0 : existT (fun a0 : nat => DP a0) 0 (DPC 0) = existT (fun a0 : nat => DP a0) a b) =>
(fun (H1 : 0 = a) (H2 : existT (fun a0 : nat => DP a0) 0 (DPC 0) = existT (fun a0 : nat => DP a0) a b) =>
let H3 : existT (fun x : nat => DP x) 0 (DPC 0) = existT (fun x : nat => DP x) a b :=
f_equal
(fun e : {a0 : nat & DP a0} => let (x, d) := e in existT (fun x0 : nat => (fun a0 : nat => DP a0) x0) x d)
H2 in
(let H4 : 0 = a := f_equal (fun e : {a0 : nat & DP a0} => let (x, _) := e in x) H2 in
(fun (H5 : 0 = a) (H6 : existT (fun x : nat => DP x) 0 (DPC 0) = existT (fun x : nat => DP x) a b) =>
let H7 : existT (fun x : nat => DP x) 0 (DPC 0) = existT (fun x : nat => DP x) a b := H6 in
eq_ind (existT (fun x : nat => DP x) 0 (DPC 0)) (fun _ : {x : nat & DP x} => False)
?Goal@{H:=H1; H1:=H5; H2:=H6} (existT (fun x : nat => DP x) a b) H7) H4) H3) H H0
end in
H eq_refl eq_refl)
*)
Abort.
なんかさらに証明項が大きくなっている。 あまり読む気がしないが、f_equal が 2回、eq_ind が 1回使われている。 最初の f_equal は H2 から H3 を作っているが、型は同じでなんか意味が無さそう。 後の f_equal は Set Keep Proof Equalities しなかったときと同じく 0 = a の証明を取り出していている。 eq_ind は existT (fun x : nat => DP x) a b を existT (fun x : nat => DP x) 0 (DPC 0) に置き換えていると思うのだが、 そんな項は conclusion に含まれていないので意味は無い。
inversion はインデックスについて等式を作るが、 インデックスの中に依存型があったらどうなるか。 インデックスが match の外側と内側で違う (convertible でない) ので、 そういうインデックスに依存した型は、外側と内側で型が異なることになり、 ふつうに等式をつくると、型があわなくなるはずである。
以下のようにいろいろ試したところ、inversion はそういう場合に existT の等式を作るようだ。
まず、とりあえずどんな型の値でも型の中に取り込める帰納型 D を定義する。 D 1 とか D true とか、どんな値でもインデックスとして指定できる。
Inductive D {T : Type} : T -> Type := DC : forall (x : T), D x.
この D を使って、インデックスのところに (a : nat) (b : D a) と記述した帰納型をつくる。 インデックスがふたつあって、最初のインデックスが 2番目のインデックスの型に現れている。 これを simple inversion すると、等式が 2個生成される。 追加された等式だけをコメントで示しているが、 H : 0 = a が最初のインデックスの等式であり、 H0 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a b が 2番目のインデックスの等式である。
Inductive Test1 : forall (a : nat) (b : D a), Type := C1 : Test1 0 (DC 0). Lemma L a b (t : Test1 a b) : False. Proof. simple inversion t. (* H : 0 = a H0 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a b *) Abort.
2番目のインデックスは、match の外側では b, 内側では DC 0 なので、 素朴には DC 0 = b という等式を期待してしまうが、DC 0 : D 0 と b : D a では型が D 0 と D a と異なる (convertible でない) ので 等式 DC 0 = b は型がつかない。 そこで、その D 0 と D a の異なる部分 (0 と a) を existT で隠蔽して等式を作っている。 なお、existT (fun a : nat => D a) 0 (DC 0) と existT (fun a : nat => D a) a b は両方とも {x : nat & D x} という型である。 (notation を抑制すると、sigT (fun x : nat => D x) という型であることがわかる。) この型には 0 や a は出てこない。
次に、インデックスを (a : nat) (b : nat) (c : D (a, b)) としてみる。 1番目と2番目のインデックス (a, b) に 3番目のインデックス (c) の型が依存している。 そうすると、3個の等式のうち、3番目のインデックスだけが existT の等式になっている。 また、その等式では、existT がネストしており、依存しているインデックス a, b をそれぞれで隠蔽しているようだ。
Inductive Test2 : forall (a : nat) (b : nat) (c : D (a, b)), Type := C2 : Test2 0 0 (DC (0, 0)).
Lemma L a b c (t : Test2 a b c) : False.
Proof.
simple inversion t.
(*
H : 0 = a
H0 : 0 = b
H1 : existT (fun a : nat => {b : nat & D (a, b)}) 0 (existT (fun b : nat => D (0, b)) 0 (DC (0, 0))) =
existT (fun a : nat => {b : nat & D (a, b)}) a (existT (fun b : nat => D (a, b)) b c)
*)
Abort.
インデックスを (a : nat) (b : D a) (c : nat) (d : D c) としてみると、 依存型のインデクスの b, d に対応する等式が existT の形になっている。
Inductive Test3 : forall (a : nat) (b : D a) (c : nat) (d : D c), Type := C3 : Test3 0 (DC 0) 1 (DC 1). Lemma L a b c d (t : Test3 a b c d) : False. Proof. simple inversion t. (* H : 0 = a H0 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a b H1 : 1 = c H2 : existT (fun c : nat => D c) 1 (DC 1) = existT (fun c : nat => D c) c d *) Abort.
インデックスを (a : nat) (b : nat) (c : D a) (d : D b) と順番を変えても、 依存型のインデクスの c, d に対応する等式が existT の形になっている。
Inductive Test4 : forall (a : nat) (b : nat) (c : D a) (d : D b), Type := C4 : Test4 0 1 (DC 0) (DC 1). Lemma L a b c d (t : Test4 a b c d) : False. Proof. simple inversion t. (* H : 0 = a H0 : 1 = b H1 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a c H2 : existT (fun b : nat => D b) 1 (DC 1) = existT (fun b : nat => D b) b d *) Abort.
合流するとどうだろうか、ということでインデックスを (a : nat) (b : D a) (c : nat) (d : D c) (e : D (b, d)) としてみると 最後のインデックス e : D (b, d) に対応する等式は existT が 4重にネストして、a, b, c, d を隠蔽していることがわかる。
Inductive Test5 : forall (a : nat) (b : D a) (c : nat) (d : D c) (e : D (b, d)), Type :=
C5 : Test5 0 (DC 0) 1 (DC 1) (DC ((DC 0), (DC 1))).
Lemma L a b c d e (t : Test5 a b c d e) : False.
Proof.
simple inversion t.
(*
H : 0 = a
H0 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a b
H1 : 1 = c
H2 : existT (fun c : nat => D c) 1 (DC 1) = existT (fun c : nat => D c) c d
H3 : existT (fun a : nat => {b : D a & {c : nat & {d : D c & D (b, d)}}}) 0
(existT (fun b : D 0 => {c : nat & {d : D c & D (b, d)}}) (DC 0)
(existT (fun c : nat => {d : D c & D (DC 0, d)}) 1
(existT (fun d : D 1 => D (DC 0, d)) (DC 1) (DC (DC 0, DC 1))))) =
existT (fun a : nat => {b : D a & {c : nat & {d : D c & D (b, d)}}}) a
(existT (fun b : D a => {c : nat & {d : D c & D (b, d)}}) b
(existT (fun c : nat => {d : D c & D (b, d)}) c
(existT (fun d : D c => D (b, d)) d e)))
*)
Abort.
分岐、合流する場合は、ということで (a : nat) (b : D a) (c : D a) (d : D (b, c)) とすると、 最後のインデックス d : D (b, c) に対応する等式は existT が 3重にネストして、a, b, c を隠蔽していることがわかる。
Inductive Test6 : forall (a : nat) (b : D a) (c : D a) (d : D (b, c)), Type :=
C6 : Test6 0 (DC 0) (DC 0) (DC ((DC 0), (DC 0))).
Lemma L a b c d (t : Test6 a b c d) : False.
Proof.
simple inversion t.
(*
H : 0 = a
H0 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a b
H1 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a c
H2 : existT (fun a : nat => {b : D a & {c : D a & D (b, c)}}) 0
(existT (fun b : D 0 => {c : D 0 & D (b, c)}) (DC 0)
(existT (fun c : D 0 => D (DC 0, c)) (DC 0) (DC (DC 0, DC 0)))) =
existT (fun a : nat => {b : D a & {c : D a & D (b, c)}}) a
(existT (fun b : D a => {c : D a & D (b, c)}) b
(existT (fun c : D a => D (b, c)) c d))
*)
Abort.
inversion がどういう等式を作るかということを上記から推測すると、 各インデックスについて依存しているインデックスを調べて、 それを順に existT で隠蔽する、という仕掛けで作られているのではないかと思う。
なお existT を使えば、inversion の場合分け対象そのものの等式を生成することもできるはずだが、 そういう機能はなさそうである。
あと、simple inversion の後に証明を続けるときにどうするかであるが、existT の等式 E : existT D a x = existT D a' x' からは、 まず EqdepFacts.eq_sig_fst により a = a' を取り出せる。 これにより書き換えを行い、E : existT D a x = existT D a x' という形にできたら、 Eqdep_dec.inj_pair2_eq_dec により x = x' を取り出せる。 このとき公理は不要であるが、a の型に decidable equality が必要である。
まぁ、inversion はすべてのインデックスに等式を生成するので、EqdepFacts.eq_sig_fst で取り出さなくても その等式は別に生成されるため、EqdepFacts.eq_sig_fst は使わなくて済む気がする。
inversion は等式を生成する、というが、どんな等式を生成するかはマニュアルを読んでもはっきりしない。
Each such goal includes the hypotheses needed to deduce the proposition. と書いてあるが、 proposition を deduce するのに必要な hypotheses といわれても、具体性に欠ける。
まぁ、実際のところ、帰納型のインデックスについての等式を生成するのである。
たとえば、vanilla Coq で、自然数の less than or equal (<=) というのは le という帰納型で定義される。
Print le. (* Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m. *)
ここでは、a <= b は le a b の記法で、le の第1引数はパラメータで、第2引数がインデックスである。
p : le a b をコンストラクタ毎に場合分けすると、le_n a : le a a と le_S a m (_ : le a m) : le a (S m) になるので、 インデックスは le_n の場合 a, le_S の場合 S m になる。 なので、inversion はそれぞれの場合に a = b と S m = b という等式を生成する。
Lemma L (a b : nat) (E : b = b) (H : a <= b) : H = H /\ b = b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : a <= b
______________________________________(1/1)
H = H /\ b = b
*)
simple inversion H.
(*
2 goals
a, b : nat
E : b = b
H : a <= b
H0 : a = b
______________________________________(1/2)
H = H /\ b = b
______________________________________(2/2)
a <= m -> H = H /\ b = b
*)
Show 2.
(*
goal 2 is:
a, b : nat
E : b = b
H : a <= b
m : nat
H1 : S m = b
============================
a <= m -> H = H /\ b = b
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) =>
let H0 : (fun n : nat => n = b -> H = H /\ b = b) b :=
match H as _ in (_ <= n) return (n = b -> H = H /\ b = b) with
| le_n _ => fun H0 : a = b => ?Goal
| le_S _ m x => (fun (m0 : nat) (H0 : a <= m0) (H1 : S m0 = b) => ?Goal0@{m:=m0} H0) m x
end in
H0 eq_refl)
*)
Abort.
証明項の match 式をみると、in (_ <= n) return (n = b -> H = H /\ b = b) という形で型が指定されている。 in 節の in (_ <= n) によって、インデックスが n に束縛され、 return 節の型 n = b -> H = H /\ b = b の中で使われている。 n は match 式全体、各分岐それぞれで置換される。 match 式全体では match で場合分けの対象とした H : a <= b のインデックス b に n が置換されるので b = b -> H = H /\ b = b 型となる。 le_n の分岐では le_n a : a <= a のインデックス a に置換されるので、a = b -> H = H /\ b = b になる。 le_S の分岐では le_S a m _ : a <= (S m) のインデックス S m に置換されるので、S m = b -> H = H /\ b = b になる。
convoy pattern により、match 式の外側で生成した eq_refl : b = b という項が、 各分岐では、それぞれの等式の型となり、それを関数の引数として受けとっているので、context に等式が現れる。
また、context の E : b = b や、conclusion の H = H /\ b = b に含まれる b は置換されていない。
inversion は、各コンストラクタに場合分けして等式を追加し、等式を整理し、矛盾するゴールを除去する、という tactic である。 match 式が生成されるのは最初の部分で、その部分だけ行うのが simple inversion である。
destruct の対象がインデックス付き帰納型の項であった場合、 context と conclusion のインデックスをすべて置換するが、 そんな大雑把な方法では失敗することもあるだろうと思う。
というわけでしばらく考えた結果、以下のように destruct が失敗する例を作れた。
Definition f (m n : nat) := le m (S n). Lemma L a b (E : b = b) (H : le a (S b)) (H2 : f a b) : H = H2. Proof. destruct H. (* Abstracting over the terms "n" and "H" leads to a term fun (n0 : nat) (H0 : a <= n0) => H0 = H2 which is ill-typed. Reason is: Illegal application: The term "@eq" of type "forall A : Type, A -> A -> Prop" cannot be applied to the terms "a <= n0" : "Prop" "H0" : "a <= n0" "H2" : "f a b" The 3rd term has type "f a b" which should be a subtype of "a <= n0". *)
ここでは、f という関数を用意して、それを使って型を記述することにより、 S を表面上隠している。
destruct H はインデックスの S b を置換するが、f によって隠れた S により、H2 の型を変えることができず、 H = H2 という等式の型が壊れ、エラーになっている。
もっと単純にすると以下のようにもできる。 S の別名として S' をつくってS を隠し、インデックスの置換を防げば、失敗させることができる。 (S の別名を作るというのはあまり現実味がないかもしれないが)
Definition S' := S. Lemma L a b (E : b = b) (H : le a (S b)) (H2 : le a (S' b)) : H = H2. Proof. destruct H. (* Abstracting over the terms "n" and "H" leads to a term fun (n0 : nat) (H0 : a <= n0) => H0 = H2 which is ill-typed. Reason is: Illegal application: The term "@eq" of type "forall A : Type, A -> A -> Prop" cannot be applied to the terms "a <= n0" : "Prop" "H0" : "a <= n0" "H2" : "a <= S' b" The 3rd term has type "a <= S' b" which should be a subtype of "a <= n0". *)
インデックスをぜんぶ置換するというのは、インデックスが単純な変数ならうまくいくのだろうが、 それより複雑な項になると、うまくいかないことが出てくるのだと思う。
インデックス付き帰納型の場合分けを destruct でやってみよう。 destruct は context の中も置換するので、context 内の b は convoy pattern で置換されると予想できる。
Lemma L a b (E : b = b) (H : le a b) (H2 : H = H) : H = H /\ b = b /\ le a b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : a <= b
H2 : H = H
______________________________________(1/1)
H = H /\ b = b /\ a <= b
*)
destruct H.
(*
2 goals
a : nat
E : a = a
H2 : le_n a = le_n a
______________________________________(1/2)
le_n a = le_n a /\ a = a /\ a <= a
______________________________________(2/2)
le_S a m H = le_S a m H /\ S m = S m /\ a <= S m
*)
Show 2.
(*
goal 2 is:
a, m : nat
E : S m = S m
H : a <= m
H2 : le_S a m H = le_S a m H
============================
le_S a m H = le_S a m H /\ S m = S m /\ a <= S m
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) (H2 : H = H) =>
match H as l in (_ <= n) return (n = n -> l = l -> l = l /\ n = n /\ a <= n) with
| le_n _ => fun (E0 : a = a) (H3 : le_n a = le_n a) => ?Goal@{E:=E0; H2:=H3}
| le_S _ m l =>
(fun (m0 : nat) (H0 : a <= m0) (E0 : S m0 = S m0) (H3 : le_S a m0 H0 = le_S a m0 H0) =>
?Goal0@{m:=m0; E:=E0; H:=H0; H2:=H3}) m l
end E H2)
*)
Abort.
予想通り、context 内の H と b が置換されている。 そのために convoy pattern で E と H2 の型を変えている。
destruct に at をつけるとどうなるだろうか。
Lemma L a b (E : b = b) (H : le a b) (H2 : H = H) : H = H /\ b = b /\ le a b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : a <= b
H2 : H = H
______________________________________(1/1)
H = H /\ b = b /\ a <= b
*)
destruct H at 1.
(*
2 goals
a : nat
E : a = a
H : a <= a
H2 : H = H
______________________________________(1/2)
le_n a = H /\ a = a /\ a <= a
______________________________________(2/2)
le_S a m l = H /\ S m = S m /\ a <= S m
*)
Show 2.
(*
goal 2 is:
a, m : nat
E : S m = S m
H : a <= S m
H2 : H = H
l : a <= m
============================
le_S a m l = H /\ S m = S m /\ a <= S m
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) (H2 : H = H) =>
let l : a <= b := H in
match l as l0 in (_ <= n) return (n = n -> forall H0 : a <= n, H0 = H0 -> l0 = H0 /\ n = n /\ a <= n) with
| le_n _ => fun (E0 : a = a) (H0 : a <= a) (H3 : H0 = H0) => ?Goal@{E:=E0; H:=H0; H2:=H3}
| le_S _ m l0 =>
(fun (m0 : nat) (l1 : a <= m0) (E0 : S m0 = S m0) (H0 : a <= S m0) (H3 : H0 = H0) =>
?Goal0@{m:=m0; E:=E0; H:=H0; H2:=H3; l:=l1}) m l0
end E H H2)
*)
Abort.
destruct H at 1 としたので、conclusion 内の H は、1番目の出現だけがコンストラクタの形に置換されている。 インデックスは context, conclusion の両方ですべて置換されている。
まぁ、インデックスは context 内のも置換しておかないと、le_n a = H のような等式に型がつかないので、 インデックスはもともと context 内も含めてぜんぶ置換するというのが destruct の方針で、 at があってもなくてもそれは一貫している、ということかなぁ。
case の場合は (インデックス付きの場合に) context 内の置換の有無がいろいろ変わるので、 その一貫性のなさが美しくないとはいえるかもしれない。
あと、destruct では、eqn: 節により、(case_eq のような) 等式の生成が可能である。
Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
destruct n eqn:E.
(*
2 goals
n : nat
E : n = 0
H : 0 = 0
______________________________________(1/2)
0 = 0
______________________________________(2/2)
S n0 = S n0
*)
Show 2.
(*
goal 2 is:
n, n0 : nat
E : n = S n0
H : S n0 = S n0
============================
S n0 = S n0
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) =>
let n0 := n in
let E : n = n0 := eq_refl in
match n0 as n1 return (n = n1 -> n1 = n1 -> n1 = n1) with
| 0 => fun (E0 : n = 0) (H0 : 0 = 0) => ?Goal@{E:=E0; H:=H0}
| S n1 => (fun (n2 : nat) (E0 : n = S n2) (H0 : S n2 = S n2) => ?Goal0@{n0:=n2; E:=E0; H:=H0}) n1
end E H)
*)
Abort.
証明項をみると、(まずなぜか let n0 := n in で n0 という変数を導入した後) let E : n = n0 := eq_refl in で、n = n という等式の証明を E に束縛し、 convoy pattern で n = 0 と n = S n2 に変えている。
なお、eqn: をつけても、context 内の置換は行われるようだ。 H : n = n が 0 = 0 と S n0 = S n0 に変わっている。
(ちなみに、destruct n eqn:E at 1 というように、eqn: と at の両方をつけると、context 内の置換は抑制されるようである。)
case 同様、destruct でも at 節を使える。 しかし、意図したことかどうかはわからないが、at を使うと、context 内での置換はされなくなるようである。
Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
destruct n at 1.
(*
2 goals
n : nat
H : n = n
______________________________________(1/2)
0 = n
______________________________________(2/2)
S n0 = n
*)
Show 2.
(*
goal 2 is:
n : nat
H : n = n
n0 : nat
============================
S n0 = n
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) =>
let n0 := n in match n0 as n1 return (n1 = n) with
| 0 => ?Goal
| S n1 => (fun n2 : nat => ?Goal0@{n0:=n2}) n1
end)
*)
Abort.
destrct n at 1 の後では、0 と S の場合に分岐しているが、 context にある H : n = n はそのまま n = n として残っている。
まぁ、そもそも、at のところには conclusion の中での出現の番号を並べるというものなので、 context 内の各出現の置換を行うかどうかを指定できなさそうではある。
あと、証明項をみると、convoy pattern が使われていない。 context の H を変えないので、使う必要が無いのだろう。
destruct は、vanilla Coq の標準的な場合分け tactic である。
context 内の項を case は置換しなかったのに対し、destruct は置換するはずなので、それがわかるように試してみよう。
Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
destruct n.
(*
2 goals
H : 0 = 0
______________________________________(1/2)
0 = 0
______________________________________(2/2)
S n = S n
*)
Show 2.
(*
goal 2 is:
n : nat
H : S n = S n
============================
S n = S n
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) =>
match n as n0 return (n0 = n0 -> n0 = n0) with
| 0 => fun H0 : 0 = 0 => ?Goal@{H:=H0}
| S n0 => (fun (n1 : nat) (H0 : S n1 = S n1) => ?Goal0@{n:=n1; H:=H0}) n0
end H)
*)
Abort.
context 内にあった H : n = n が、destruct n の後では、H : 0 = 0 と H : S n = S n になっていて、 たしかに置換されている。
また、証明項をみると、これも convoy pattern を使っているようだ。
なお、context は goal の外側で束縛された変数であるが、 証明項における束縛変数の名前と、context 内の変数の名前の対応は好き勝手に変えることができる。 この証明項の ?Goal@{H:=H0} の H:=H0 はその対応を示している。 また、証明項の束縛変数を context から消すこともできる。 上の例では、外側の fun (n : nat) (H : n = n) => という部分で束縛された H は消えている。
(ちなみに、手動で変数の名前を変えるには rename tactic, 変数を消すには clear tactic を利用できる)
case_eq にインデックス付き帰納型の項を与えたらどうなるだろうか。
Lemma L a b (H : le a b) : le a b. Proof. (* 1 goal a, b : nat H : a <= b ______________________________________(1/1) a <= b *) case_eq H. (* 2 goals a, b : nat H : a <= b ______________________________________(1/2) le_n a = le_n a -> a <= a ______________________________________(2/2) forall (m : nat) (l : a <= m), le_S a m l = le_S a m l -> a <= S m *) Show Proof. (* (fun (a b : nat) (H : a <= b) => (match H as l in (_ <= n) return (l = l -> a <= n) with | le_n _ => ?Goal | le_S _ m l => ?Goal0 m l end : H = H -> a <= b) eq_refl) *) Abort.
えーと、le_n a = le_n a と le_S a m l = le_S a m l が追加されているんですが、なんですかねこれは。 両辺が同じで役に立たないんですが。
まぁ、単純に H = le_n a とかにするのは型があわないので無理ということはわかるのだが。
case at のように context を巻き込んで置換することはしないようだ。 でも役に立たない等式を加えるよりは (適切なエラーメッセージの) エラーにしてもらった方が嬉しいような気がする。
case_eq は、場合分けの際に、もともとの項と場合分け結果の等式を生成する機能を case tactic に加えた tactic である。
Lemma L (n : nat) (H : n < n) : n < n. Proof. (* 1 goal n : nat H : n < n ______________________________________(1/1) n < n *) Show Proof. (* (fun (n : nat) (H : n < n) => ?Goal) *) case_eq n. (* 2 goals n : nat H : n < n ______________________________________(1/2) n = 0 -> 0 < 0 ______________________________________(2/2) forall n0 : nat, n = S n0 -> S n0 < S n0 *) Show Proof. (* (fun (n : nat) (H : n < n) => (match n as n0 return (n = n0 -> n0 < n0) with | 0 => ?Goal | S n0 => ?Goal0 n0 end : n = n -> n < n) eq_refl) *) Abort.
conclusion が n < n のときに、case_eq n とすると、 n が 0 と S n0 の場合に場合分けされる。 0 の場合は n = 0 という assumption が追加され、 S n0 の場合は n = S n0 という assumption が追加される。
もともとの conclusion の n < n は 0 < 0 と S n0 < S n0 に置換される。
証明項をみると、どうやって等式を生成しているのかわかる。 match 式では as n0 return (n = n0 -> n0 < n0) となっているので、 この match 式全体の型は n = n -> n < n である。 それを、等式の左辺の n は置換せず、右辺の n は置換することにより、 各分岐の中では、 n とコンストラクタの等式になるようにしている。
match 式全体の型は、(なぜか) 証明項で match 式にキャストで型が明示されていて、n = n -> n < n と書いてあることからも分かる。
この match式の型は case_eq n 直前の conclusion とは異なり、n = n という assumption が付け加えられている。 これは、n = n 型の式 eq_refl を引数とする関数適用 (_ eq_refl) で match 式をくるむことで実現されている。
なお、case_eq は、case 同様、context 内の項は置換しない。 つまり、H : n < n の n は 0 や S n0 にはならない。
あと、case_eq は case と異なり、at 節は指定できないようだ。
なお、マニュアルでは case_eq よりも destruct の eqn: 節を使うのが勧められている。
case に at と eqn: をつけるかどうか、また、場合分け対象がインデックス付き帰納型かどうかで、context/conclusion のなにを置換するかをまとめてみた。
インデックス無し:
インデックス付き:
推測というか妄想になるが、最初は単に match を作るだけの tactic だったのが、 インデックス付き帰納型で at をサポートする都合により、 型をあわせるために (大雑把にも) コンテキスト内に出現するインデックスをすべて置換するようになって、 eqn: はなぜか destruct を使って実装され、 conclusion だけを変えるという当初の想定が崩れてよくわからない仕様になっている、という印象をもった。
まぁ、case (SSReflect) のように、インデックスを置換する箇所を指定できるようにして、どんな match 式でも生成できるようなプリミティブとして進化すればよかったのに、とは思う。
なお、後述する destruct では、context のインデックスはいつも置換するように一貫している。 まぁ、それがいいかというとそれはそれで問題なのだが。
case では、等式を生成する eqn: という指定ができる。
case H eqn:E2 として、等式を生成してみよう。
Lemma L a b (E : b = b) (H : le a b) (H2 : H = H) : H = H /\ b = b /\ le a b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : a <= b
H2 : H = H
______________________________________(1/1)
H = H /\ b = b /\ a <= b
*)
case H eqn:E2.
(*
2 goals
a : nat
E : a = a
H : a <= a
E2 : H = le_n a
H2 : le_n a = le_n a
______________________________________(1/2)
le_n a = le_n a /\ a = a /\ a <= a
______________________________________(2/2)
le_S a m l = le_S a m l /\ S m = S m /\ a <= S m
*)
Show 2.
(*
goal 2 is:
a, m : nat
E : S m = S m
H : a <= S m
l : a <= m
E2 : H = le_S a m l
H2 : le_S a m l = le_S a m l
============================
le_S a m l = le_S a m l /\ S m = S m /\ a <= S m
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) (H2 : H = H) =>
let l : a <= b := H in
let E2 : H = l := eq_refl in
match l as l0 in (_ <= n) return (n = n -> forall H0 : a <= n, H0 = l0 -> l0 = l0 -> l0 = l0 /\ n = n /\ a <= n) with
| le_n _ =>
fun (E0 : a = a) (H0 : a <= a) (E3 : H0 = le_n a) (H3 : le_n a = le_n a) => ?Goal@{E:=E0; H:=H0; E2:=E3; H2:=H3}
| le_S _ m l0 =>
(fun (m0 : nat) (l1 : a <= m0) (E0 : S m0 = S m0) (H0 : a <= S m0) (E3 : H0 = le_S a m0 l1)
(H3 : le_S a m0 l1 = le_S a m0 l1) => ?Goal0@{m:=m0; E:=E0; H:=H0; l:=l1; E2:=E3; H2:=H3}) m l0
end E H E2 H2)
*)
Abort.
ここでは context の場合分け対象 (H) とインデックスがぜんぶ置換されている。 たとえば、H2 : H = H が H2 : le_n a = le_n a に変わっている。
at をつけていないからといって、context 内の H までコンストラクタに置換するのはやりすぎな気がするが。 (気がついたのだが、GitHub coq/coq issue #19487: case with eqn: modifies hypotheses, destructing an expression that does not even appear in the goal という issue があって、 なんか、case eqn: は destruct で実装されているという話があるようだ)
なお、case H eqn:E2 at 1 として、eqn: と at を両方つけると、 インデックスは context と conclusion の両方、場合分け対象 (H) は conclusion 内の at で指定されたものだけが置換されるようだ。
case では、どこを置換するかを at で指定できる。
ここで case H at 1 として、H の 1番目の出現だけを場合分けするようにしてみよう。
Lemma L a b (E : b = b) (H : le a b) (H2 : H = H) : H = H /\ b = b /\ le a b. Proof. (* 1 goal a, b : nat E : b = b H : a <= b H2 : H = H ______________________________________(1/1) H = H /\ b = b /\ a <= b *)
以下を見ると、conclusion の H = H が le_n a = H になっているのは指定したとおりであるが、 考えてみるとちょっと奇妙で、le_n a は le a a 型で、H は le a b 型なので、型があわないはずである。 と思って context を確認すると、H の型が a <= a (つまり le a a) に変わっている。 というか、b が消えていて、E も a = a になっている。 あと、conclusion 内のすべての b が a に変わっている。 (2番目のゴールでは、すべての b が S m に変わっている)
case H at 1. (* 2 goals a : nat E : a = a H : a <= a H2 : H = H ______________________________________(1/2) le_n a = H /\ a = a /\ a <= a ______________________________________(2/2) le_S a m l = H /\ S m = S m /\ a <= S m *) Show 2. (* goal 2 is: a, m : nat E : S m = S m H : a <= S m H2 : H = H l : a <= m ============================ le_S a m l = H /\ S m = S m /\ a <= S m *)
case は context を変えないんじゃなかったのか、と思いつつ証明項をみると、以下のようになっている。
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) (H2 : H = H) =>
let l : a <= b := H in
match l as l0 in (_ <= n) return (n = n -> forall H0 : a <= n, H0 = H0 -> l0 = H0 /\ n = n /\ a <= n) with
| le_n _ => fun (E0 : a = a) (H0 : a <= a) (H3 : H0 = H0) => ?Goal@{E:=E0; H:=H0; H2:=H3}
| le_S _ m l0 =>
(fun (m0 : nat) (l1 : a <= m0) (E0 : S m0 = S m0) (H0 : a <= S m0) (H3 : H0 = H0) =>
?Goal0@{m:=m0; E:=E0; H:=H0; H2:=H3; l:=l1}) m l0
end E H H2)
*)
Abort.
ここでは、match 式が関数を返し、その関数に即座に E, H, H2 が引数として与えられ、 match 式で型が変えられ、各分岐で変えられた型の引数を受け取る、という形になっている。 return 節でその関数の引数の型が記述されるのだが、そこで置換がおこるようになっているために、 E, H, H2 を異なる型として受け取ることができている。 (こういうのを、convoy pattern という。) return 節の中で E は n = n となっているので、(n は in (_ <= n) で束縛されている変数なので) 両辺が置換される。 H, H2 も同様に、b が分岐の中でのインデックス (le_n の場合は a, le_S の場合は S m) になるように置換される。
まぁ、こうやって置換しないと、le_n a = H などは型が壊れるので、context も含めてやってくれるということだろう。
そして、どうやら、インデックスの置換は可能なすべての部分について行うようで、どこを置換するかを指定する機能はなさそうである。 (まぁ、conclusion はともかく、context のどこを変えるかを指定するのは番号だけでは難しそうである)
上の例だと、H のインデックスは b という変数だったので、変数 b を置換すれば、b を跡形もなく消すことができたが、 もっと複雑な項だとそれが可能とは限らない。。 そういう例として (H : le a (S b)) を試してみた。 インデックスが S b なので、S b を置換するはずだが、それだと S がついていない b は残るのではないかと思う。
Lemma L a b (E : b = b) (E2 : S b = S b) (H : le a (S b)) (H2 : H = H) : H = H /\ b = b /\ S b = S b /\ le a b. Proof. (* 1 goal a, b : nat E : b = b E2 : S b = S b H : a <= S b H2 : H = H ______________________________________(1/1) H = H /\ b = b /\ S b = S b /\ a <= b *)
以下のように H の 1番目の出現だけを場合分けすると、 やはり、context の E : b = b や、conclusion の b = b はそのまま残る。
case H at 1.
(*
2 goals
a, b : nat
E : b = b
E2 : a = a
H : a <= a
H2 : H = H
______________________________________(1/2)
le_n a = H /\ b = b /\ a = a /\ a <= b
______________________________________(2/2)
le_S a m l = H /\ b = b /\ S m = S m /\ a <= b
*)
Show 2.
(*
goal 2 is:
a, b : nat
E : b = b
m : nat
E2 : S m = S m
H : a <= S m
H2 : H = H
l : a <= m
============================
le_S a m l = H /\ b = b /\ S m = S m /\ a <= b
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (E2 : S b = S b) (H : a <= S b) (H2 : H = H) =>
let l : a <= S b := H in
let n := S b in
match
l as l0 in (_ <= n0) return (n0 = n0 -> forall H0 : a <= n0, H0 = H0 -> l0 = H0 /\ b = b /\ n0 = n0 /\ a <= b)
with
| le_n _ => fun (E3 : a = a) (H0 : a <= a) (H3 : H0 = H0) => ?Goal@{E2:=E3; H:=H0; H2:=H3}
| le_S _ m l0 =>
(fun (m0 : nat) (l1 : a <= m0) (E3 : S m0 = S m0) (H0 : a <= S m0) (H3 : H0 = H0) =>
?Goal0@{m:=m0; E2:=E3; H:=H0; H2:=H3; l:=l1}) m l0
end E2 H H2)
*)
Abort.
というわけで、case H at 1 は、H のインデックスである S b を可能な限り置換して a にするが、それだけでは b を消すことはできない。 また、a と b の関係 (le_n の場合 S b = a) は得られていない。
nat にはインデックスがなかったが、 インデックスがある帰納型として、le を例として case で場合分けを行ってみる。
le の定義は以下のとおりである。 これは 自然数の less than or equal を表現している。 vanilla Coq では le a b は a <= b という notation で表示される。 (SSReflect では (a <= b)%coq_nat と表示される。)
Print le. (* Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m. *)
ここでは、le の第1引数 n はパラメータで、第2引数 (名前はついていない) がインデックスである。
以下のように試す。 場合分けで、H 自身や b が置換されるかどうかを確認するため、context や conclusion に b = b や H = H を入れてある。
Lemma L a b (E : b = b) (H : le a b) (H2 : H = H) : H = H /\ b = b /\ le a b. Proof. (* 1 goal a, b : nat E : b = b H : a <= b H2 : H = H ______________________________________(1/1) H = H /\ b = b /\ a <= b *)
case H で場合分けすると、以下のように conclusion 内の H と b が置換される。 H は le_n a と le_S a m l に置換され、b は a と S m に置換される。 context 内の H, b は置換されない。
case H. (* 2 goals a, b : nat E : b = b H : a <= b H2 : H = H ______________________________________(1/2) le_n a = le_n a /\ a = a /\ a <= a ______________________________________(2/2) forall (m : nat) (l : a <= m), le_S a m l = le_S a m l /\ S m = S m /\ a <= S m *) Show 2. (* goal 2 is: a, b : nat E : b = b H : a <= b H2 : H = H ============================ forall (m : nat) (l : a <= m), le_S a m l = le_S a m l /\ S m = S m /\ a <= S m *)
証明項をみると、return 節が (l = l /\ n = n /\ a <= n) となっていて、l と n の部分が置換されることがわかる。 context の a, b, E, H, H2 は外側の束縛のままなので、なにも変わらないことも確認できる。
Show Proof. (* (fun (a b : nat) (E : b = b) (H : a <= b) (H2 : H = H) => match H as l in (_ <= n) return (l = l /\ n = n /\ a <= n) with | le_n _ => ?Goal | le_S _ m l => ?Goal0 m l end) *) Abort.
case (vanilla Coq) は、マニュアルで An older, more basic tactic to perform case analysis without recursion. と説明されていて、いちばん基本的な場合分け tactic である。
(destruct と違って) conclusion だけを変更し、context は変更しない、という説明もあるので、 それがわかるような例を作って証明項を調べてみよう。
Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) => ?Goal)
*)
case n.
(*
2 goals
n : nat
H : n = n
______________________________________(1/2)
0 = 0
______________________________________(2/2)
forall n0 : nat, S n0 = S n0
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) => match n as n0 return (n0 = n0) with
| 0 => ?Goal
| S n0 => ?Goal0 n0
end)
*)
Abort.
ここでは、context に (n : nat) (H : n = n) がある状態で n = n という conclusion を証明するという状態で、 case n を行っている。
証明項をみると、case n の直前には (fun (n : nat) (H : n = n) => ?Goal) だったのが、 case n により、?Goal のところに以下の match 式が生成されている。
match n as n0 return (n0 = n0) with | 0 => ?Goal | S n0 => ?Goal0 n0 end
証明項というのは、型が conclusion な項なので、 match 式の return 節は conclusion の n = n となる、のだが、 ここでは n が n0 に置き換わっている。 n0 は as n0 で束縛されている変数で、match 式全体の型としては n となり、 各分岐の型としてはコンストラクタ適用の形となる。
そのため、0 の分岐では 0 = 0 となり、 S の分岐では (S の引数が n0 であるとして) S n0 = S n0 となる。 (ここの n0 は、match 式が "| S n0 =>" の部分で束縛した変数であり、return 節のために "as n0" で束縛した変数とは別の変数である)
S の分岐では ?Goal0 n0 という項になっているので、?Goal0 には、n0 を受け取って S n0 = S n0 という型の値を返す関数を埋めなければならない。 なので、case n が生成した 2番めのゴールでは、conclusion が forall n0 : nat, S n0 = S n0 となっている。
ところで、case n は conclusion の n = n を n0 = n0 に変えたが、 ここの変え方は at 節で制御できる。
Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) => ?Goal)
*)
case n at 1.
(*
2 goals
n : nat
H : n = n
______________________________________(1/2)
0 = n
______________________________________(2/2)
S n0 = n
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) =>
let n0 := n in match n0 as n1 return (n1 = n) with
| 0 => ?Goal
| S n1 => (fun n2 : nat => ?Goal0@{n0:=n2}) n1
end)
*)
Abort.
今回は、case n at 1 として、場合分けの対象を n の 1番目の出現と指定した。 その結果、生成される match 式の as-return 節は as n1 return (n1 = n) となっており、 場合分けによってコンストラクタ適用に置換されるのは = の左辺だけとなっている。
なぜか match 式の外側に不要な let が入っているが... なんでかな? (想像としては、match 式の生成では conclusion に出現する n を無差別に置換するようになっていて、それを事前に let で別名に置き換えることで、置換するかどうかを制御しているとか?)
なお、case n at 2 とすると、as n1 return (n = n1) となる。
case n at 1 2 とすれば、at 1 2 を指定しない場合と同じに、= の両辺が置換される。(let は入る)
(fun (n : nat) (H : n = n) =>
let n0 := n in match n0 as n1 return (n1 = n1) with
| 0 => ?Goal
| S n1 => (fun n2 : nat => ?Goal0@{n0:=n2}) n1
end)
case n at と、番号を指定しない形は syntax error のようだ。 動作をするとしたら、置換を行わないという動作になると思うが、そうすると conclusion が変化しないので、意味が無いということだろう。
ところで、case は (destruct と違って) conclusion だけを変更し、local context は変更しない、という話がどうだったかというと、 context に入っている H : n = n はまったく変わっていないので、これは説明どおりに動作している。 また、conclusion を型とする match 式を生成するかぎりは、context (外側の変数束縛) が変わるはずもないので、これは match 式の生成というところからみると、基本的で、予想通りの動作といえるだろう。 単に match 式を生成する tactic を作ったら case tactic になりました、という感じである。
マニュアルを読むと、それぞれの機能は、だいたい以下のように説明されている
帰納型 D は以下のように定義される。
Inductive D params : forall targs, sort := | C1 fargs_1 : D params indexes_1 ... | Cn fargs_n : D params indexes_n
ここで、params と targs は 0 個以上の変数束縛であり、D の引数である。
D は引数として params と targs をとり、その結果は sort に属する型である。 そのため、params と targs の両方が空の場合は、ひとつの型を定義する。 そうでなく、params と targs のどちらかでも空でない場合は、0個以上の型からなる型族 (type family) を定義することになる。
コンストラクタ C1, ..., Cn は、この帰納型の値を定義する。 Ci は引数として params, fargs_i を受け取り、D params indexes_i 型の値となる。 コンストラクタの返値の型 D params indexes_i では、params は帰納型の params をそのまま指定しなければならない。 indexes_i は式であり、その中では params と fargs_i を使える。
ここで、D params targs 型の式 d の値がコンストラクタ Ci で作られた値だったとしよう。 Ci は、Ci params aargs_i という形で呼ばれ、その結果は D params indexes_i という型の値である。 つまり、d : D params targs と Ci params aargs_i : D params indexes_i が等しいはず、ということがわかる。 そして、それらの各部分が等しいので、以下のふたつが等しいことになる。 (targs と index_i は同数の要素を持ち、0 個以上なので、それぞれの要素が等しいことになる。)
この帰納型 d : D params targs を場合分けする match 式は以下のようになる。
match d as d' in D _ targs' return P targs' d' with | C1 ... => ... ... | Cn ... => ... end
ふつうの (ML とかの) match 式と似ているが、as d' in D _ targs' return P targs' d' の部分は Coq 特有のものである。
ふつうの match 式では、場合分けすると、コンストラクタの種類、およびその種類に応じたコンストラクタの引数が得られ、 それらを利用して分岐の中身を記述できる。 分岐の部分に書いた式の値が match 式の値となる。 Coq でもそれは同じである。
そして、ふつうの ML の match 式の型は、各分岐の型と等しい。 まぁ、各分岐の値が match 式の値になるので、値が等しいので型も等しい、ということである。
しかし Coq では、as d' in D _ targs' return P targs' d' の部分によって、 match 式全体の型、および各分岐の型を指定することができる。 といっても、各分岐の値が match 式の値になるので、分岐の型と match の型が同じはず、というのは同じで、 この指定は、型の一部分をそこと同じ値であるずの式に置き換える、という指定だけができるようになっている。 そうやって指定することで、結局のところ同じ型になる範囲で、型を変えることができる。
as d' in D _ targs' の部分で、d' と targs' が束縛され、 P targs' d' の部分には、型を書く。 この型の中では targs' や d' を使ってよい。(使わなくてもよい)
なお、in D _ targs' の targs' は targs と同数の束縛を書く。 あと、その前の _ は params と同数の _ を書くことになっている。 (params は分岐の返値の型にはそのまま記述することになっている、つまり分岐において変わらないことが保証されているので、そこを変えるための変数を束縛することはできない。)
match 式全体の型は P targs' d' の targs' と d' が targs と d に置換された結果となる。 コンストラクタ Ci に分岐した場合の型は、P targs' d' の targs' と d' が indexes_i と Ci params aargs_i に置換された結果となる。
Ci に分岐した場合は、(targs, d) は (indexes_i, Ci params aargs_i) に等しいので、結局は同じ型であり、 うまく P を作ると、それぞれが等しいという情報を分岐の中で利用できる。
ちょっと用語について確認しておく。
Coq < Lemma L (H : 0 = 0) : 1 = 1 -> 2 = 2 -> 3 = 3. 1 goal H : 0 = 0 ============================ 1 = 1 -> 2 = 2 -> 3 = 3
Coq では上のような表示を tactic でいじっていくのだが、 横線の上を context、下を conclusion という。 上の例では、context の中には H : 0 = 0 があり、 conclusion は 1 = 1 -> 2 = 2 -> 3 = 3 である。
context と conclusion をあわせて goal という。
また、conclusion の中の、-> の左の部分 (1 = 1 や 2 = 2) を assumption という。 とくに、いちばん左の assumption (1 = 1) を top assumption という。 (これは SSReflect の流儀にしたがっているつもりである)
なお、conclusion の部分を指して goal ということがある。 マニュアルにもそういう表現があるので、文脈に応じて察する必要がある。
なにが知りたいかというと、とくに、それぞれがどんな match 式を証明項として生成するのか理解したい。 帰納型の場合分けは結局は match 式なので、そこが本質である。
マニュアルを読んでそれぞれの tactic の位置づけを調べてみる。
まず、edestruct と ecase は、apply に対する eapply みたいなやつで、 existential variables を生成してもよい tactic のようだ。 たぶん、生成される match 式は destruct や case と変わらないと思う。
simple destruct ident はマニュアルに intros until ident; case ident と同じと書いてある。 match 式は case が生成するものと同じなのだろう。
dependent destruction は、JMeq を使うもので、 公理が必要になるので、とりあえず興味が無い。
inversion_clear は inversion した後で inversion が使った仮定を消すというものなので、 生成される match 式は inversion と同じだろう。 dependent inversion_clear も同様である。
inversion は、各コンストラクタに場合分けして等式を追加し、等式を整理し、矛盾するゴールを除去する、 という tactic なのだが、 match 式は最初の部分で生成される。 そして、simple inversion は inversion の最初の部分だけを行う tactic である。 なので、match 式の生成については simple inversion だけ調べればよい。 dependent inversion も、match 式の生成を行うのは dependent simple inversion だけ調べればよい。
というわけで、調べる対象は以下となった。
これらのどれを選んで使うのか、というのは自分でもよくわかっていない。 (まぁ、SSReflect に移行してしまったので、vanilla Coq の tactic をまじめに調べるモチベーションがほとんどなくなってしまったというのもあるが)
とくに vanilla Coq だと、 まず destruct を使って、それでうまく行かない (必要な情報が出てこない) なら、 destruct の eqn: オプション (あるいは case_eq) を使うとか、 inversion を試してみる、という感覚である。 どれがどう違うのかは、完全に理解しているとは言い難い。
SSReflect 流なら case 一択であるが、 inversion が必要になったときにはけっこう困る。 SSReflect には inversion に相当する (SSReflect 流の) tactic はない。 これは inversion がなにをするものなのかをちゃんと理解していないのが原因な気がする。
あと、refine で match 式を直接記述できるが、 他の tactic で生成できず、refine が絶対に必要な場合が存在するのかどうかというのも気になる。
というわけで、一念発起してそれぞれがどう違うのか調べてみた。
Coq で帰納型の式を各コンストラクタ毎に場合分けする tactic には case, destcut, inversion などさまざまなものがある。
Coq マニュアルの Reasoning with inductive types で、 場合分けを行う tactic は以下が載っている。 (用途が限定されすぎている tactic は除いてある)
また SSReflect には、(上記の vanilla Coq の case とは異なる) case tactic がある。 (vanilla Coq というのは、Coq/SSReflect と対比して、もともとの Coq を指す用語だと思う)
あと、任意の証明項を作る refine tactic がある。 これは場合分けをするためだけのものではないが、match 式を作れば場合分けを行える。