소재지는 다음과 같이있을 때 나는 다양한 시나리오에서 <code>apply</code> 전술을 시도하고있다 그것은 다음과 같은 경우에 갇혀 것 같다 변수

Question

에 대한 인스턴스를 찾을 수없는 전술을 적용

H1 : a 
    H2 : a -> forall e : nat, b -> g e 
    ============================ 
    ... 

내가 apply H2 in H1.을 시도, 그것은 나 건물의 한 부분으로 forall e : nat, b -> g e을 가지고 할

Error: Unable to find an instance for the variable e. 

어떤 방법 : 나에게 오류를 제공합니다.

Lemma test : forall {a b c : Prop} {g : nat} (f : nat -> Prop), 
    a /\ (a -> forall {e : nat}, b -> f e) -> c. 
Proof. 
    intros a b c f g. 
    intros [H1 H2]. 
    (* apply H2 in H1. *) 
Abort. 

Answer 1

COQ 참조 설명서, §8.2.5 : 이것은 위의 시나리오와 전체 작업 코드 귀하의 경우에 위의 설명을 적용, 지금

The tactic applyterminident tries to match the conclusion of the type of ident against a non-dependent premise of the type of term, trying them from right to left. If it succeeds, the statement of hypothesis ident is replaced by the conclusion of the type of term.

, 우리는 다음을 얻을 COQ는에 시도 H1 : a을 H2의 결과와 바꾸십시오 (즉, g e). 이를 위해서는 보편적으로 정량화 된 변수 e을 일부 값으로 인스턴스화해야합니다.이 값은 분명히 추측 할 수 없으므로 사용자가 본 오류 메시지입니다.

... 
    H2 : a -> forall e : nat, b -> g e 
    H1 : g ?e 
    ============================ 
    c 

및

... 
    H1 : a 
    H2 : a -> forall e : nat, b -> g e 
    ============================ 
    b 

H1 가설 :

eapply H2 in H1. 

당신에게 두 개의 하위 목표를 줄 것이다 :

것을 볼 수있는 또 다른 방법은 apply ... in ...의 다른 변형을 시도하는 것입니다 첫 번째 부 목적의 Coq가 일반 012로 무엇을하려고했는지를 보여줍니다.전술이지만, eapply in 경우 변수 e은 실존 적 변수 (?e)로 대체되었습니다. 실존 적 변수에 익숙하지 않다면, 그들은 나중에 Coq에 조건을 짓겠다고 약속하는 것입니다. 당신은 통일을 통해 암묵적으로 용어를 구축해야합니다.

어쨌든, specialize (H2 H1).은 당신이 원하는, 또는 @AntonTrunov처럼이

pose proof (H2 H1) as H; clear H1; rename H into H1.