Coqはビルトインのタクティックの集合を持っています。reflexivity、intros、 inversionなどです。これらのタクティックだけで証明を構成することは可能ですが、 より強力なタクティックの集合を使うことで、生産性を飛躍的に上げることができます。 この章では、とても便利なのに、 いろいろな理由でデフォルトのCoqでは用意されていないたくさんのタクティックを説明します。 それらのタクティックは、LibTactics_J.vファイルに定義されています。

注記: SSReflect は強力なタクティックを提供する別のパッケージです。 ライブラリ"LibTactics"は"SSReflect"と次の2点で異なります:

• "SSReflect"は主として数学の定理を証明するために開発されました。 一方、"LibTactics"は主としてプログラミング言語の定理の証明のために開発されました。 特に"LibTactics"は、"SSReflect"パッケージには対応するものがない、 いくつもの有用なタクティックを提供します。
• "SSReflect"はタクティックの提示方法を根底から考え直しています。 一方、"LibTactics"はCoqタクティックの伝統的提示方法をほとんど崩していません。 このことからおそらく"LibTactics"の方が"SSReflect"よりとっつきやすいと思われます。

この章は"LibTactics"ライブラリの最も便利な機能に焦点を当てたチュートリアルです。 "LibTactics"のすべての機能を示すことを狙ってはいません。 タクティックの完全なドキュメンテーションはソースファイルLibTactics_J.vにあります。 さらに、タクティックのはたらきを見せるデモは、ファイルLibTacticsDemos_J.vにあります。 (訳注:原文ファイル群にも LibTacticsDemos.v は含まれていません。 このファイル名でネット検索してみてください。)

タクティックの説明にはほとんど、「ソフトウェアの基礎」 ("Software Foundations")のコースの主要な章から抽出した例を使います。 タクティックのいろいろな使い方を説明するために、ゴールを複製するタクティックを使います。 より詳しく言うと、dupは現在のゴールを2つにコピーします。 またdup nはゴールのn個のコピーを作ります。

導入と場合分けについてのタクティック

この節では、以下のタクティックを説明します:

• introv :仮定に名前をつける時間を省くのに使います
• inverts :inversionタクティックの改良です
• cases :情報を失わずに場合分けします
• cases_if :ifの引数について自動的に場合分けします

タクティックintrov

タクティックintrovは、定理の変数を自動的に導入し、生成される仮定に明示的に名前を付けます。 次の例では、決定性の主張に関する変数c、st、st1、st2 には明示的に命名する必要はありません。これらは補題の主張の中で既に名前が付けられているからです。 これに対して、2つの仮定E1とE2には名前をつけると便利です。

仮定に名前をつける必要がない場合には、引数なしでintrovを呼ぶことができます。

タクティックintrovは∀と→が交互に現れる主張にも適用できます。

introsと同様、introvも、構造化パターンを引数にとることができます。

注記: タクティックintrovは、 定義をunfoldしないと仮定が出てこない場合にも使うことができます。

タクティックinverts

Coqのinversionタクティックは3つの点で十分なものだと言えません。 1つ目は、inversionは、substで置換して消してしまいたいような、 たくさんの等式を生成することです。 2つ目は、仮定に意味のない名前を付けることです。 3つ目は、inversion Hは、ほとんどの場合Hを後で使うことはないにもかかわらず、 コンテキストからHを消去しないことです。 タクティックinvertsはこの3つの問題すべてを扱います。 このタクティックは、タクティックinversionにとって代わることを意図したものです。

次の例は、タクティックinverts Hが、 置換を適切に行う以外はinversion Hと同様にはたらくことを示しています。

次にもう少し興味深い例を見てみましょう。

タクティックinverts H as.はinverts Hと同様ですが、次の点が違います。 inverts H as.では、生成される変数と仮定がコンテキストではなくゴールに置かれます。 この戦略により、 これらの変数と仮定にintrosやintrovを使って明示的に名前を付けることができるようになります。

inversionを使ったとするとゴールが1つだけできる場合に、invertsを inverts H as H1 H2 H3の形で呼ぶことができます。このとき新しい仮定は H1、H2、H3と名付けられます。言い換えると、タクティックinverts H as H1 H2 H3 は、invert H; introv H1 H2 H3と同じです。例を示します。

より複雑な例です。特に、invertされた仮定の名前を再利用できることを示しています。

注意: 稀に、仮定HをinvertするときにHをコンテキストから除去したくない場合があります。 その場合には、タクティックinverts keep Hを使うことができます。 キーワードkeepは仮定をコンテキストに残せということを示しています。

タクティックcasesとcases_if

