UseTactics_J:Coq用タクティックライブラリのご紹介¶

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

Require Import LibTactics_J.

注記: 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`¶

Module IntrovExamples.
  Require Import Stlc_J.
  Import Imp_J STLC.

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

Theorem ceval_deterministic: forall c st st1 st2,
  c / st || st1 ->
  c / st || st2 ->
  st1 = st2.
Proof.
  introv E1 E2.
Admitted.

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

Theorem ceval_and_ceval_step_coincide: forall c st st',
      c / st || st'
  <-> exists i, ceval_step st c i = Some st'.
Proof.
  introv.
Admitted.

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

Theorem ceval_deterministic': forall c st st1,
  (c / st || st1) -> forall st2, (c / st || st2) -> st1 = st2.
Proof.
  introv E1 E2.
Admitted.

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

Theorem ceval_step__ceval: forall c st st',
      (exists i, ceval_step st c i = Some st') ->
      c / st || st'.
Proof.
  introv [i E].

Admitted.

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

End IntrovExamples.

タクティック`inverts`¶

Module InvertsExamples.
  Require Import Stlc_J Equiv_J Imp_J.
  Import STLC.

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

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

Theorem skip_left: forall c,
  cequiv (SKIP; c) c.
Proof.
  introv. split; intros H.
  dup.

  inversion H. subst. inversion H2. subst. assumption.

  inverts H. inverts H2. assumption.
Admitted.

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

Theorem ceval_deterministic: forall c st st1 st2,
  c / st || st1  ->
  c / st || st2 ->
  st1 = st2.
Proof.
  introv E1 E2. generalize dependent st2.
  (ceval_cases (induction E1) Case); intros st2 E2.
  admit. admit.
  dup.
   inversion E2. subst. admit.
   inverts E2. admit.
Admitted.

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

Theorem ceval_deterministic': forall c st st1 st2,
     c / st || st1  ->
     c / st || st2 ->
     st1 = st2.
Proof.
  introv E1 E2. generalize dependent st2.
  (ceval_cases (induction E1) Case); intros st2 E2;
    inverts E2 as.
  Case "E_Skip". reflexivity.
  Case "E_Ass".

     subst n.
    reflexivity.
  Case "E_Seq".

     intros st3 Red1 Red2.
    assert (st' = st3) as EQ1.
      SCase "Proof of assertion". apply IHE1_1; assumption.
    subst st3.
    apply IHE1_2. assumption.
  Case "E_IfTrue".
    SCase "b1 evaluates to true".

       intros.
      apply IHE1. assumption.
    SCase "b1 evaluates to false (contradiction)".
       intros.
      rewrite H in H5. inversion H5.

Admitted.

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

Theorem skip_left': forall c,
  cequiv (SKIP; c) c.
Proof.
  introv. split; intros H.
  inverts H as U V.
  inverts U. assumption.
Admitted.

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

Example typing_nonexample_1 :
  ~ exists T,
      has_type empty
        (tm_abs a ty_Bool
            (tm_abs b ty_Bool
               (tm_app (tm_var a) (tm_var b))))
        T.
Proof.
  dup 3.


  intros C. destruct C.
  inversion H. subst. clear H.
  inversion H5. subst. clear H5.
  inversion H4. subst. clear H4.
  inversion H2. subst. clear H2.
  inversion H5. subst. clear H5.
  inversion H1.


  intros C. destruct C.
  inverts H as H1.
  inverts H1 as H2.
  inverts H2 as H3.
  inverts H3 as H4.
  inverts H4.


  intros C. destruct C.
  inverts H as H.
  inverts H as H.
  inverts H as H.
  inverts H as H.
  inverts H.
Qed.

End InvertsExamples.

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

タクティック`cases`と`cases_if`¶

Module CasesExample.
  Require Import Stlc_J.
  Import STLC.

タクティック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の振る舞いを表しています。

Theorem update_same : forall x1 k1 k2 (f : state),
  f k1 = x1 ->
  (update f k1 x1) k2 = f k2.
Proof.
  intros x1 k1 k2 f Heq.
  unfold update. subst.
  dup.


  remember (beq_id k1 k2) as b. destruct b.
    apply beq_id_eq in Heqb. subst. reflexivity.
    reflexivity.


  cases' (beq_id k1 k2) as E.
    apply beq_id_eq in E. subst. reflexivity.
    reflexivity.
Qed.

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

Theorem update_same' : forall x1 k1 k2 (f : state),
  f k1 = x1 ->
  (update f k1 x1) k2 = f k2.
Proof.
  intros x1 k1 k2 f Heq.
  unfold update. subst.


  cases_if' as E.
    apply beq_id_eq in E. subst. reflexivity.
    reflexivity.
Qed.

End CasesExample.

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

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

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

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

Module NaryExamples. Require Import References_J SfLib_J. Import STLCRef.

タクティック`splits`¶

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

Lemma demo_splits : forall n m,
  n > 0 /\ n < m /\ m < n+10 /\ m <> 3.
Proof.
  intros. splits.
Admitted.

タクティック`branch`¶

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

Lemma demo_branch : forall n m,
  n < m \/ n = m \/ m < n.
Proof.
  intros.
  destruct (lt_eq_lt_dec n m) as [[H1|H2]|H3].
  branch 1. apply H1.
  branch 2. apply H2.
  branch 3. apply H3.
Qed.

タクティック`exists`¶

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

Theorem progress : forall ST t T st,
  has_type empty ST t T ->
  store_well_typed ST st ->
  value t \/ exists t' st', t / st ==> t' / st'.

Proof with eauto.
  intros ST t T st Ht HST. remember (@empty ty) as Gamma.
  (has_type_cases (induction Ht) Case); subst; try solve by inversion...
  Case "T_App".
    right. destruct IHHt1 as [Ht1p | Ht1p]...
    SCase "t1 is a value".
      inversion Ht1p; subst; try solve by inversion.
      destruct IHHt2 as [Ht2p | Ht2p]...
      SSCase "t2 steps".
        inversion Ht2p as [t2' [st' Hstep]].
        exists (tm_app (tm_abs x T t) t2') st'...

Admitted.

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

End NaryExamples.

等式を扱うタクティック¶

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

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

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

Module EqualityExamples.

タクティック`asserts_rewrite`と`cuts_rewrite`¶

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

Theorem mult_0_plus : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  dup.

  intros n m.
  assert (H: 0 + n = n). reflexivity. rewrite -> H.
  reflexivity.


  intros n m.
  asserts_rewrite (0 + n = n).
    reflexivity.
    reflexivity.
Qed.

注記:`asserts_rewrite (E1 = E2) in H`と書いた場合、¶

ゴールの代わりに仮定Hを書き換えます。

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

Theorem mult_0_plus' : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  intros n m.
  cuts_rewrite (0 + n = n).
    reflexivity.
    reflexivity.
Qed.

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

Theorem mult_0_plus'' : forall u v w x y z: nat,
  (u + v) * (S (w * x + y)) = z.
Proof.
  intros. asserts_rewrite (forall a b, a*(S b) = a*b+a).


Admitted.

タクティック`substs`¶

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

Lemma demo_substs : forall x y (f:nat->nat),
  x = f x -> y = x -> y = f x.
Proof.
  intros. substs.
  assumption.
Qed.

タクティック`fequals`¶

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

Lemma demo_fequals : forall (a b c d e : nat) (f : nat->nat->nat->nat->nat),
  a = 1 -> b = e -> e = 2 ->
  f a b c d = f 1 2 c 4.
Proof.
  intros. fequals.

Admitted.

タクティック`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を呼んだときの振る舞いを示します。

