UseTactics: Coq用タクティックライブラリの簡単な紹介
Coqはビルトインのタクティックの集合を持っています。
reflexivity、intros、inversionなどです。
これらのタクティックだけで証明を構成することは可能ですが、より強力なタクティックの集合を使うことで、生産性を飛躍的に上げることができます。
この章では、とても便利なのに、いろいろな理由でデフォルトのCoqでは用意されていないたくさんのタクティックを説明します。
それらのタクティックは、LibTactics.vファイルに定義されています。
Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Arith.Arith.
From PLF Require Import Maps.
From PLF Require Import Imp.
From PLF Require Import Types.
From PLF Require Import Smallstep.
From PLF Require Import LibTactics.
From PLF Require Stlc.
From PLF Require Equiv.
From PLF Require Imp.
From PLF Require References.
From PLF Require Smallstep.
From PLF Require Hoare.
From PLF Require Sub.
注記: SSReflect は強力なタクティックを提供する別のパッケージです。
ライブラリ"LibTactics"は"SSReflect"と次の2点で異なります:
- "SSReflect"は主として数学の定理を証明するために開発されました。 一方、"LibTactics"は主としてプログラミング言語の定理の証明のために開発されました。 特に"LibTactics"は、"SSReflect"パッケージには対応するものがない、 いくつもの有用なタクティックを提供します。
- "SSReflect"はタクティックの提示方法を根底から考え直しています。 一方、"LibTactics"はCoqタクティックの伝統的提示方法をほとんど崩していません。 このことからおそらく"LibTactics"の方が"SSReflect"よりとっつきやすいと思われます。
この章は"LibTactics"ライブラリの最も便利な機能に焦点を当てたチュートリアルです。
"LibTactics"のすべての機能を示すことを狙ってはいません。
タクティックの詳細な仕様はソースファイルLibTactics.vにあります。
さらに、タクティックのはたらきを見せるデモは、
http://www.chargueraud.org/softs/tlc/ にあります。
このチュートリアルにおいて、タクティックの説明に用いる例は「ソフトウェアの基礎」
("Software Foundations")のコースの主要な章から抽出しています。
タクティックのいろいろな使い方を説明するために、ゴールを複製するタクティックを使います。
より詳しく言うと、dupは現在のゴールを2つにコピーします。
またdup nはゴールのn個のコピーを作ります。
この節では、以下のタクティックを説明します:
- introv :効率的に仮定に名前をつけます
- inverts :inversionタクティックの改良です
タクティックintrovは、定理の変数を自動的に導入し、生成される仮定に明示的に名前を付けます。
次の例では、決定性の主張に関する変数c、st、st1、st2には明示的に命名する必要はありません。
これらは補題の主張の中で既に名前が付けられているからです。
これに対して、2つの仮定には名前を付けると便利で、ここではそれぞれE1とE2と付けてみます。
Theorem ceval_deterministic: forall c st st1 st2,
st =[ c ]=> st1 ->
st =[ c ]=> st2 ->
st1 = st2.
Proof.
introv E1 E2. Abort.
仮定に名前をつける必要がない場合には、引数なしでintrovを呼ぶことができます。
Theorem dist_exists_or : forall (X:Type) (P Q : X -> Prop),
(exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Proof.
introv. Abort.
タクティックintrovはforallと->が交互に現れる主張にも適用できます。
Theorem ceval_deterministic': forall c st st1,
(st =[ c ]=> st1) ->
forall st2,
(st =[ c ]=> st2) ->
st1 = st2.
Proof.
introv E1 E2. Abort.
introsと同様、introvも、構造化パターンを引数にとることができます。
Theorem exists_impl: forall X (P : X -> Prop) (Q : Prop) (R : Prop),
(forall x, P x -> Q) ->
((exists x, P x) -> Q).
Proof.
introv [x H2]. eauto.
Qed.
注記: タクティックintrovは、
定義をunfoldしないと仮定が出てこない場合にも使うことができます。
Coqのinversionタクティックは3つの点で十分なものだと言えません。
1つ目は、inversionは、substで置換して消してしまいたいような、たくさんの等式を生成することです。
2つ目は、仮定に意味のない名前を付けることです。
3つ目は、inversion Hは、ほとんどの場合Hを後で使うことはないにもかかわらず、コンテキストからHを消去しないことです。
タクティックinvertsはこの3つの問題すべてを扱います。
このタクティックは、タクティックinversionにとって代わることを意図したものです。
次の例は、タクティックinverts Hが、
inversionが生成する明らかな等式を消去するために置換を行う以外は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.
Abort.
次にもう少し興味深い例を見てみましょう。
Theorem ceval_deterministic: forall c st st1 st2,
st =[ c ]=> st1 ->
st =[ c ]=> st2 ->
st1 = st2.
Proof.
introv E1 E2. generalize dependent st2.
induction E1; intros st2 E2.
admit. admit. dup. - inversion E2. subst. admit.
- inverts E2. admit.
Abort.
タクティックinverts H as.はinverts Hと同様ですが、次の点が違います。
inverts H as.では、生成される変数と仮定がコンテキストではなくゴールに置かれます。
この戦略により、
これらの変数と仮定にintrosやintrovを使って明示的に名前を付けることができるようになります。
Theorem ceval_deterministic': forall c st st1 st2,
st =[ c ]=> st1 ->
st =[ c ]=> st2 ->
st1 = st2.
Proof.
introv E1 E2. generalize dependent st2.
(induction E1); intros st2 E2;
inverts E2 as.
- reflexivity.
-
subst n.
reflexivity.
-
intros st3 Red1 Red2.
assert (st' = st3) as EQ1.
{ apply IHE1_1; assumption. }
subst st3.
apply IHE1_2. assumption.
-
intros.
apply IHE1. assumption.
-
intros.
rewrite H in H5. inversion H5.
Abort.
inversionを使ったとするとゴールが1つだけできる場合に、invertsを
inverts H as H1 H2 H3の形で呼ぶことができます。このとき新しい仮定は
H1、H2、H3と名付けられます。言い換えると、タクティックinverts H as H1 H2 H3
は、invert H as; 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.
Abort.
次はより複雑な例です。特に、invertされた仮定の名前を再利用できることを示しています。
Example typing_nonexample_1 :
~ exists T,
has_type empty
(abs x Bool
(abs y Bool
(app (var x) (var y))))
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 H1.
- intros C. destruct C.
inverts H as H1.
inverts H1 as H2.
inverts H2 as H3 H4.
inverts H3 as H5.
inverts H5.
- intros C. destruct C.
inverts H as H.
inverts H as H.
inverts H as H1 H2.
inverts H1 as H1.
inverts H1.
Qed.
End InvertsExamples.
注意: 稀に、仮定HをinvertするときにHをコンテキストから除去したくない場合があります。
その場合には、タクティックinverts keep Hを使うことができます。
キーワードkeepは仮定をコンテキストに残せということを示しています。
Coqは and と or を2引数コンストラクタ/\および\/でコード化するため、
N個の事実についての and や or の扱いがとても面倒なものになります。
このため、"LibTactics"では n個の and と or を直接サポートするタクティックを提供します。
さらに、n個の存在限量に対する直接的サポートも提供します。
この節では以下のタクティックを説明します:
- splits :n個の and を分解します
- branch :n個の or を分解します
タクティック 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.
End NaryExamples.
他の対話的証明支援器と比べたCoqの大きな弱点の一つは、
等式に関する推論のサポートが比較的貧弱なことです。
次に説明するタクティックは、等式を扱う証明記述を簡単にすることを狙ったものです。
この節で説明するタクティックは次のものです:
タクティック 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.
タクティック 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).
Abort.
Lemma demo_substs : forall x y (f:nat->nat),
x = f x ->
y = x ->
y = f x.
Proof.
intros. substs. assumption.
Qed.
タクティック 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.
Abort.
タクティック 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. Abort.
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.
Abort.
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.
Abort.
End EqualityExamples.
チュートリアルのこの節では、証明記述をより短かく、
より読みやすくするのに役立つタクティックをいくつか紹介します:
タクティック 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します。
タクティックfalseとtryfalse
タクティックfalseは任意のゴールをFalseに置換します。
簡単に言うと、exfalsoの略記法です（訳注：以前は比較対象がもっと長いタクティックでした）。
さらにfalseは、不条理な仮定(Falseや0 = S nなど)
や矛盾した仮定(x = trueとx = falseなど)を含むゴールを証明します。
Lemma demo_false_arg :
(forall n, n < 0 -> False) ->
3 < 0 ->
4 < 0.
Proof.
intros H L. false H. apply L.
Qed.
Lemma demo_tryfalse : forall n,
S n = 1 ->
n = 0.
Proof.
intros. destruct n; tryfalse. reflexivity.
Qed.
Module GenExample.
Import Stlc.
Import STLC.
Lemma substitution_preserves_typing : forall Gamma x U v t S,
has_type (update Gamma x U) t S ->
has_type empty v U ->
has_type Gamma ([x:=v]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.
Abort.
End GenExample.
一時的にサブゴールを承認(admit)できることは証明を構成するうえでとても便利です。
以降いくつかのタクティックは組み込みのadmitタクティックの便利なラッパーとして作られています。
タクティック admits H: P は仮定 H: P をコンテキストに追加します。
このときに命題Pが真かどうかのチェックはしません。
このタクティックは、事実を、証明を後回しにして利用するのに便利です。
注意: admits H: P は単に assert (H:P). admit. の略記法です。
タクティック admit_rewrite (E1 = E2) はゴールのE1をE2で置換します。
このときにE1が実際にE2と等しいかはチェックしません。
Theorem mult_plus_0 : forall n m : nat,
(n + 0) * m = n * m.
Proof.
dup 3.
intros n m.
assert (H: n + 0 = n). admit. rewrite -> H. clear H.
reflexivity.
intros n m.
admit_rewrite (n + 0 = n).
reflexivity.
intros n m.
admit_rewrite (forall a, a + 0 = a).
reflexivity.
Admitted.
タクティックadmit_goalは現在のゴールを仮定として追加します。
このごまかしは帰納法による証明の構造の構成の際に、
帰納法の仮定がより小さい引数だけに適用されるかを心配しないで済むため有用です。
admit_goalを使うことで、証明を次の2ステップで構成できます：
最初に、帰納法の仮定の細部の調整に時間を浪費せずに、主要な議論が通るかをチェックし、
その後、帰納法の仮定の呼び出しの調整にフォーカスするというステップです。
Theorem ceval_deterministic: forall c st st1 st2,
st =[ c ]=> st1 ->
st =[ c ]=> st2 ->
st1 = st2.
Proof.
admit_goal.
introv E1 E2. gen st2.
(induction E1); introv E2; inverts E2 as.
- reflexivity.
-
subst n.
reflexivity.
-
intros st3 Red1 Red2.
assert (st' = st3) as EQ1.
{
eapply IH. eapply E1_1. eapply Red1. }
subst st3.
eapply IH. eapply E1_2. eapply Red2.
Abort.
End SkipExample.
タクティックsortは証明コンテキストを再構成し、変数が上に仮定が下になるようにします。
これにより、証明コンテキストはより読みやすくなります。
Theorem ceval_deterministic: forall c st st1 st2,
st =[ c ]=> st1 ->
st =[ c ]=> st2 ->
st1 = st2.
Proof.
intros c st st1 st2 E1 E2.
generalize dependent st2.
(induction E1); intros st2 E2; inverts E2.
admit. admit. sort. Abort.
End SortExamples.
この最後の節では、補題に引数のいくつかを与え、他の引数は明示化しないままで、
補題を具体化するメカニズムについて記述します。
具体値を与えられない変数は存在変数となり、具体化が与えられない事実はサブゴールになります。
注記: この具体化メカニズムは「暗黙の引数」メカニズムをはるかに超越する能力を提供します。
この節で記述する具体化メカニズムのポイントは、どれだけの '_'
記号を書かなければならないかの計算に時間を使わなくてよくなることです。
この節では、Coq の便利な連言(and)と存在限量の分解機構を使います。
簡単に言うと、introsやdestructは [H1 [H2 [H3 [H4 H5]]]]
の略記法としてパターン (H1 & H2 & H3 & H4 & H5) をとることができます。
例えば destruct (H _ _ _ Htypt) as [T [Hctx Hsub]].
は destruct (H _ _ _ Htypt) as (T & Hctx & Hsub).
と書くことができます。
利用したい補題(または仮定)がある場合、大抵、この補題に明示的に引数を与える必要があります。
例えば次のような形です:
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.
Import Sub.
Import Sub.
Axiom typing_inversion_var : forall (G:context) (x:string) (T:ty),
has_type G (var x) T ->
exists S, G x = Some S /\ subtype S T.
最初に、型が has_type G (var x) T である仮定Hを持つとします。
タクティック lets K: typing_inversion_var H
を呼ぶことで補題typing_inversion_varを結論として得ることができます。
以下の通りです。
Lemma demo_lets_1 : forall (G:context) (x:string) (T:ty),
has_type G (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.
Abort.
今、G、x、Tの値を知っていて、Sを得たいとします。
また、サブゴールとして has_type G (var x) T が生成されていたとします。
typing_inversion_var
の残った引数のすべてをサブゴールとして生成したいことを示すために、
'_'を三連した記号___を使います。
(後に、___を書くのを避けるためにforwardsという略記用タクティックを導入します。)
Lemma demo_lets_2 : forall (G:context) (x:string) (T:ty), True.
Proof.
intros G x T.
lets (S & Eq & Sub): typing_inversion_var G x T ___.
Abort.
通常、has_type G (var x) T を証明するのに適したコンテキスト
Gと型Tは1つだけしかないので、
実はGとTを明示的に与えることに煩わされる必要はありません。
lets (S & Eq & Sub): typing_inversion_var x とすれば十分です。
このとき、変数GとTは存在変数を使って具体化されます。
Lemma demo_lets_3 : forall (x:string), True.
Proof.
intros x.
lets (S & Eq & Sub): typing_inversion_var x ___.
Abort.
さらに進めて、typing_inversion_varの具体化のために引数をまったく与えないこともできます。
この場合、3つの単一化変数が導入されます。
注意: letsに補題の名前だけを引数として与えた場合、
その補題が証明コンテキストに追加されるだけで、
その引数を具体化しようとすることは行いません。
letsの最後の便利な機能は '_' を2つ続けた記号__です。
これを使うと、いくつかの引数が同じ型を持つとき引数を1つスキップできます。
以下の例は、仮定が二つの自然数mとnについて量化されている場合です。
mを値3に具体化したい一方、nは存在変数を使って具体化したい場面です。
これは lets K: H __ 3 と書くことで達成できます。
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.
Abort.
注意: lets H: E0 E1 E2 の代わりに lets: E0 E1 E2 と書くことができます。
この場合、Hの名前は適宜付けられます。
注意: タクティックletsは5つまでの引数をとることができます。
5個を越える引数を与えることができる場合に、別の構文があります。
キーワード>>から始まるリストを使ったものです。
例えば lets H: (>> E0 E1 E2 E3 E4 E5 E6 E7 E8 E9 10) と書きます。
タクティックapplys、forwards、specializesは
letsを特定の用途に使う場面での略記法です。
applysの使用例は以下で出てきます。
forwardsの使用例は、チュートリアルの章UseAutoにあります。
- 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 と続けることと同じです。
以下の証明では、destructの代わりにletsを、
applyの代わりにapplysを使う方法を見せます。
また、練習問題として埋めるいくつかの部分も残されています。
Lemma substitution_preserves_typing : forall Gamma x U v t S,
has_type (update Gamma x U) t S ->
has_type empty v U ->
has_type Gamma ([x:=v]t) S.
Proof with eauto.
intros Gamma x U v t S Htypt Htypv.
generalize dependent S. generalize dependent Gamma.
(induction t); intros; simpl.
-
rename s into y.
lets (T&Hctx&Hsub): typing_inversion_var Htypt.
unfold update, t_update in Hctx.
destruct (eqb_stringP x y)...
+
subst.
inversion Hctx; subst. clear Hctx.
apply context_invariance with empty...
intros x Hcontra.
lets [T' HT']: free_in_context S (@empty ty) Hcontra...
inversion HT'.
-
admit.
-
rename s into y. rename t into T1.
lets (T2&Hsub&Htypt2): typing_inversion_abs Htypt.
applys T_Sub (Arrow T1 T2)...
apply T_Abs...
destruct (eqb_stringP x y).
+
eapply context_invariance...
subst.
intros x Hafi. unfold update, t_update.
destruct (eqb_stringP y x)...
+
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (eqb_stringP y z)...
subst. rewrite false_eqb_string...
-
lets: typing_inversion_true Htypt...
-
lets: typing_inversion_false Htypt...
-
lets (Htyp1&Htyp2&Htyp3): typing_inversion_if Htypt...
-
lets: typing_inversion_unit Htypt...
Admitted.
End ExamplesInstantiations.
本章では、証明スクリプトを簡潔で変更に強くするタクティックをいくつか紹介しました。
これらを使えばより証明の生産性が向上するでしょう。
もし LibTactics.v を自分の作る証明に使いたい場合は、
http://www.chargueraud.org/softs/tlc/
から最新版を取得してください。
- inversionの名前付けをよりよくするintrovとinverts。
- 証明できないゴールを捨てやすくするfalseとtryfalse。
- 先頭の定義を展開する（unfoldする）unfolds。
- 帰納法の状況を整えやすくするgen。
- 場合分けをよりよくするcasesとcases_if。
- n-引数コンストラクタを扱うsplitsとbranch。
- 等価性を扱いやすくするasserts_rewrite、cuts_rewrite、substs、fequals。
- 補題の具体化と使用方法を表現するlets、forwards、specializes、applys。
- 補題を適用する前に行う書き換えを自動化するapplys_eq。
- 柔軟に集中、無視するサブゴールを選ぶadmits、admit_rewrite、admit_goal。