Coq에서 중첩 된 실존 문장을 인스턴스화하는 가장 좋은 방법

Question

중첩 된 실존 진술 문이 문맥에 H : exists (a : A) (b : B) (c : C) ... (z : Z), P a b c ... z 있다고 가정합니다. H을 인스턴스화하고 새로운 가설 H' : P a b c ... z을 얻는 가장 좋은 방법은 무엇입니까? 이렇게 반복하면 inversion이 걸리며 원치 않는 중간 단계는 모두 H0 : exists (b : B) (c : C) ... (z : Z), P a b c ... z과 같습니다.

내 previous question은 매우 유사합니다. 어쩌면 pose proof 또는 generalize을 사용하여이 방법을 사용할 수도 있습니다.

Answer 1

원하는 작업을 "인스턴스화"라고하지 마십시오. 보편적으로 정량화 된 가설을 인스턴스화 할 수 있으며, 존재 론적으로 정량화 된 결론을 인스턴스화 할 수 있지만 그 반대는 아닙니다. 나는 적절한 이름이 "소개"라고 생각하고 있습니다. 가설에서 실존 적 정량화를 도입 할 수 있으며 결론에 보편적 인 정량화를 도입 할 수 있습니다. 대신에 "제거"하는 것처럼 보이면, 그것은 뭔가를 증명할 때 연속적인 미적분 유도의 맨 아래에서 시작하여 맨 위로 거꾸로 작업하기 때문입니다.

어쨌든 전술 번호 firstorder을 사용하십시오. 또한 목표를 단순화하려는 경우에는 Set Firstorder Depth 0 명령을 사용하여 시험용 검색 기능을 해제하십시오.

목표에 더 높은 순위 요소가있는 경우 오류 메시지가 표시 될 수 있습니다. 이 경우 simplify과 같은 것을 사용할 수 있습니다.

Ltac simplify := repeat 
    match goal with 
    | h1 : False |- _ => destruct h1 
    | |- True => constructor 
    | h1 : True |- _ => clear h1 
    | |- ~ _ => intro 
    | h1 : ~ ?p1, h2 : ?p1 |- _ => destruct (h1 h2) 
    | h1 : _ \/ _ |- _ => destruct h1 
    | |- _ /\ _ => constructor 
    | h1 : _ /\ _ |- _ => destruct h1 
    | h1 : exists _, _ |- _ => destruct h1 
    | |- forall _, _ => intro 
    | _ : ?x1 = ?x2 |- _ => subst x2 || subst x1 
    end.