Axiom big_expression_using : nat->nat.

Lemma demo_applys_eq_1 : forall (P:nat->nat->Prop) x y z,
  P x (big_expression_using z) ->
  P x (big_expression_using y).
Proof.
  introv H. dup.


  assert (Eq: big_expression_using y = big_expression_using z).
    admit.
  rewrite Eq. apply H.


  applys_eq H 1.
    admit.
Qed.

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

Lemma demo_applys_eq_2 : forall (P:nat->nat->Prop) x y z,
  P (big_expression_using z) x ->
  P (big_expression_using y) x.
Proof.
  introv H. applys_eq H 2.
Admitted.

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

Lemma demo_applys_eq_3 : forall (P:nat->nat->Prop) x1 x2 y1 y2,
  P (big_expression_using x2) (big_expression_using y2) ->
  P (big_expression_using x1) (big_expression_using y1).
Proof.
  introv H. applys_eq H 1 2.

Admitted.

End EqualityExamples.

便利な略記法をいくつか¶

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

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

タクティック`unfolds`¶

Module UnfoldsExample.
  Require Import Hoare_J.

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

Lemma bexp_eval_true : forall b st,
  beval st b = true -> (bassn b) st.
Proof.
  intros b st Hbe. dup.


  unfold bassn. assumption.


  unfolds. assumption.
