Application applique tactique aux locaux au lieu de l'objectif

Question

Si l'état de but est comme ceci:

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

Ensuite, je peux le convertir en l'état suivant à l'aide apply H2 tactique:

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

Maintenant, je vouloir faire la même chose, mais pour l'hypothèse:

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

Je veux introduire une nouvelle hypothèse (ou simplifier l'exi hypothèse de sting) de telle sorte que j'ai un nouveau H3 : b dans les locaux. Est-ce possible ?

J'ai essayé différentes variantes de apply mais tout est source d'erreur. Code pour mettre à l'état ci-dessus:

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

Answer 1

Ceci est impossible, parce que votre lemme test ne tient pas. Par exemple, prenez a pour être True et b pour être False. Les deux locaux (a et b -> a) sont maintenus, mais b ne tient pas.

Cela fonctionnerait, cependant, si vous avez modifié l'état de votre résultat un peu:

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