Kombinieren von zwei Coq-Hypothesen

Question

So habe ich zwei Hypothesen, eine, die h : A -> B ist, und die andere, die h2 : A ist. Wie kann ich h3 : B in meinen Hypothesen erscheinen lassen?

Answer 1

pose proof (h h2) as h3. 

einleitet h3 : B als eine neue Hypothese,

specialize (h h2). 

modifiziert h : A -> B in h : B - dies kann nützlich sein, wenn Sie nicht h später benötigen, und symmetrisch,

apply h in h2. 

konvertiert h2 : A in h2 : B.

wäre eine andere (nicht sehr bequem) Art und Weise

assert B as h3 by exact (h h2). 

sein, das ist es, was die pose proof Variante entspricht.

Auch in einem einfachen Fall wie die folgenden, können Sie Ihr Ziel ohne die Einführung einer neuen Hypothese lösen können:

Goal forall (A B : Prop), (A -> B) -> A -> B. 
    intros A B h h2. 
    apply (h h2). 
Qed.