적용

Question

목표 상태는 다음과 같은 경우 : 지금

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

I을 :

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. 

: 조금 당신의 결과의 성명을 변경 한 경우

그러나 이것은 작동합니다