Qed.

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

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

End UnfoldsExample.

タクティック`false`と`tryfalse`¶

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

Lemma demo_false :
  forall n, S n = 1 -> n = 0.
Proof.
  intros. destruct n. reflexivity. false.
Qed.

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

Lemma demo_tryfalse :
  forall n, S n = 1 -> n = 0.
Proof.
  intros. destruct n; tryfalse. reflexivity.
Qed.

タクティック`gen`¶

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

Module GenExample.
  Require Import Stlc_J.
  Import STLC.

Lemma substitution_preserves_typing : forall Gamma x U v t S,
     has_type (extend Gamma x U) t S ->
     has_type empty v U ->
     has_type Gamma (subst v x t) S.
Proof.
  dup.


  intros Gamma x U v t S Htypt Htypv.
  generalize dependent S. generalize dependent Gamma.
  induction t; intros; simpl.
  admit. admit. admit. admit. admit. admit.


  introv Htypt Htypv. gen S Gamma.
  induction t; intros; simpl.
  admit. admit. admit. admit. admit. admit.
Qed.

End GenExample.

タクティック`skip`、`skip_rewrite`、`skip_goal`¶

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

Module SkipExample.
  Require Import Stlc_J.
  Import STLC.

Example astep_example1 :
  (APlus (ANum 3) (AMult (ANum 3) (ANum 4))) / empty_state ==>a* (ANum 15).
Proof.
  eapply rsc_step. skip.
  eapply rsc_step. skip. skip.

Admitted.

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

Theorem demo_skipH : True.
Proof.
  skip H: (forall n m : nat, (0 + n) * m = n * m).
Admitted.

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

Theorem mult_0_plus : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  dup.


  intros n m.
  assert (H: 0 + n = n). skip. rewrite -> H.
  reflexivity.


  intros n m.
  skip_rewrite (0 + n = n).
  reflexivity.
Qed.

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

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

Theorem ceval_deterministic: forall c st st1 st2,
  c / st || st1 ->
  c / st || st2 ->
  st1 = st2.
