應用適用的戰術房地而不是目標

Question

如果目標狀態是這樣的：

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

然後，我可以將其轉換爲使用apply H2戰術以下狀態：

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

現在，我想要做同樣的事情，但假設：

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.