Taktik anwenden kann keine Instanz für eine Variable

Question

Ich habe versucht, aus apply Taktik in verschiedenen Szenarien, und es scheint zu stecken im folgenden Fall finden, wenn Räumlichkeiten wie diese sind:

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

Wenn ich apply H2 in H1. versuchen, es gibt mir den Fehler:

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

eine Möglichkeit für mich forall e : nat, b -> g e als Teil der Räume zu bringen. Dies ist der volle Arbeits Code mit dem obigen Szenario:

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

Das Handbuch Coq Reference, §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.

nun die obige Beschreibung auf Ihren Fall anwenden, wir folgende erhalten, Coq versucht, ersetzen Sie H1 : a durch die Schlussfolgerung von H2, dh g e. Dazu muss es die universell quantifizierte Variable e mit einem gewissen Wert instanziieren, die Coq nicht offensichtlich herleiten kann - daher die Fehlermeldung, die Sie gesehen haben.

Ein anderer Weg, das zu sehen ist eine andere Variante von apply ... in ... versuchen:

eapply H2 in H1. 

welche geben Ihnen zwei Teilziele:

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

und

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

Die H1 Hypothese des ersten Teilziels zeigt, was Coq mit dem gewöhnlichen 012 anstrebteTaktik, aber im eapply in Fall wurde die Variable e durch eine existentielle Variable ersetzt (?e). Wenn Sie mit existentiellen Variablen noch nicht vertraut sind, dann sind sie eine Art Versprechen, die Sie an Coq richten, dass Sie später Begriffe für sie erstellen werden. Du solltest die Begriffe implizit durch Vereinheitlichung aufbauen.

Sowieso specialize (H2 H1). sein könnte, was Sie tun wollen, oder so etwas wie dieses

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