Coq "local application of tactics"의 올바른 사용법은 무엇입니까? 다음과 같이

Question

나는, 그래서이 두 가지 목표는 각각 두 개의 사소한 전술을 적용하는 노력과 약간의 테스트를했다

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 ]. 

그러나 단 하나의 전술이 예상된다는 오류가 나타납니다.

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

나는 혼란 스럽습니다. 어떤 사람이 내가 잘못한 것을 설명 할 수 있습니까? 올바른 사용법은 무엇입니까?

Answer 1

중요한 부분은 여기에 당신은이 목표를 집중해야 할

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

입니다. 초점을 목표 수는 다음과 같이 확인할 수 있습니다 :

여러 초점을 맞춘 목표를 가져 오는 여러 가지 방법이 있습니다

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 *) 

:

(1) 사용 순서 : destruct H; [> idtac | idtac].

은 (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] 인 버전이 가장 유용합니다.