UseAuto_J: Coqの証明自動化の理論と実際¶

機械がチェックした証明においては、細部の一つ一つの正しさが確認されています。これが巨大な証明記述にもなります。幸い、Coqは証明探索メカニズムと決定手続きを持っていて、それにより証明の小さな部分を自動合成することができます。自動化は設定を適切に行えば非常に強力です。この章の目的は自動化の扱い方の基本を説明することです。

この章は2つの部分から成ります。第一部は証明探索(“proof search”)と呼ばれる一般的メカニズムに焦点を当てます。簡単に言うと、証明探索は、証明が終わるまで、単純に補題と仮定を可能なすべての方法で適用してみようとします。第二部は決定手続き(“decision procedures”)について記述します。それらは、Coqの論理の特定の断片についての証明課題を解くことを得意とするタクティックです。

この章の例には、自動化の特定の側面を示す小さな補題から、「ソフトウェアの基礎」(SoftwareFoundations)の他の部分から抽出した大きな例までを含みます。大きな例においては、ライブラリLibTactics_J.vのタクティックが使用されます。それらのタクティックについてはUseTactics_J.v章に記述されています。(この章の後半を理解するにはUseTactics_J.v章を読んでおくべきです。しかし、前半は他の知識を必要としません。)

Require Import LibTactics_J.

証明探索の基本性質¶

証明探索のアイデアは、補題や仮定を適用するタクティックの列を、例えばautoのような1つのタクティックで置き換えることです。この形の証明自動化で、たくさんの作業を省くことができます。典型的には証明記述ははるかに短くなり、またその記述は典型的にはより変更に強いものになります。もし定義に何か小さな変更をした場合、自動化を使った証明はおそらく何の変更も必要ありません。もちろん、自動化の使い過ぎはよいことではありません。証明記述が証明の主要議論をもはや記録していないときには、定義の変更で証明が成立しなくなったときに、直すことは難しくなります。全体として、自動化の適度の利用は大きな勝利です。証明の構築と、その後のメンテナンスの時間を、ともに大きく減らすことができます。

証明探索の強さ¶

これから4つの証明探索のタクティックを勉強します:auto、eauto、iauto、jautoです。タクティックautoとeautoはCoqのビルトインです。タクティックiautoはビルトインのタクティックtry solve [intuition eauto]の略記法です。タクティックjautoはライブラリLibTactics_Jに定義されています。このタクティックは単にeautoを呼ぶ前にゴールにある前処理を行います。この章のゴールは証明探索の一般原理を説明し、与えられたゴールを解くために上述の4つのタクティックのうちどれが一番適当かを推測する経験則を示すことです。

証明探索は効率と表現力の妥協案です。つまり、どれだけ複雑なゴールを解くことができるか、と、タクティックが停止するまでにどれだけの時間を必要とするかのトレードオフです。タクティックautoは、基本タクティックreflexivity、assumption、applyだけを使って証明を構築します。タクティックeautoはこれに加えてeapplyも使います。タクティックjautoはeautoを拡張して、コンテキストに現れる連言(and結合)と存在限量を展開することができるようにしています。タクティックiautoは連言(and結合)、選言(or結合)、否定を非常に賢い方法で扱います。しかしながらiautoはコンテキストから存在限量を展開することはできません。さらに、iautoはゴールがいくつかの選言を含む場合にとても遅くなるのが普通です。

注意するべきは、証明探索は書き換えステップ(タクティックrewrite、subst)、任意のデータ構造や述語についての場合分け分析(タクティックdestruct、inversion)、帰納法による証明(タクティックinduction)のいずれも実行しないことです。そのため証明探索は、実際は証明のたくさんの枝の最後のステップを自動化することを意図したものです。証明の全体構造を発見することはできません。

基本¶

タクティックautoは、intros、apply、assumption、reflexivityの列で証明できるゴールを証明することができます。以下で2つの例を示します。1つ目の例はautoがreflexivityをいつでも呼べることを示します。実際、autoは常に最初にreflexivityを適用しようとします。

Lemma solving_by_reflexivity :
  2 + 3 = 5.
Proof. auto. Qed.

2つ目の例はapplyを2回続けて呼ぶ必要がある証明です。ゴールは、任意のnについてQ nならばP nであり、かつ任意のnについてQ nが成立するならば、P 2が成立する、というものです。

Lemma solving_by_apply : forall (P Q : nat->Prop),
  (forall n, Q n -> P n) ->
  (forall n, Q n) ->
  P 2.
Proof. auto. Qed.

autoに、どのような証明を見つけたのか教えてもらうことができます。そのためには、autoの代わりにinfo autoとして呼びます。

Lemma solving_by_apply' : forall (P Q : nat->Prop),
  (forall n, Q n -> P n) ->
  (forall n, Q n) ->
  P 2.
Proof. info auto. Qed.

タクティックautoはapplyを呼ぶことがありますが、eapplyは呼びません。そのためautoは、証明のゴールから直接具体化できない補題は使うことができません。そのような補題を使うためにはタクティックeautoを呼ぶ必要があります。eautoはeapplyを呼ぶことができます。

以下の例では、最初の仮定は、あるmについてQ mが真のとき、P nが真であると主張しています。そして、ゴールはQ 1ならばP 2を証明することです。この含意は、仮定の中のmを値1で具体化することから得られます。次の証明記述はeautoが証明に成功し、一方autoはそうではないことを示します。

Lemma solving_by_eapply : forall (P Q : nat->Prop),
  (forall n m, Q m -> P n) ->
  Q 1 -> P 2.
Proof. auto. eauto. Qed.

注記: 同様に、info eautoを使うとeautoが何を見つけたかを知ることができます。

連言¶

ここまで、eautoがeapplyを使えるという意味でautoより強いことを見てきました。同様に、ここでは、jautoとiautoが連言に対してより優れたサポートをしているという点で、autoやeautoより強いことを見ます。

タクティックautoとeautoはF /\ F'という形のゴールを証明できます。ここでFとF'は2つの命題で、両者とも現在のコンテキストですぐに証明できるものです。次はその例です。

Lemma solving_conj_goal : forall (P : nat->Prop) (F : Prop),
  (forall n, P n) -> F -> F /\ P 2.
Proof. auto. Qed.

しかしながら、仮定が連言の場合、autoとeautoはこの連言を使うことができません。eautoがとても複雑なゴールを証明できるのに、「F /\ F'ならばF」を証明できないことに、最初はとても驚きます。タクティックiautoとjautoはコンテキストの連言を分解することができます。次はその例です。

Lemma solving_conj_hyp : forall (F F' : Prop),
  F /\ F' -> F.
Proof. auto. eauto. jauto.  Qed.

タクティックjautoは、最初にjauto_setという前処理のタクティックを呼び、その後eautoを呼ぶように作られています。これから、jautoがどうはたらくかを理解するためには、タクティックjauto_setを直接呼んでみるのが良いでしょう。

Lemma solving_conj_hyp' : forall (F F' : Prop),
  F /\ F' -> F.
Proof. intros. jauto_set. eauto. Qed.

次はiautoとjautoで解けるより複雑なゴールです。

Lemma solving_conj_more : forall (P Q R : nat->Prop) (F : Prop),
  (F /\ (forall n m, (Q m /\ R n) -> P n)) ->
  (F -> R 2) ->
  Q 1 ->
  P 2 /\ F.
