目標状態はこのようであれば、目標

Question

するのではなく、構内へ戦術を適用する適用：私は、今

a : Prop 
    b : Prop 
    H1 : a 
    H2 : b -> c 
    ============================ 
    b 

：

a : Prop 
    b : Prop 
    H1 : a 
    H2 : b -> c 
    ============================ 
    c 

その後、私はapply H2戦術を使用して、次の状態に変換することができます仮説についても同じことをしたいが：

a : Prop 
    b : Prop 
    H1 : a 
    H2 : b -> a 
    ============================ 
    b 

私は新しい仮説を導入したい（またはexi私は新しいH3 : bを構内に持っています。それは可能ですか？

applyのさまざまなバリエーションを試しましたが、何らかのエラーが発生しています。上記の状態に起動するためのコード：

Lemma test : forall {a b : Prop}, 
    a /\ (b -> a) -> b. 
Proof. 
    intros a b. 
    intros [H1 H2]. 
Abort. 

Answer 1

あなたtest補題が成立しないので、これは、不可能です。たとえば、aをTrueとし、bをFalseとする。両方の構内（aおよびb -> a）が保持されますが、bは保持されません。

Lemma test : forall a b : Prop, a /\ (a -> b) -> b. 
Proof. intros [H1 H2]. apply H2 in H1. exact H1. Qed. 

：あなたは少しあなたの結果のステートメントを変更した場合

これは、しかし、働くだろう