Coq: Wie man eine Hypothese auf eine andere anwenden

Question

Angenommen, ich habe zwei Hypothesen im Kontext, a_b : A -> B und a : A. Ich sollte a_b auf a anwenden können, um eine weitere Hypothese zu erhalten, b : B.

Das heißt, daß der folgende Zustand gegeben:

1 subgoal 
A : Prop 
B : Prop 
C : Prop 
a_b : A -> B 
a : A 
______________________________________(1/1) 
C 

Es sollte eine gewisse Taktik sein, foo (a_b a), dies in den folgenden Zustand zu transformieren:

1 subgoal 
A : Prop 
B : Prop 
C : Prop 
a_b : A -> B 
a : A 
b : B 
______________________________________(1/1) 
C 

Aber ich weiß nicht, was foo ist.

Eine Sache, die ich tun kann, ist dies:

assert B as b. 
apply a_b. 
exact a. 

aber das ist eher langatmig und skaliert schlecht, wenn statt a_b a ich etwas größeren Ausdruck haben.

Eine andere Sache, die ich tun kann, ist:

specialize (a_b a). 

aber ersetzt die a_b Hypothese, die ich will nicht zu tun.

Answer 1

pose proof (a_b a) as B. 

sollte tun, was Sie wollen.