appliquer la tactique ne peut pas trouver une instance pour une variable

Question

J'ai essayé à apply tactique dans divers scénarios et il semble coincé dans le cas suivant lorsque les locaux sont comme ceci:

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

Lorsque je tente apply H2 in H1., il me donne l'erreur:

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

de toute façon pour moi d'apporter forall e : nat, b -> g e dans le cadre des locaux. Ceci est le code de travail complet avec le scénario ci-dessus:

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

Le Coq Manuel de référence, §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.

Maintenant, l'application de la description ci-dessus à votre cas, nous obtenons ce qui suit, Coq essaie de remplacer H1 : a avec la conclusion de H2, soit g e. Pour ce faire, il doit instancier la variable universellement quantifiée e avec une certaine valeur, que Coq ne peut évidemment pas déduire - d'où le message d'erreur que vous avez vu.

Une autre façon de voir est d'essayer une autre variante de apply ... in ...:

eapply H2 in H1. 

qui vous donnera deux objectifs secondaires:

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

et

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

L'hypothèse H1 du premier sous-ensemble montre ce que Coq allait avec le 012 ordinairetactique, mais dans le cas eapply in la variable e a été remplacée par une variable existentielle (?e). Si vous n'êtes pas encore familier avec les variables existentielles, alors vous êtes en quelque sorte promis à Coq que vous allez les construire plus tard. Vous êtes censé construire les termes implicitement, via l'unification.

Quoi qu'il en soit, specialize (H2 H1). peut-être ce que vous voulez faire, ou quelque chose comme ça

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