タクティックcases Eは、remember E as x; destruct x の略記法です。 しかしそれだけでなく、rememberが生成する等式の右辺と左辺を逆にしたものを生成します。 例えば、casesは、等式 true = beq_id k1 k2 ではなく等式 beq_id k1 k2 = true を作ります。なぜなら、true = beq_id k1 k2 は読むのにかなり不自然な形だからです。 タクティック cases E as H の形にすると、生成された等式に名前を付けることができます。

注記: cases は case_eq にかなり近いです。 remember および case_eq との互換性のために、ライブラリ"LibTactics"には cases' というタクティックが用意されています。 cases' は remember および case_eq とまったく同じ等式を生成します。 つまり、beq_id k1 k2 = true ではなく true = beq_id k1 k2 という形の等式です。 次の例は、タクティックcases' E as Hの振る舞いを表しています。

タクティックcases_ifはゴールまたはコンテキストのifの引数として現れる式Eに対して cases Eを呼びます。このため、タクティックcases_ifを使うと、 ゴールに既に現れている式をコピーする必要がなくなります。 先と同様、互換性のため、ライブラリには cases_if' というタクティックが用意されています。 また cases_if' as H という形で、生成される等式に名前をつけることができます。

n-引数論理演算のためのタクティック

Coqは and と or を2引数コンストラクタ∧および∨でコード化するため、 N個の事実についての and や or の扱いがとても面倒なものになります。 このため、"LibTactics"では n個の and と or を直接サポートするタクティックを提供します。 さらに、n個の存在限量に対する直接的サポートも提供します。

この節では以下のタクティックを説明します:

• splits :n個の and を分解します
• branch :n個の or を分解します
• ∃ :n個の存在限量の証明をします。

タクティック splits

タクティックsplitsは、n個の命題の and に適用され、n個のサブゴールを作ります。 例えば、ゴールG1 ∧ G2 ∧ G3を3つのサブゴールG1、G2、G3に分解します。

タクティック branch

タクティック branch k は n個の or の証明に使うことができます。 例えば、ゴールが G1 ∨ G2 ∨ G3 という形のとき、 タクティック branch 2 は G2 だけをサブゴールとします。 次の例はbranchタクティックの振る舞いを表しています。

タクティック ∃

ライブラリ "LibTactics" は n個の存在限量についての記法を用意しています。 例えば、∃ x, ∃ y, ∃ z, H と書く代わりに ∃ x y z, H と書くことができます。 同様に、ライブラリはn引数のタクティック∃ a b cを提供します。 これは、∃ a; ∃ b; ∃ cの略記法です。 次の例はn個の存在限量についての記法とタクティックを表しています。

注記: n個の存在限量についての同様の機能が標準ライブラリのモジュール Coq.Program.Syntaxで提供されています。ただ、 このモジュールのものは限量対象が4つまでしか対応していませんが、 LibTacticsは10個までサポートしています。

等式を扱うタクティック

他の対話的証明支援器と比べたCoqの大きな弱点の一つは、 等式に関する推論のサポートが比較的貧弱なことです。 次に説明するタクティックは、等式を扱う証明記述を簡単にすることを狙ったものです。

この節で説明するタクティックは次のものです:

• asserts_rewrite : 書き換えのための等式を導入します
• cuts_rewrite : サブゴールが交換される以外は同じです
• substs : subst タクティックを改良します
• fequals : f_equal タクティックを改良します
• applys_eq : 仮定 P x z を使って、等式 y = z を自動生成し、 P x y を証明します

タクティック asserts_rewrite と cuts_rewrite

タクティック asserts_rewrite (E1 = E2) はゴール内の E1 を E2 で置換し、 ゴール E1 = E2 を生成します。

タクティック cuts_rewrite (E1 = E2) は asserts_rewrite (E1 = E2) と同様ですが、 等式 E1 = E2 が最初のサブゴールになります。

より一般には、タクティック asserts_rewrite と cuts_rewrite は補題を引数としてとることができます。 例えば asserts_rewrite (∀ a b, a*(S b) = a*b+a) と書くことができます。 この記法はaやbが大きな項であるとき便利です。 その大きな項を繰り返さずに済むからです。

タクティック substs

タクティック substs は subst と同様ですが、subst と違い、 ゴールが x = f x のような「循環する等式」を含むときも失敗しません。

タクティック fequals

タクティック fequals は f_equal と同様ですが、 生成される自明なサブゴールを直接解決してしまう点が違います。 さらに、タクティック fequals はタプル間の等式の扱いが強化されています。

タクティック applys_eq

タクティック applys_eq は eapply の変種で、 単一化できない部分項間の等式を導入します。 例えば、ゴールが命題 P x y で、P x z が成立するという仮定Hがあるとします。 またyとzが等しいことが証明できることはわかっているとします。 すると、タクティック assert_rewrite (y = z) を呼び、ゴールを P x z に変えることができます。 しかしこれには、yとzの値のコピー&ペーストが必要になります。 タクティックapplys_eqを使うと、この場合 applys_eq H 1 とできます。 すると、ゴールは証明され、サブゴール y = z が残ります。 applys_eqの引数の値1は、 P x y の右から1番目の引数についての等式を導入したいことを表します。 以下の3つの例は、それぞれ applys_eq H 1、applys_eq H 2、applys_eq H 1 2 を呼んだときの振る舞いを示します。