Proof.

  skip_goal.

  introv E1 E2. gen st2.
  (ceval_cases (induction E1) Case); introv E2; inverts E2 as.
  Case "E_Skip". reflexivity.
  Case "E_Ass".
    subst n.
    reflexivity.
  Case "E_Seq".
    intros st3 Red1 Red2.
    assert (st' = st3) as EQ1.
      SCase "Proof of assertion".

         eapply IH. eapply E1_1. eapply Red1.
    subst st3.

     eapply IH. eapply E1_2. eapply Red2.

Admitted.

End SkipExample.

タクティック`sort`¶

Module SortExamples.
  Require Import Imp_J.

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

Theorem ceval_deterministic: forall c st st1 st2,
  c / st || st1 ->
  c / st || st2 ->
  st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2.
  (ceval_cases (induction E1) Case); intros st2 E2; inverts E2.
  admit. admit.
  sort.
Admitted.

End SortExamples.

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

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

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

この節では、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 アルゴリズムを使います。

Module ExamplesLets.
  Require Import Subtyping_J.



Axiom typing_inversion_var : forall (G:context) (x:id) (T:ty),
  has_type G (tm_var x) T ->
  exists S, G x = Some S /\ subtype S T.

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

Lemma demo_lets_1 : forall (G:context) (x:id) (T:ty),
  has_type G (tm_var x) T -> True.
Proof.
  intros G x T H. dup.


  lets K: typing_inversion_var H.
  destruct K as (S & Eq & Sub).
  admit.


  lets (S & Eq & Sub): typing_inversion_var H.
  admit.

Qed.

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

Lemma demo_lets_2 : forall (G:context) (x:id) (T:ty), True.
Proof.
  intros G x T.
  lets (S & Eq & Sub): typing_inversion_var G x T ___.
Admitted.

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

Lemma demo_lets_3 : forall (x:id), True.
Proof.
  intros x.
  lets (S & Eq & Sub): typing_inversion_var x ___.
Admitted.

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

Lemma demo_lets_4 : True.
Proof.
  lets (S & Eq & Sub): typing_inversion_var ___.
Admitted.

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

Lemma demo_lets_5 : True.
Proof.
  lets H: typing_inversion_var.
Admitted.

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

Lemma demo_lets_underscore :
  (forall n m, n <= m -> n < m+1) -> True.
Proof.
  intros H.


  lets K: H 3.
    clear K.


  lets K: H __ 3.
    clear K.
Admitted.

注意: 証明記述の中で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)と書きます。

End ExamplesLets.

`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にいくつか含まれています。

具体化の例¶

Module ExamplesInstantiations.
  Require Import Subtyping_J.

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

Lemma substitution_preserves_typing : forall Gamma x U v t S,
     has_type (extend Gamma x U) t S ->
     has_type empty v U ->
     has_type Gamma (subst v x t) S.
Proof with eauto.
  intros Gamma x U v t S Htypt Htypv.
  generalize dependent S. generalize dependent Gamma.
  (tm_cases (induction t) Case); intros; simpl.
  Case "tm_var".
    rename i into y.


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

lets (T&Hctx&Hsub): typing_inversion_var Htypt.
    unfold extend in Hctx.
    remember (beq_id x y) as e. destruct e...
    SCase "x=y".
      apply beq_id_eq in Heqe. subst.
      inversion Hctx; subst. clear Hctx.
      apply context_invariance with empty...
      intros x Hcontra.


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

lets [T' HT']: free_in_context S empty Hcontra...
        inversion HT'.
  Case "tm_app".


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


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

(* FILL IN HERE *) admit.

  Case "tm_abs".
    rename i into y. rename t into T1.


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

lets (T2&Hsub&Htypt2): typing_inversion_abs Htypt.


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

applys T_Sub (ty_arrow T1 T2)...
     apply T_Abs...
    remember (beq_id x y) as e. destruct e.
    SCase "x=y".
      eapply context_invariance...
      apply beq_id_eq in Heqe. subst.
      intros x Hafi. unfold extend.
      destruct (beq_id y x)...
    SCase "x<>y".
      apply IHt. eapply context_invariance...
      intros z Hafi. unfold extend.
      remember (beq_id y z) as e0. destruct e0...
      apply beq_id_eq in Heqe0. subst.
      rewrite <- Heqe...
  Case "tm_true".
    lets: typing_inversion_true Htypt...
  Case "tm_false".
    lets: typing_inversion_false Htypt...
  Case "tm_if".
    lets (Htyp1&Htyp2&Htyp3): typing_inversion_if Htypt...
  Case "tm_unit".


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

lets: typing_inversion_unit Htypt...


Qed.

End ExamplesInstantiations.

UseTactics_J:Coq用タクティックライブラリのご紹介¶

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

タクティックintrov¶

タクティックinverts¶

タクティックcasesとcases_if¶

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

タクティックsplits¶

タクティックbranch¶

タクティックexists¶

等式を扱うタクティック¶

タクティックasserts_rewriteとcuts_rewrite¶

注記:asserts_rewrite (E1 = E2) in Hと書いた場合、¶

タクティックsubsts¶

タクティックfequals¶

タクティックapplys_eq¶