Proof. jauto.  Qed.

iautoとjautoの戦略は、トップレベルの連言をグローバルに解析し、その後eautoを呼ぶというものです。このため、全称限量子を持つ仮定の、結論部の連言を扱うのが苦手です。次の例は、Coqの証明探索メカニズムの一般的な弱点を示しています。

Lemma solving_conj_hyp_forall : forall (P Q : nat->Prop),
  (forall n, P n /\ Q n) -> P 2.
Proof.
  auto. eauto. iauto. jauto.

  intros. destruct (H 2). auto.
Qed.

この状況にはちょっとがっかりします。というのは、ほとんど同じである次のゴールは自動証明できるのです。唯一の違いは、全称限量子が連言のそれぞれに別々に付けられていることです。

Lemma solved_by_jauto : forall (P Q : nat->Prop) (F : Prop),
  (forall n, P n) /\ (forall n, Q n) -> P 2.
Proof. jauto.  Qed.

選言¶

タクティックautoとeautoはゴールに現れる選言を扱うことができます。

Lemma solving_disj_goal : forall (F F' : Prop),
  F -> F \/ F'.
Proof. auto. Qed.

しかし、コンテキストに現れる選言についての推論を自動化できるのはiautoだけです。例えば、iautoは「F \/ F'ならばF' \/ F」を証明できます。

Lemma solving_disj_hyp : forall (F F' : Prop),
  F \/ F' -> F' \/ F.
Proof. auto. eauto. jauto. iauto. Qed.

より一般に、iautoは連言、選言、否定の複雑な組み合わせを扱うことができます。次はその例です。

Lemma solving_tauto : forall (F1 F2 F3 : Prop),
  ((~F1 /\ F3) \/ (F2 /\ ~F3)) ->
  (F2 -> F1) ->
  (F2 -> F3) ->
  ~F2.
Proof. iauto. Qed.

しかしながら、iautoが選言の場合分けを自動実行する能力には、悪い面もあります。iautoは非常に遅くなることがあるのです。コンテキストが数個の選言を含む仮定を持つとき、iautoは通常、その指数の数のサブゴールを作り、その1つ1つについてeautoを呼びます。iautoと比べたjautoの長所は、このような場合分けをする時間を費さないことです。

存在限量¶

タクティックeauto、iauto、jautoは結論部が存在限量であるゴールを証明することができます。例えばゴールがexists x, f xのとき、タクティックeautoはxの場所に存在変数を導入します。それを?25としましょう。残ったゴールはf ?25になります。そしてeautoは、?25を何らかの適当な値で具体化することで、これを解こうとします。例えば、仮定f 2があるならば、変数?25を2で置換してゴールが解決されます。以下の通りです。

Lemma solving_exists_goal : forall (f : nat->Prop),
  f 2 -> exists x, f x.
Proof.
  auto.
  eauto.
Qed.

証明探索の他のタクティックと比べたjautoの主な長所は、存在限量された、つまりexists x, Pという形の「仮定」を使える点です。

Lemma solving_exists_hyp : forall (f g : nat->Prop),
  (forall x, f x -> g x) ->
  (exists a, f a) ->
  (exists a, g a).
Proof.
  auto. eauto. iauto.
  jauto.

Qed.

否定¶

タクティックautoとeautoは、否定の扱いに関して制限があります。これは主に、否定(~ Pと記述される)がP -> Falseと定義されているのに、この定義の展開が自動では行われないことに関係しています。次の例を見てください。

Lemma negation_study_1 : forall (P : nat->Prop),
  P 0 -> (forall x, ~ P x) -> False.
Proof.
  intros P H0 HX.
  eauto.
  unfold not in *. eauto.
Qed.

このため、タクティックiautoとjautoは前処理の中でunfold not in *を組織的に呼びます。これにより、iauto、jautoは上記のゴールをすぐに解決できます。

Lemma negation_study_2 : forall (P : nat->Prop),
  P 0 -> (forall x, ~ P x) -> False.
Proof. jauto.  Qed.

(定義の展開に関する証明探索の振る舞いについては後でまた議論します。)

等式¶

Coq の証明探索機能は等式を扱うのが不得意です。反射律、対称律といった基本的操作は行うことができますが、それぐらいです。以下はautoが解くことができる簡単な例です。最初にsymmetryを呼び、その後仮定を適用します。

Lemma equality_by_auto : forall (f g : nat->Prop),
  (forall x, f x = g x) -> g 2 = f 2.
Proof. auto. Qed.

等式についてのより高度な推論を自動化するためには、むしろタクティックcongruenceを使うべきです。これについてはこの章の終わりの「決定手続き」節で説明します。

証明探索はどのようにはたらくか¶

探索の深さ¶

タクティックautoは次のようにはたらきます。最初にreflexivityとassumptionを試してみます。もしどちらかがゴールを解いたならば仕事は完了です。そうでないときautoは、エラーにならずにゴールに適用できる仮定のうち、一番最後に導入されたものを適用することを試みます。この適用によりサブゴールが生成されます。このあと2つの場合があります。もし生成されたサブゴールがすべてautoの再帰的呼び出しにより解かれた場合、それで終了です。そうではなく、生成されたサブゴール中にautoが解けないものが1つでもある場合、やり直して、最後から2番目に導入された仮定を適用しようとします。同様のやり方を、証明を発見するか、適用する仮定がなくなるかするまで続けます。

autoタクティックの実行の際のバックトラックプロセスを明確に理解しておくことはとても重要です。そうしないと、autoの振る舞いにはかなり当惑します。例えば、autoは次の自明なものを解くことができません。

Lemma search_depth_0 :
  True /\ True /\ True /\ True /\ True /\ True.
Proof.
  auto.
Admitted.

このゴールにautoが失敗する理由は、連言の数が多すぎることです。もしこれが5個だったら、autoは証明に成功したでしょう。しかし6個は多過ぎなのです。タクティックautoは補題と仮定の数を制限することで、証明探索がいつかは停止することを保証しています。デフォルトではステップの最大数は5です。制限を別の値にするには、例えばauto 6と書くと、証明探索は最大6ステップまでになります。例えばauto 6は上記の補題を解くことができるでしょう。(同様に、eauto 6やintuition eauto 6として呼ぶことができます。)auto nの引数nは探索の深さ(“search depth”)と呼ばれます。タクティックautoは単にauto 5の略記法として定義されています。

auto nの振る舞いは次のように要約されます。最初にゴールをreflexivityとassumptionを使って解こうとします。もし失敗したときは、仮定(またはヒントデータベースに登録された補題)を適用しようとします。これによりいくつものサブゴールが生成されます。このそれぞれのサブゴールに対してタクティックauto (n-1)が呼ばれます。もしすべてのサブゴールが解かれたならば処理は完了です。そうでなければ、auto nは別の仮定を適用しようとします。

この過程は、auto nはauto (n-1)を呼び、次にauto (n-1)はauto (n-2)を呼び... と続きます。タクティックauto 0が適用を試みるのはreflexivityとassumptionだけで、補題を適用しようとすることはありません。これは全体として、指定されたステップ数の上限値に逹したときには、autoタクティックは探索を中止し、バックトラックして別のパスを調べることを意味します。

次の補題には1つだけ証明があり、それは3ステップです。このため、auto nは、nが3以上の時これを証明し、3未満のときは証明できません。

Lemma search_depth_1 : forall (P : nat->Prop),
  P 0 ->
  (P 0 -> P 1) ->
  (P 1 -> P 2) ->
  (P 2).
Proof.
  auto 0.
  auto 1.
  auto 2.
  auto 3.

Qed.

この例を次のように一般化することができます。すべてのkについて、P kがP (k-1)から導出されると仮定します。また、P 0が成立するとします。タクティックauto、つまりauto 5と同じですが、これは5未満のすべてのkの値についてP kを導出することができます。例えばautoはP 4を証明できます。

Lemma search_depth_3 : forall (P : nat->Prop),
   (P 0) ->
   (forall k, P (k-1) -> P k) ->
   (P 4).
Proof. auto. Qed.

しかし、P 5を証明するためには、少なくともauto 6を呼ぶ必要があります。

Lemma search_depth_4 : forall (P : nat->Prop),
   (P 0) ->
   (forall k, P (k-1) -> P k) ->
   (P 5).
Proof. auto. auto 6. Qed.

autoが限られた深さで証明を探すことから、autoがゴールFもF'も証明できるのにF /\ F'を証明できない、という場合があります。次の例では、autoはP 4を証明できますが、P 4 /\ P 4を証明できません。なぜなら連言を分解するには1ステップ必要だからです。この連言を証明するためには、探索の深さを増やして少なくともauto 6を使う必要があります。

Lemma search_depth_5 : forall (P : nat->Prop),
   (P 0) ->
   (forall k, P (k-1) -> P k) ->
   (P 4 /\ P 4).
Proof. auto. auto 6. Qed.

バックトラック¶

前の節で、各ステップでautoが適用できる仮定が唯一である証明を考えてきました。一般には、autoの各ステップでいくつかの選択肢がある場合があります。autoの戦略は、すべての可能性を(深さ優先探索によって)試してみる、というものです。

どのように自動証明がはたらくかを示すために、前の例を拡張して、P kがP (k+1)からも導出できるとします。この仮定を追加したことで、autoが各ステップで考慮する新たな選択肢が提供されます。

証明探索で考慮するすべてのステップをトレースすることができる特別なコマンドがあります。そのトレースを見るためには、debug eautoと書きます。(ある理由から、コマンドdebug autoは存在しないため、代わりにコマンドdebug eautoを使う必要があります。)

Lemma working_of_auto_1 : forall (P : nat->Prop),
   (P 0) ->
   (forall k, P (k+1) -> P k) ->
   (forall k, P (k-1) -> P k) ->
   (P 2).

Proof. intros P H1 H2 H3.  eauto. Qed.

debug eautoの出力メッセージは次の通りです。

depth=5
depth=4 apply H3
depth=3 apply H3
depth=3 exact H1

depth はeauto nが呼ばれるnの値を示します。メッセージに見られるタクティックは、eautoが最初にすることはH3を適用してみることであることを示します。H3の適用の結果、ゴールP 1はゴールP 2に代わります。すると、再度H3が適用され、ゴールP 1がP 2に代わります。この時点でゴールは仮定H1と一致します。

この場合、eautoは非常にラッキーだったようです。仮定H2を一度も使ってみようとすることもありませんでした。理由は、autoは常に最後に導入された仮定を最初に試してみることと、ゴールにおいてH3はH2より後で導入された仮定であることです。それでは、仮定H2とH3を入れ替えるとどうなるか見てみましょう。

Lemma working_of_auto_2 : forall (P : nat->Prop),
   (P 0) ->
   (forall k, P (k-1) -> P k) ->
   (forall k, P (k+1) -> P k) ->
   (P 2).
Proof. intros P H1 H3 H2.  eauto. Qed.

このとき、出力メッセージは証明探索がたくさんの可能性を調べることを示唆しています。debug eautoをinfo eautoに替えると、eautoが見つける証明は実際に単純なものではないことを見ることができます。

apply H2; apply H3; apply H3; apply H3; exact H1

この証明は、証明課題P 3を調べます。たとえそれが何の役にも立たなくてもです。以下に描かれた木は自動証明が通ったすべてのゴールを記述しています。

|5||4||3||2||1||0| -- 以下で、タブは深さを示しています

[P 2]
-> [P 3]
   -> [P 4]
      -> [P 5]
         -> [P 6]
            -> [P 7]
            -> [P 5]
         -> [P 4]
            -> [P 5]
            -> [P 3]
      --> [P 3]
         -> [P 4]
            -> [P 5]
            -> [P 3]
         -> [P 2]
            -> [P 3]
            -> [P 1]
   -> [P 2]
      -> [P 3]
         -> [P 4]
            -> [P 5]
            -> [P 3]
         -> [P 2]
            -> [P 3]
            -> [P 1]
      -> [P 1]
         -> [P 2]
            -> [P 3]
            -> [P 1]
         -> [P 0]
            -> !! 完了です !!

最初の数行は次のように読みます。P 2を証明するためにeauto 5は最初にH2を適用しサブゴールP 3を作ります。これを解くために、eauto 4は再度H2を適用し、ゴールP 4を作ります。同様に探索はP 5、P 6、P 7と進みます。P 7に逹したときタクティックeauto 0が呼ばれますが、eauto 0は補題を適用することができないため、失敗します。このためゴールP 6に戻り、ここでは仮定H3を適用し、サブゴールP 5を生成します。ここでまたeauto 0はこのゴールを解くことに失敗します。

このプロセスは延々と続きます。P 3までバックトラックし、H2を3回連続して適用してP 2、P 1、P 0と進むまでは。この探索木は、eautoがなぜapply H2から始まる証明を発見できるかを説明しています。

ヒントを追加する¶

デフォルトでは、auto(およびeauto)は証明コンテキストに現れる仮定だけを適用しようとします。それより前に証明した補題を使うことをautoに教えてやる方法は2つあります。1つはautoを呼ぶ直前に補題を仮定として加えてやることです。もう1つは、補題をヒントとして追加することです。そうすると、autoを呼ぶときいつでもそれを使うことができるようになります。

1つ目の方法は、この特定の場所のためだけに補題をautoに使わせるのに便利です。補題を仮定として追加するためには、generalize mylemma; intros、あるいは単にlets: mylemmaと打ちます(後者にはLibTactics_J.vが必要です)。

2つ目の方法は何回も補題を使う必要がある場合に便利です。補題をヒントに追加する構文はHint Resolve mylemmaです。例えば、任意の数値は自分以下であるという補題forall x, x <= xはCoq標準ライブラリではLe.le_reflと呼ばれていますが、これをヒントとして追加するには次のようにします。

Hint Resolve Le.le_refl.

帰納的データ型のすべてのコンストラクタをヒントとして追加する便利な略記法がコマンドHint Constructors mydatatypeです。

ワーニング: いくつかの補題、推移律のようなものは、ヒントとして追加するべきではありません。証明探索のパフォーマンスに非常に悪い影響を与えるからです。この問題の記述と推移律の一般的な回避策の提示は後で出てきます。

タクティックへの自動証明の統合¶

ライブラリ “LibTactics” はタクティックを呼んだ後で自動証明を呼ぶ便利な機能を提供します。要するに、タクティック名に星印(*)をつければ良いのです。例えば、apply* Hはapply H; auto_starと等価です。ここでauto_starは必要なように定義できます。デフォルトでは、auto_starは最初にautoを使ってゴールを解こうとします。そしてそれに成功しなかった場合jautoを呼ぼうとします。jautoの強さがautoを越えているのに、autoを先に呼ぶのは意味があります。autoで成功した場合、かなりの時間を節約できるかもしれません。そしてautoが証明に失敗するときには、非常に速く失敗するのです。

星印の意味を定めるauto_starの定義は、いつでも必要なときに変更できます。単に次のように書きます:

Ltac auto_star ::= a_new_definition.

ここで、:=ではなく::=が使われていることを見てください。これは、このタクティックが新しい定義に再束縛されていることを示しています。そのデフォルトの定義は次の通りです。

Ltac auto_star ::= try solve [ auto | jauto ].

標準のCoqタクティックのほとんどすべてと、”LibTactics”のタクティックのすべては、星印を付けて呼ぶことができます。例えば、subst*、destruct* H、inverts* H、lets* I: H x、specializes* H x、等々が可能です。注記すべき例外が2つあります。タクティックauto*はauto_starの別名です。また、タクティックapply* Hはeapply H(または、もし必要ならばより強力なapplys H)を呼び、その後auto_starを呼びます。eapply* Hタクティックは存在しないので、代わりにapply* Hを呼ぶように注意してください。

大きな開発では、2つの段階の自動化を使うのが便利でしょう。典型的には、1つはautoのような速いタクティック、もう1つはjautoのように遅いけれどもより強力なタクティックです。2種類の自動化をスムーズに共存させるために、LibTactics_J.vはタクティックにチルダ(~)を付けるバージョンも定義しています。apply~ H、destruct~ H、subst~、auto~などです。チルダ記号の意味はauto_tildeタクティックによって記述されています。このデフォルトの実装はautoです。

Ltac auto_tilde ::= auto.

以降の例では、auto_starだけが必要です。

自動化の使用例¶

「ソフトウェアの基礎」(“Software Foundations”)コースの主要定理に証明探索を実際にどのように使うかを見てみましょう。決定性、保存、進行などの特定の結果を証明します...

決定性¶

Module DeterministicImp.
  Require Import Imp_J.

Imp言語の決定性補題のオリジナルの証明を振り返ってみましょう。以下の通りです。

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; inversion E2; subst.
  Case "E_Skip". reflexivity.
  Case "E_Ass". reflexivity.
  Case "E_Seq".
    assert (st' = st'0) as EQ1.
      SCase "Proof of assertion". apply IHE1_1; assumption.
    subst st'0.
    apply IHE1_2. assumption.
  Case "E_IfTrue".
    SCase "b1 evaluates to true".
      apply IHE1. assumption.
    SCase "b1 evaluates to false (contradiction)".
      rewrite H in H5. inversion H5.
  Case "E_IfFalse".
    SCase "b1 evaluates to true (contradiction)".
      rewrite H in H5. inversion H5.
    SCase "b1 evaluates to false".
      apply IHE1. assumption.
  Case "E_WhileEnd".
    SCase "b1 evaluates to true".
      reflexivity.
    SCase "b1 evaluates to false (contradiction)".
      rewrite H in H2. inversion H2.
  Case "E_WhileLoop".
    SCase "b1 evaluates to true (contradiction)".
      rewrite H in H4. inversion H4.
    SCase "b1 evaluates to false".
      assert (st' = st'0) as EQ1.
        SSCase "Proof of assertion". apply IHE1_1; assumption.
      subst st'0.
      apply IHE1_2. assumption.
Qed.

練習問題: この証明を可能な限りautoを使って書き直しなさい。

Theorem ceval_deterministic': forall c st st1 st2,
  c / st || st1 ->
  c / st || st2 ->
  st1 = st2.
Proof.
  (* FILL IN HERE *) admit.
Qed.

実際、自動化の利用は、ただ1つや2つの別のタクティックの代わりにautoを使うというようなことではないのです。自動化の利用は、証明を記述しメンテナンスする作業を最小化するために、タクティック列の構成を再考することなのです。このプロセスはLibTactics_J.vのタクティックを使うことで楽になります。そこで、自動化の使用法の最適化に取り組む前に、まず決定性の証明を書き直してみましょう:

intros x Hの代わりにintrov Hを使います
generalize dependent xの代わりにgen xを使います
generalize dependent xの代わりにgen xを使います
inversion H; substの代わりにinverts Hを使います
矛盾を扱うためにtryfalseを使い、コンテキストにbeval st b1 = trueとbeval st b1 = falseの両者が現れているのを除去します
場合にラベルを付けるためのceval_casesの使用を止めます。

Theorem ceval_deterministic’‘: forall c st st1 st2, c / st || st1 -> c / st || st2 -> st1 = st2. Proof. introv E1 E2. gen st2. induction E1; intros; inverts E2; tryfalse. auto. auto. assert (st’ = st‘0). auto. subst. auto. auto. auto. auto. assert (st’ = st‘0). auto. subst. auto. Qed.

きれいな証明記述を得るためには、assert (st' = st'0)の呼び出しを消去しなければなりません。このようなタクティックの呼び出しは、きれいではありません。なぜなら、自動命名された変数を参照しているからです。こういうタクティックはとても脆弱なものになりやすいのです。タクティックassert (st' = st'0)は帰納法の仮定から導出したい結論を主張するのに使われています。そこで、この結論を明示的に述べる代わりに、帰納法の仮定を具体化する際に自動処理によって計算される具体化法を使うようにCoqに伝えてみましょう。LibTactics_J.vに記述されたタクティックforwardsは、事実の具体化について的確に助けてくれます。それでは、この例についてどのようにはたらくか見てみましょう。

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

  introv E1 E2. gen st2.
  induction E1; intros; inverts E2; tryfalse.
  auto. auto.

  dup 4.


  assert (st' = st'0). apply IHE1_1. apply H1.
     skip.


  forwards: IHE1_1. apply H1.
     skip.


  forwards: IHE1_1. eauto.
     skip.


  forwards*: IHE1_1.
     skip.

Admitted.

証明記述を洗練するために、星印を使って呼び出しをautoに分解することが残っています。そうすると、決定性の証明はたった4行の10個を越えないタクティックに書き直されます。

Theorem ceval_deterministic'''': forall c st st1 st2,
  c / st || st1  ->
  c / st || st2 ->
  st1 = st2.
Proof.
  introv E1 E2. gen st2.
  induction E1; intros; inverts* E2; tryfalse.
  forwards*: IHE1_1. subst*.
  forwards*: IHE1_1. subst*.
Qed.

End DeterministicImp.

STLC の保存¶

Module PreservationProgressStlc.
  Require Import Stlc_J.
  Import STLC.

STLC の保存の証明を振り返ってみましょう。次の通りです。この証明では既にドット3つ(...)のメカニズムを通じてeautoを使っています。

Theorem preservation : forall t t' T,
  has_type empty t T  ->
  t ==> t'  ->
  has_type empty t' T.
Proof with eauto.
  remember (@empty ty) as Gamma.
  intros t t' T HT. generalize dependent t'.
  (has_type_cases (induction HT) Case); intros t' HE; subst Gamma.
  Case "T_Var".
    inversion HE.
  Case "T_Abs".
    inversion HE.
  Case "T_App".
    inversion HE; subst...


    SCase "ST_AppAbs".
      apply substitution_preserves_typing with T11...
      inversion HT1...
  Case "T_True".
    inversion HE.
  Case "T_False".
    inversion HE.
  Case "T_If".
    inversion HE; subst...
Qed.

練習問題: この証明をLibTacticsのタクティックを使って書き直しなさい。そして、...の代わりに星印を使って自動証明を呼びなさい。より詳しくは、invertsあるいはapplysの後でauto*を呼ぶためにinverts*とapplys*を使いなさい。解は3行の長さです。

Theorem preservation' : forall t t' T,
  has_type empty t T  ->
  t ==> t'  ->
  has_type empty t' T.
Proof.
  (* FILL IN HERE *) admit.
Qed.

STLC の前進¶

前進定理の証明を振り返りましょう。

Theorem progress : forall t T,
  has_type empty t T ->
  value t \/ exists t', t ==> t'.
Proof with eauto.
  intros t T Ht.
  remember (@empty ty) as Gamma.
  (has_type_cases (induction Ht) Case); subst Gamma...
  Case "T_Var".
    inversion H.
  Case "T_App".
    right. destruct IHHt1...
    SCase "t1 is a value".
      destruct IHHt2...
      SSCase "t2 is a value".
        inversion H; subst; try solve by inversion.
        exists (subst t2 x t)...
      SSCase "t2 steps".
       destruct H0 as [t2' Hstp]. exists (tm_app t1 t2')...
    SCase "t1 steps".
      destruct H as [t1' Hstp]. exists (tm_app t1' t2)...
  Case "T_If".
    right. destruct IHHt1...
    destruct t1; try solve by inversion...
    inversion H. exists (tm_if x t2 t3)...
Qed.

練習問題: 前進定理の証明を最適化しなさい。ヒント:destruct*とinverts*を使いなさい。解は10行の長さです(行は短いです)。

Theorem progress' : forall t T,
  has_type empty t T ->
  value t \/ exists t', t ==> t'.
Proof.
  (* FILL IN HERE *) admit.
Qed.

End PreservationProgressStlc.

ビッグステップとスモールステップ¶

Module Semantics.
Require Import Smallstep_J.

スモールステップ簡約ジャッジメントとビッグステップ簡約ジャッジメントを関係づける証明を振り返りましょう。

Theorem stepmany__eval : forall t v,
  normal_form_of t v -> t || v.
Proof.
  intros t v Hnorm.
  unfold normal_form_of in Hnorm.
  inversion Hnorm as [Hs Hnf]; clear Hnorm.
  apply nf_is_value in Hnf. inversion Hnf. clear Hnf.
  (rsc_cases (induction Hs) Case); subst.
  Case "rsc_refl".
    apply E_Const.
  Case "rsc_step".
    eapply step__eval. eassumption. apply IHHs. reflexivity.
Qed.

練習問題: 上の証明を、introv、invert、applys*を使って最適化しなさい。解は4行の長さです。

Theorem stepmany__eval' : forall t v,
  normal_form_of t v -> t || v.
Proof.
  (* FILL IN HERE *) admit.
Qed.

End Semantics.

STLCRef の保存¶

Module PreservationProgressReferences.
  Require Import References_J.
  Import STLCRef.
  Hint Resolve store_weakening extends_refl.

STLCRefの保存の証明はReferences_J.vにあります。(場合にラベル付けをする行を除いて)58行です。最適化された証明は2分の1以下の短かさになります。以下の資料は最適化された証明記述をどのように構築するかを説明します。最適化された結果の保存定理の証明記述は、後で出てきます。

Theorem preservation : forall ST t t' T st st',
  has_type empty ST t T ->
  store_well_typed ST st ->
  t / st ==> t' / st' ->
  exists ST',
    (extends ST' ST /\
     has_type empty ST' t' T /\
     store_well_typed ST' st').
Proof.


  remember (@empty ty) as Gamma. introv Ht. gen t'.
  (has_type_cases (induction Ht) Case); introv HST Hstep;

   subst Gamma; inverts Hstep; eauto.

  Case "T_App".
  SCase "ST_AppAbs".


  exists ST. inverts Ht1. splits*. applys* substitution_preserves_typing.

  SCase "ST_App1".


  forwards: IHHt1. eauto. eauto. eauto.

  jauto_set_hyps; intros.

  jauto_set_goal; intros.

  eauto. eauto. eauto.

  SCase "ST_App2".


  forwards*: IHHt2.


  forwards*: IHHt.
  forwards*: IHHt.
  forwards*: IHHt1.
  forwards*: IHHt2.
  forwards*: IHHt1.

  Case "T_Ref".
  SCase "ST_RefValue".


  exists (snoc ST T1). inverts keep HST. splits.

    apply extends_snoc.

    applys_eq T_Loc 1.

      rewrite length_snoc. omega.

    unfold store_ty_lookup. rewrite <- H. rewrite* nth_eq_snoc.

    apply* store_well_typed_snoc.

  forwards*: IHHt.

  Case "T_Deref".
  SCase "ST_DerefLoc".


  exists ST. splits*.

  lets [_ Hsty]: HST.

  applys_eq* Hsty 1.

  inverts* Ht.

  forwards*: IHHt.

  Case "T_Assign".
  SCase "ST_Assign".


  exists ST. splits*. applys* assign_pres_store_typing. inverts* Ht1.

  forwards*: IHHt1.
  forwards*: IHHt2.
Qed.

証明の最適化が難しい場合に戻りましょう。困難さの原因はnth_eq_snocです。これは、nth (length l) (snoc l x) d = xをとります。この補題は使うのが難しいのです。それは最初の引数length lがlに言及していて、それがsnoc l xに現れるlと完全に同じだからです。実際、通常は引数は自然数nで、これはlength lと等しいかもしれませんが、構文的にはlength lと違っています。nth_eq_snocを適用しやすくする簡単な修正方法があります。中間的な変数nを明示的に導入し、ゴールをnth n (snoc l x) d = xにします。そして、その際に仮定n = length lを加えます。

Lemma nth_eq_snoc' : forall (A : Type) (l : list A) (x d : A) (n : nat),
  n = length l -> nth n (snoc l x) d = x.
Proof. intros. subst. apply nth_eq_snoc. Qed.

保存定理の証明のrefの場合は、はるかに簡単に証明できるようになります。rewrite nth_eq_snoc'が成功するからです。

Lemma preservation_ref : forall (st:store) (ST : store_ty) T1,
  length ST = length st ->
  ty_Ref T1 = ty_Ref (store_ty_lookup (length st) (snoc ST T1)).
Proof.
  intros. dup.


  unfold store_ty_lookup. rewrite* nth_eq_snoc'.


  fequal. symmetry. apply* nth_eq_snoc'.
Qed.

保存の最適化された証明は次のようにまとめられます。

Theorem preservation' : forall ST t t' T st st',
  has_type empty ST t T ->
  store_well_typed ST st ->
  t / st ==> t' / st' ->
  exists ST',
    (extends ST' ST /\
     has_type empty ST' t' T /\
     store_well_typed ST' st').
Proof.
  remember (@empty ty) as Gamma. introv Ht. gen t'.
  induction Ht; introv HST Hstep; subst Gamma; inverts Hstep; eauto.
  exists ST. inverts Ht1. splits*. applys* substitution_preserves_typing.
  forwards*: IHHt1.
  forwards*: IHHt2.
  forwards*: IHHt.
  forwards*: IHHt.
  forwards*: IHHt1.
  forwards*: IHHt2.
  forwards*: IHHt1.
  exists (snoc ST T1). inverts keep HST. splits.
    apply extends_snoc.
    applys_eq T_Loc 1.
      rewrite length_snoc. omega.
      unfold store_ty_lookup. rewrite* nth_eq_snoc'.
    apply* store_well_typed_snoc.
  forwards*: IHHt.
  exists ST. splits*. lets [_ Hsty]: HST.
   applys_eq* Hsty 1. inverts* Ht.
  forwards*: IHHt.
  exists ST. splits*. applys* assign_pres_store_typing. inverts* Ht1.
  forwards*: IHHt1.
  forwards*: IHHt2.
Qed.

STLCRef の前進¶

STLCRefの前進の証明はファイルReferences_J.vにあります。その証明は53行で、最適化された証明記述は、また、2分の1になります。

Theorem progress : forall ST t T st,
  has_type empty ST t T ->
  store_well_typed ST st ->
  (value t \/ exists t', exists st', t / st ==> t' / st').
Proof.
  introv Ht HST. remember (@empty ty) as Gamma.
  induction Ht; subst Gamma; tryfalse; try solve [left*].
  right. destruct* IHHt1 as [K|].
    inverts K; inverts Ht1.
     destruct* IHHt2.
  right. destruct* IHHt as [K|].
    inverts K; try solve [inverts Ht]. eauto.
  right. destruct* IHHt as [K|].
    inverts K; try solve [inverts Ht]. eauto.
  right. destruct* IHHt1 as [K|].
    inverts K; try solve [inverts Ht1].
     destruct* IHHt2 as [M|].
      inverts M; try solve [inverts Ht2]. eauto.
  right. destruct* IHHt1 as [K|].
    inverts K; try solve [inverts Ht1]. destruct* n.
  right. destruct* IHHt.
  right. destruct* IHHt as [K|].
    inverts K; inverts Ht as M.
      inverts HST as N. rewrite* N in M.
  right. destruct* IHHt1 as [K|].
    destruct* IHHt2.
     inverts K; inverts Ht1 as M.
     inverts HST as N. rewrite* N in M.
Qed.

End PreservationProgressReferences.

サブタイプ¶

Module SubtypingInversion.
  Require Import Subtyping_J.

サブタイプを持つ型システムの抽象化の型ジャッジメントに関する反転補題を振り返ってみましょう。

Lemma abs_arrow : forall x S1 s2 T1 T2,
  has_type empty (tm_abs x S1 s2) (ty_arrow T1 T2) ->
     subtype T1 S1
  /\ has_type (extend empty x S1) s2 T2.
Proof with eauto.
  intros x S1 s2 T1 T2 Hty.
  apply typing_inversion_abs in Hty.
  destruct Hty as [S2 [Hsub Hty]].
  apply sub_inversion_arrow in Hsub.
  destruct Hsub as [U1 [U2 [Heq [Hsub1 Hsub2]]]].
  inversion Heq; subst...
Qed.

練習問題:introv、lets、inverts*を使って証明記述を最適化しなさい。特にapply K in H. destruct H as Iをlets I: K Hに置き換えることは有効です。解は4行です。

Lemma abs_arrow' : forall x S1 s2 T1 T2,
  has_type empty (tm_abs x S1 s2) (ty_arrow T1 T2) ->
     subtype T1 S1
  /\ has_type (extend empty x S1) s2 T2.
Proof.
  (* FILL IN HERE *) admit.
Qed.

補題substitution_preserves_typingはファイルUseTactics_J.vでletsとapplysのはたらきを示すために既に使われています。この証明のさらなる最適化を、(星印付きの)自動処理とタクティックcases_if'を使って行いなさい。解は33行で、Case命令を含みます。

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.
  (* FILL IN HERE *) admit.
Qed.

End SubtypingInversion.

証明探索の進んだ話題¶

補題を正しい方法で記述する¶

深さ優先探索のため、eautoは探索の深さが増えるにつれ指数的に遅くなります。短かい証明が存在する場合でもそうです。一般に、証明探索を合理的な速さにするため、証明の深さを5から6を越える深さの探索は避けるべきです。さらに、適用可能な補題の数を最小化し、通常は証明の中で存在変数を具体化する仮定を最初に置くべきです。

実際、eautoが特定のゴールを解く能力は、仮定がどの順番で記述されるかに依存します。このことが以下の例で示されます。この例では、Pは自然数についての述語です。この述語は、P mが0以外のいずれかのmについて成立するとき、任意のnについてP nが成立するというものです。ゴールは、P 2ならばP 1を証明することです。Pについての仮定がforall n m, P m -> m <> 0 -> P nの形で主張されるとき、eautoははたらきます。しかしながら、forall n m, m <> 0 -> P m -> P nのときはタクティックeautoは失敗します。

Lemma order_matters_1 : forall (P : nat->Prop),
  (forall n m, P m -> m <> 0 -> P n) -> P 2 -> P 1.
Proof.
  eauto.

Qed.

Lemma order_matters_2 : forall (P : nat->Prop),
  (forall n m, m <> 0 -> P m -> P n) -> P 5 -> P 1.
Proof.
  eauto.


  intros P H K.
  eapply H.


  eauto.

Admitted.

理解の上で重要な点は、仮定forall n m, P m -> m <> 0 -> P nはeautoに優しく、一方forall n m, m <> 0 -> P m -> P nは実際はそうではない、ということです。P mが成立するmの値を推測し、それからm <> 0が成立することをチェックするのがうまくいくのは、P mが成立するmがほとんどないからです。これから、eautoが正しいmを見つける可能性は高いのです。一方、m <> 0となるmの値を推測し、それからP mが成立するかをチェックすることはうまくいきません。なぜなら、m <> 0でありながらP mではないmはたくさんあるからです。

証明検索中で定義を展開する¶

中間的定義を使うことは通常、主張をより簡潔に、より読みやすくすることから、形式的開発では一般に奨励されます。しかし定義は、証明を自動化することを少し難しくします。問題は、証明探索メカニズムにとって、定義を展開しなければならないのがいつかが明らかではないことです。ここで、証明探索を呼ぶ前にすべての定義を展開しておくという素朴な戦略は、大きな証明ではスケールしない(拡大適用できない)ため、それは避ける、ということに注意します。この節では、証明探索前に手動で定義を展開することを避けるためのいくつかのテクニックを紹介します。

定義の扱い方を示すために、Pを自然数についての抽象述語で、myFactを、命題3以下の任意のxについて命題P xが成立することの定義であるとします。

Axiom P : nat -> Prop.

Definition myFact := forall x, x <= 3 -> P x.

任意のxについてP xが成立するという仮定のもとでmyFactを証明することは、雑作もないことのはずです。しかし、myFactの定義を明示的に展開しない限り、autoは証明に失敗します。

Lemma demo_hint_unfold_goal_1 :
  (forall x, P x) -> myFact.
Proof.
  auto.
  unfold myFact. auto.
Qed.

証明課題に現れる定義の展開を自動化するために、コマンドHint Unfold myFactを使うことができます。こうすると、myFactがゴールに現れたときに常にmyFactを展開してみるべきであるということを、Coqに伝えることができます。

Hint Unfold myFact.

これでやっと、自動証明は、myFactの定義の中を見ることができるようになります。

Lemma demo_hint_unfold_goal_2 :
  (forall x, P x) -> myFact.
Proof. auto. Qed.

しかしながら、Hint Unfoldメカニズムがはたらくのは、ゴールに現れる定義の展開だけです。一般に証明探索は、コンテキストの定義を展開しません。例えば、True -> myFactの仮定のもとで、P 3が成立することを証明したいとします。

Lemma demo_hint_unfold_context_1 :
  (True -> myFact) -> P 3.
Proof.
  intros.
  auto.
  unfold myFact in *. auto.
Qed.

注意: 前の規則に1つ例外があります:コンテキストの定数はゴールに直接適用されるときに自動的に展開されます。例えば仮定がTrue -> myFactではなくmyFactであるとき、autoは証明に成功します。

不合理なゴールの証明の自動化¶

この節では、否定を結論部とする補題は一般にはヒントには適さないこと、そしてFalseを結論部とする補題は有用なヒントになりますが、それが多過ぎると証明探索が非効率になるということを示します。また、効率問題の現実的な回避策も見ます。

次の補題を考えましょう。この補題は、3以下の数は3を越えていないと主張しています。

Parameter le_not_gt : forall x,
  (x <= 3) -> ~ (x > 3).

等価的に、3を越える数は3以下ではないと主張することもできるでしょう。

Parameter gt_not_le : forall x,
  (x > 3) -> ~ (x <= 3).

実際、両主張は3つ目の主張：x <= 3かつx > 3は矛盾する、と、Falseを含意するという意味で同値です。

Parameter le_gt_false : forall x,
  (x <= 3) -> (x > 3) -> False.

以下でやることの狙いは、証明自動化に関しては3つの主張のうちどれが便利かを調べることです。以下の素材はSection内に入れられています。これは、追加するヒントのスコープを限定するためです。言い換えると、セクションが終わった後では、セクション内で追加されたヒントはアクティブではなくなります。

Section DemoAbsurd1.

最初の補題le_not_gtをヒントとして追加して、命題exists x, x <= 3 /\ x > 3が不合理であることを証明できるか試してみましょう。

Hint Resolve le_not_gt.

Lemma demo_auto_absurd_1 :
  (exists x, x <= 3 /\ x > 3) -> False.
Proof.
  intros. jauto_set.
   eauto.
  eapply le_not_gt. eauto. eauto.
Qed.

補題gt_not_leはle_not_gtと対称性があるため、同じことです。3つ目の補題le_gt_falseはより有効なヒントです。なぜなら、Falseが結論部になっているため、現在のゴールがFalseであるときに、証明探索が適用してみようとするからです。

Hint Resolve le_gt_false.

Lemma demo_auto_absurd_2 :
  (exists x, x <= 3 /\ x > 3) -> False.
Proof.
  dup.


  intros. jauto_set.  eauto.


  jauto.
Qed.

まとめると、H1 -> H2 -> Falseという形の補題はH1 -> ~ H2よりはるかに有効なヒントです。両者は否定記号~の定義のもとで同値であるにもかかわらずそうなのです。

しかし、Falseを結論部とする補題をヒントに追加するのは慎重に行うべきです。理由は、ゴールFalseに到達するときはいつでも、証明探索メカニズムは、適切なヒントを適用する前に、結論部がFalseであるヒントをすべて適用してみる可能性があるからです。

End DemoAbsurd1.

結論部がFalseである補題をヒントに追加することは、ローカルにはとても効率的な解です。しかし、このアプローチはグローバルなヒントにはスケールアップ(拡大適用)できません。一番現実的な適用のためには、矛盾を導くのに使う補題に名前を付けるのが合理的です。タクティックfalse Hはこの目的に有用です。このタクティックは、ゴールをFalseに置換し、eapply Hを呼びます。その振る舞いは以下で記述します。3つの主張le_not_gt、gt_not_le、le_gt_falseのいずれでも使えることを見てください。

Lemma demo_false : forall x,
  (x <= 3) -> (x > 3) -> 4 = 5.
Proof.
  intros. dup 4.


  false. eapply le_gt_false.
    auto.

    skip.


  false. eapply le_gt_false.
    eauto.
    eauto.


  false le_gt_false. eauto. eauto.


  false le_not_gt. eauto. eauto.
Qed.

上の例で、false le_gt_false; eautoはゴールを証明します。しかしfalse le_gt_false; autoはゴールを証明できません。なぜならautoは存在変数を正しく具体化しないからです。false* le_gt_falseも動作しないことに注意します。なぜなら*記号はautoを最初に呼ぶからです。ここでは、証明を完結するのに2つの可能性があります。false le_gt_false; eautoを呼ぶかfalse* (le_gt_false 3)を呼ぶかです。

推移性補題についての自動化¶

いくつかの補題はヒントに追加するべきではありません。それは、証明探索を非常に遅くするからです。典型的な例は推移的な結果についてのものです。この節では、その問題を説明し、一般的な回避策を示します。型typの2つのオブジェクトSとTの間のサブタイプ関係subtype S Tを考えましょう。この関係は反射的かつ推移的であることが証明されていると仮定します。対応する補題をsubtype_reflとsubtype_transとします。

Parameter typ : Type.

Parameter subtype : typ -> typ -> Prop.

Parameter subtype_refl : forall T,
  subtype T T.

Parameter subtype_trans : forall S T U,
  subtype S T -> subtype T U -> subtype S U.

反射性をヒントに加えるのは一般に良い考えです。サブタイプ関係の反射性をヒントに加えましょう。

Hint Resolve subtype_refl.

推移性をヒントに加えることは一般には良い考えではありません。それが何故かを理解するために、ヒントに加えてみて何が起こるか見てみましょう。一度ヒントに追加するとそれを除去することはできないので、セクション(“Section”)を設けて、推移性ヒントのスコープをそのセクションに限定するようにします。

Section HintsTransitivity.

Hint Resolve subtype_trans.

このとき、ゴールforall S T, subtype S Tを考えます。これは明らかに解ける見込みがありません。このゴールにeautoを呼んでみましょう。

Lemma transitivity_bad_hint_1 : forall S T,
  subtype S T.
Proof.
  intros.  eauto.
Admitted.

セクションを閉じた後では、ヒントsubtype_transはもうアクティブではなくなることに注意します。

End HintsTransitivity.

上の例では、証明探索は多くの時間を費して、推移性と反射性を可能なすべての方法で適用しようと試みています。この過程は以下のようにまとめられます。最初のゴールはsubtype S Tです。これに反射性は適用できないことから、eautoは推移性を呼びます。この結果2つのサブゴールsubtype S ?Xとsubtype ?X Tができます。最初のサブゴールsubtype S ?Xはすぐに解くことができます。反射性を適用すれば十分です。この結果?XはSと単一化されます。これから、第二のサブゴールsubtype ?X Tはsubtype S Tとなります。これは最初のゴールとまったく同一です...

推移性補題の問題は、この補題がサブタイプ関係を結論部とするどのようなゴールにも適用可能だということです。このことから、eautoは、ほとんどの場合ゴールを解決する助けにならないにもかかわらず、この補題を適用しようとし続けます。これから、証明探索のヒントに推移性を加えることはやめるべきです。

効率を無視せずに推移性補題を自動証明で使うための一般的回避策があります。この回避策は “external hint” という強力なメカニズムを使います。このメカニズムを使うと、特定の補題を証明探索中でどういう条件の場合に試してみるべきかを手で書くことができます。

サブタイプの推移性の場合、推移性補題をsubtype S Uという形のゴールに適用してみるのは、既に証明コンテキスト内に仮定としてsubtype S Tまたはsubtype T Uがあるときに限る、とCoqに伝えます。言い換えると、推移性補題を適用するのは、その適用が証明の助けになるという何らかの根拠があるときだけ、ということです。この “external hint” を設定するために、次のように記述します。

Hint Extern 1 (subtype ?S ?U) =>
  match goal with
  | H: subtype S ?T |- _ => apply (@subtype_trans S T U)
  | H: subtype ?T U |- _ => apply (@subtype_trans S T U)
  end.

このヒント宣言は次のように理解できます。

“Hint Extern” はヒントを導入します。
数 “1” は証明探索の優先度に対応します。実際にどの優先度が使われるかはそれほど問題ではありません。
パターンsubtype ?S ?Uはパターンが適用されるべきゴールの種類を記述します。クエスチョンマークは、ヒント記述の残りの部分で変数?Sと?Uが何らかの値に束縛されることを示します。
構文match goal with ... endによって、ゴールまたは証明コンテキストまたはその両方におけるパターンを認識しようとします。
最初のパターンはH: subtype S ?T |- _です。これは、コンテキストが型subtype S ?Tである仮定Hを持たなければならないことを示します。ただしSはゴールのものと同一でなければならず、?Tは任意の値で構いません。
H: subtype S ?T |- _の最後の記号|- _は、証明課題がどのような形でなければならないかについて、これ以上の条件をつけないことを示します。
それに続く枝=> apply (@subtype_trans S T U)は、ゴールがsubtype S Uという形で、subtype S Tという形の仮定があるとき、推移性補題を引数S、T、Uを具体化して適用してみるべきであることを示します。(なお、subtype_transの前の記号@が実際に必要なのは、暗黙の引数(“Implicit Arguments”)機能がアクティブであるときだけです。)
別の枝は、H: subtype ?T Uという形の仮定に対応しますが、上記と対称です。

注意: 任意の別の推移的関係について同じ external hint を再利用することができます。その場合、subtypeをその関係の名前に置き換えるだけです。

このヒントがどのようにはたらくか例を見てみましょう。

Lemma transitivity_workaround_1 : forall T1 T2 T3 T4,
  subtype T1 T2 -> subtype T2 T3 -> subtype T3 T4 -> subtype T1 T4.
Proof.
  intros.  eauto.
Qed.

新しい external hint が複雑さの爆発を起こさないことをチェックすることもできるでしょう。

Lemma transitivity_workaround_2 : forall S T,
  subtype S T.
Proof.
  intros.  eauto.
Admitted.

決定手続き¶

決定手続きは主張が特定の形である証明課題を解くことができます。この節では、3つの有用な決定手続きについて説明します。タクティックomegaは算術と不等式を含むゴールを扱うことができますが、一般の積算は扱えません。タクティックringは積算を含む算術が扱えますが、不等式は対象としません。タクティックcongruenceは証明コンテキストから得られる等式を使って、等式および不等式を証明することができます。

Omega¶

タクティックomegaは自然数(型nat)と整数(型Z、これはZArithモジュールをincludeすることで利用可)を対象とします。加算、減算、等式、不等式を対象とします。omegaを使う前にモジュールOmegaを import する必要があります。次の通りです。

Require Import Omega.

例を示します:xとyを2つの自然数(負にはならない)とする。yは4以下と仮定し、x+x+1はy以下と仮定し、そしてxはゼロではないと仮定する。すると、xは1でなければならない。

Lemma omega_demo_1 : forall (x y : nat),
  (y <= 4) -> (x + x + 1 <= y) -> (x <> 0) -> (x = 1).
Proof. intros. omega. Qed.

別の例: もしzがxとyの間で、xとyの差が高々4である場合、xとzの間は高々2である。

Lemma omega_demo_2 : forall (x y z : nat),
  (x + y = z + z) -> (x - y <= 4) -> (x - z <= 2).
Proof. intros. omega. Qed.

コンテキストの数学的事実が矛盾している場合、omegaを使ってFalseを証明することができます。次の例では、xとyの制約をすべて同時に満たすことはできません。

Lemma omega_demo_3 : forall (x y : nat),
  (x + 5 <= y) -> (y - x < 3) -> False.
Proof. intros. omega. Qed.

注意:omegaが矛盾によってゴールを証明できるのは、ゴールの結論部がFalseに簡約されるときだけです。Falseから(ex_falso_quodlibetによって)任意の命題Pが導出されますが、タクティックomegaは、ゴールの結論部が任意の命題Pであるときは常に失敗します。

Lemma omega_demo_4 : forall (x y : nat) (P : Prop),
  (x + 5 <= y) -> (y - x < 3) -> P.
Proof.
  intros.


  false. omega.
Qed.

Ring(環)¶

omegaと比較して、タクティックringは積算を対象としていますが、不等式についての推論は放棄しています。さらに、対象とするのは整数(型Z)だけで、自然数(型nat)は対象外です。以下はringの使い方の例です。

Module RingDemo.
  Require Import ZArith.
  Open Scope Z_scope.

Lemma ring_demo : forall (x y z : Z),
    x * (y + z) - z * 3 * x
  = x * y - 2 * x * z.
Proof. intros. ring. Qed.

End RingDemo.

Congruence(合同)¶

タクティックcongruenceは、証明コンテキストの等式を使って、ゴールに至るための書き換えを自動実行することができます。タクティックsubstが扱える等式は変数xと式eについてx = eという形のものだけですが、congruenceはsubstより若干強力です。

Lemma congruence_demo_1 :
   forall (f : nat->nat->nat) (g h : nat->nat) (x y z : nat),
   f (g x) (g y) = z ->
   2 = g x ->
   g y = h z ->
   f 2 (h z) = z.
Proof. intros. congruence. Qed.

さらにcongruenceは、例えばforall a, g a = h aのように全称限量された等式を扱えます。

Lemma congruence_demo_2 :
   forall (f : nat->nat->nat) (g h : nat->nat) (x y z : nat),
   (forall a, g a = h a) ->
   f (g x) (g y) = z ->
   g x = 2 ->
   f 2 (h y) = z.
Proof. congruence. Qed.

次はcongruenceがとても有効な例です。

Lemma congruence_demo_4 : forall (f g : nat->nat),
  (forall a, f a = g a) ->
  f (g (g 2)) = g (f (f 2)).
Proof. congruence. Qed.

タクティックcongruenceは、証明コンテキストで等しくない関係にある両辺についての等式をゴールが前提とするとき、矛盾を証明できます。

Lemma congruence_demo_3 :
   forall (f g h : nat->nat) (x : nat),
   (forall a, f a = h a) ->
   g x = f x ->
   g x <> h x ->
   False.
Proof. congruence. Qed.

congruenceの強みの1つはとても速いタクティックだということです。このため、役立つかもしれないときはいつでも、試すことをためらう必要はありません。