もしミスマッチがPの第2引数ではなく第1引数だった場合には、 applys_eq H 2と書きます。 出現は右からカウントされることを思い出してください。

2つの引数にミスマッチがある場合、2つの等式が欲しくなります。 そのためには、applys_eq H 1 2 とできます。 より一般に、タクティックapplys_eqは1つの補題と自然数の列を引数としてとります。

便利な略記法をいくつか

チュートリアルのこの節では、証明記述をより短かく、 より読みやすくするのに役立つタクティックをいくつか紹介します:

• unfolds (引数なし): 先頭の定義を unfold します
• false : ゴールを False で置換します
• gen : dependent generalize の略記法です
• skip : サブゴールをスキップします(存在変数と組み合わせて使います)
• sort : 証明コンテキストの下の命題を動かします

タクティック unfolds

タクティック unfolds (引数なし) はゴールの先頭の定数を unfold します。 このタクティックは定数を明示的に指名する手間を省きます。

注記: タクティックhnfはすべての先頭の定数をunfoldしますが、 これと対照的にunfoldsは1つだけunfoldします。

注記: タクティック unfolds in H は仮定Hの先頭の定義をunfoldします。

タクティックfalseとtryfalse

タクティックfalseは任意のゴールをFalseに置換します。 簡単に言うと、apply ex_falso_quodlibetの略記法です。 さらにfalseは、不条理な仮定(Falseや0 = S nなど) や矛盾した仮定(x = trueとx = falseなど)を含むゴールを証明します。

タクティックtryfalseは try solve [false] の略記法です。 このタクティックはゴールの矛盾を探します。 タクティックtryfalseは一般に場合分けの後で呼ばれます。

タクティック gen

タクティックgenは generalize dependent の略記法です。 たくさんの引数を一度に受けます。このタクティックは gen x y z という形で呼びます。

タクティックskip、skip_rewrite、skip_goal

サブゴールをadmitできることは証明を構成するうえでとても便利です。 証明の一番興味深いケースに最初にフォーカスできるようになるからです。 タクティックskipはadmitと似ていますが、 証明が存在変数を含む場合にも機能します。 存在変数とは、?24のように名前がクエスチョンマークから始まる変数で、 典型的にはeapplyによって導入されるものであったことを思い出してください。

タクティック skip H: P は仮定 H: P をコンテキストに追加します。 このときに命題Pが真かどうかのチェックはしません。 このタクティックは、事実を、証明を後回しにして利用するのに便利です。 注意: skip H: P は単に assert (H:P). skip. の略記法です。

タクティック skip_rewrite (E1 = E2) はゴールのE1をE2で置換します。 このときにE1が実際にE2と等しいかはチェックしません。

注記: タクティックskip_rewriteは実際はasserts_rewrite と同じように補題を引数としてとることができます。

タクティックskip_goalは現在のゴールを仮定として追加します。 このごまかしは帰納法による証明の構造の構成の際に、 帰納法の仮定がより小さい引数だけに適用されるかを心配しないで済むため有用です。 skip_goalを使うことで、証明を次の2ステップで構成できます： 最初に、帰納法の仮定の細部の調整に時間を浪費せずに、主要な議論が通るかをチェックし、 その後、帰納法の仮定の呼び出しの調整にフォーカスするというステップです。

タクティック sort

タクティックsortは証明コンテキストを再構成し、変数が上に仮定が下になるようにします。 これにより、証明コンテキストはより読みやすくなります。

高度な補題具体化のためのタクティック

この最後の節では、補題に引数のいくつかを与え、他の引数は明示化しないままで、 補題を具体化するメカニズムについて記述します。 具体値を与えられない変数は存在変数となり、具体化が与えられない事実はサブゴールになります。

注記: この具体化メカニズムは「暗黙の引数」メカニズムをはるかに超越する能力を提供します。 この節で記述する具体化メカニズムのポイントは、どれだけの '_' 記号を書かなければならないかの計算に時間を使わなくてよくなることです。

この節では、Coq の便利な連言(and)と存在限量の分解機構を使います。 簡単に言うと、introsやdestructは [H1 [H2 [H3 [H4 H5]]]] の略記法としてパターン (H1 & H2 & H3 & H4 & H5) をとることができます。 例えば destruct (typing_inversion_var _ _ _ Htypt) as [T [Hctx Hsub]]. は destruct (typing_inversion_var _ _ _ Htypt) as (T & Hctx & Hsub). と書くことができます。

letsのはたらき

