Coq "ローカルアプリケーションの使用"の正しい使い方は何ですか？

Question

私はだから私は、次のように、それぞれに2つのささいな戦術を適用しようとして2つのゴールで少しテストをした

Local application of tactics

Different tactics can be applied to the different goals using the following form:

[ > expr1 | ::: | exprn ]

The expressions expri are evaluated to vi, for i = 0; ...; n and all have to be tactics. The vi is applied to the i-th goal, for = 1; ...; n. It fails if the number of focused goals is not exactly n.

についてCoqのリファレンスマニュアル（8.5p1）を読んでいる：

Goal forall P Q: Prop, P \/ Q -> Q \/ P. 
intros. destruct H. [ > idtac | idtac ]. 

しかし、私は1つの戦術しか期待できないと私に言ったエラーがあります：

Error: Incorrect number of goals (expected 1 tactic).

私は混乱しています。私が間違ったことを説明できる人がいますか？正しい使い方は何ですか？

Answer 1

ここで重要な部分は、あなたが2つの焦点目標を必要とする

It fails if the number of focused goals is not exactly n.

です。焦点目標の 数は次のように確認することができます：

（1）シーケンシングの使用：：destruct H; [> idtac | idtac].

を（

Ltac print_numgoals := let n := numgoals in idtac "# of goals:" n. 

Goal forall P Q: Prop, P \/ Q -> Q \/ P. 
    intros. destruct H. 
    print_numgoals. (* prints 1 *) 

いくつかの集中の目標を取得するいくつかの方法があります2）または少し短く：destruct H; [> idtac ..].

（3）allセレクタを使用して（手動、§8.1を参照）：この最後の場合において

destruct H. all: [ > id_tac | id_tac ]. 

、destruct H. all: print_numgoals.プリント2を。

結論としては、以下が言及されるべきである - それが標準ライブラリ（および他のいくつかのライブラリ）で使用されることはありませんので、その正確な形式（[ > ...]）における戦術のローカルアプリケーションは、非常に有用ではないようですこの機能に特化したセクションを除いて、このマニュアルには何の言及もありません。フォームのバージョンexpr; [ expr_1 | ... | expr_n]が最も有用であるようです。