利用したい補題(または仮定)がある場合、大抵、この補題に明示的に引数を与える必要があります。 例えば次のような形です: destruct (typing_inversion_var _ _ _ Htypt) as (T & Hctx & Hsub). 何回も'_'記号を書かなければならないのは面倒です。 何回書くかを計算しなければならないだけでなく、このことで証明記述がかなり汚なくもなります。 タクティックletsを使うことで、次のように簡単に書くことができます: lets (T & Hctx & Hsub): typing_inversion_var Htypt.

簡単に言うと、このタクティックletsは補題のたくさんの変数や仮定を特定します。 記法は lets I: E0 E1 .. EN という形です。 そうすると事実E0に引数E1からENを与えてIという名前の仮定を作ります。 すべての引数を与えなければならないわけではありませんが、 与えなければならない引数は、正しい順番で与えなければなりません。 このタクティックは、与えられた引数を使って補題をどうしたら具体化できるかを計算するために、 型の上の first-match アルゴリズムを使います。

最初に、型が has_type G (tm_var x) T である仮定Hを持つとします。 タクティック lets K: typing_inversion_var H を呼ぶことで補題typing_inversion_varを結論として得ることができます。 以下の通りです。

今、G、x、Tの値を知っていて、Sを得たいとします。 また、サブゴールとして has_type G (tm_var x) T が生成されていたとします。 typing_inversion_var の残った引数のすべてをサブゴールとして生成したいことを示すために、 '_'を三連した記号___を使います。 (後に、___を書くのを避けるためにforwardsという略記用タクティックを導入します。)

通常、has_type G (tm_var x) T を証明するのに適したコンテキスト Gと型Tは1つだけしかないので、 実はGとTを明示的に与えることに煩わされる必要はありません。 lets (S & Eq & Sub): typing_inversion_var x とすれば十分です。 このとき、変数GとTは存在変数を使って具体化されます。

より極端に、typing_inversion_varの具体化のために引数をまったく与えないこともできます。 この場合、3つの単一化変数が導入されます。

注意: letsに補題の名前だけを引数として与えた場合、 その補題が証明コンテキストに追加されるだけで、 その引数を具体化しようとすることは行いません。

letsの最後の便利な機能は '_' を2つ続けた記号__です。 これを使うと、いくつかの引数が同じ型を持つとき引数を1つスキップできます。 以下の例は、mを値3に具体化したい一方、nは存在変数を使って具体化したい場面です。

注意: 証明記述の中でHの名前を言う必要がないとき、lets H: E0 E1 E2 の代わりに lets: E0 E1 E2 と書くことができます。

注意: タクティックletsは5つまでの引数をとることができます。 5個を越える引数を与えることができる場合に、別の構文があります。 キーワード>>から始まるリストを使ったものです。 例えば lets H: (>> E0 E1 E2 E3 E4 E5 E6 E7 E8 E9 10) と書きます。

applys、forwards、specializesのはたらき

タクティックapplys、forwards、specializesは letsを特定の用途に使う場面での略記法です。

• forwardsは補題のすべての引数を具体化する略記法です。 より詳しくは、forwards H: E0 E1 E2 E3 は lets H: E0 E1 E2 E3 ___ と同じです。ここで ___ の意味は前に説明した通りです。
  
  
• applysは、letsの高度な具体化モードにより補題を構築し、 それをすぐに使うことにあたります。 これから、applys E0 E1 E2 E3 は、 lets H: E0 E1 E2 E3 の後 eapply H、clear H と続けることと同じです。
  
  
• specializesは、コンテキストの仮定を特定の引数でその場で具体化することの略記法です。 より詳しくは、specializes H E0 E1 は lets H': H E0 E1 の後 clear H、rename H' into H と続けることと同じです。

applysの使用例は以下で出てきます。 specializesとforwardsの使用例は、 チュートリアルファイルUseAuto_J.vにいくつか含まれています。

具体化の例

以下の証明では、いくつかの場所でletsがdestructの代わりに、 applysがapplyの代わりに使われます。 その場所は "old:"で始まるコメントで示されています。 letsを使う練習問題も示されています。

    (* old: destruct (typing_inversion_var _ _ _ Htypt) as [T [Hctx Hsub]].*) 

       (* old: destruct (free_in_context _ _ S empty Hcontra) as [T' HT']... *) 

    (* 練習問題: 次の[destruct]を[lets]に換えなさい *)

    (* old: destruct (typing_inversion_app _ _ _ _ Htypt) as [T1 [Htypt1 Htypt2]].
            eapply T_App... *)

    (* old: destruct (typing_inversion_abs _ _ _ _ _ Htypt). *)

    (* old: apply T_Sub with (ty_arrow T1 T2)... *)

    (* old: assert (subtype ty_Unit S) by apply (typing_inversion_unit _ _ Htypt)... *)