Coq true = false 차별 실패, 원시 동등하지 않음

Question

다음을 증명하기 위해 노력하고 있으며 b 및 모든 단일 인수 부울 함수에 대한 모든 사례를 열거하여 해결할 수있는 올바른 접근 방법이 있다고 생각합니다. f 4 개의 함수가 2 개의 부울 값보다 많음) 모든 것을 철저히 파괴함으로써 그 점을 증명합니다. 그러나

Theorem example : 
    forall (f : bool -> bool) (b : bool), 
    f (f b) = b. 
Proof. 
    intros. 
    destruct (f (f b)). 
    - destruct b. 
    + reflexivity. 
    + Fail discriminate. admit. 
    - destruct b eqn:Hqebb. 
    + Fail discriminate. admit. 
    + reflexivity. 
Qed. 

, 나는 다음과 같은 오류 얻을 false = true에, 2 층과 3 단계 차별하려고하면 내가 유도 유형 전에 차별을 사용했습니다

Ltac call to "discriminate" failed. 
No primitive equality found. 

을하고 일을 예상대로 , 그래서 나는 그것이 불리언 타입으로 여기에서 작동하지 않는다는 것에 놀랐다. 어떤 아이디어?

Answer 1

discriminate 전술은 다른 생성자로 시작하는 귀납적 유형 용어와 동일한 가설이있는 경우에만 작동합니다. 당신이 discriminate에 첫 번째 통화를 수행 할 때, 상황은 다음과 같습니다 : 당신이 볼 수 있듯이

f : bool -> bool 
============================ 
true = false 

는 상황이 너무 discriminate 아무것도 할 수없는, 어떤 평등 가설이 포함되어 있지 않습니다. 이를 해결하려면 destruct 전술에 eqn: 옵션을 사용해야하므로 Coq가 모든 관련 사실을 컨텍스트에 기록합니다. 예를 들어, 당신이 평소와 같이 두 개의 하위 목표를 생성 할뿐만 아니라 다음,

destruct b eqn:H. 

및 b 유형 bool입니다 호출하는 경우, COQ는 가설 H : b = true 및 H : b = false을 추가합니다.

(난 당신이 질문을 변경하는 것이 고맙지 만 난 그냥 지금 거기에 넣어 정리가 증명되지 않습니다 점에 유의하고 싶었다. 원래의 질문에이 적응도 어렵지 않을 것이다.)

Answer 2

true = false 가설 (가설)이있는 경우 discriminate을 사용하여 목표를 완료 할 수 있습니다. 당신이 붙어있는 목표에서, 당신은 을 묻습니다.true = false. 어떤 전술도 그렇게 할 수 없다. 불가능한 일이다!

당신이 사용하는 특정 예를 정리 실제로 false입니다

Theorem not_example: 
    ~ forall (f : bool -> bool) (b : bool), f (f b) = b. 
Proof. 
    intros H. 
    specialize (H (fun _ => true) false). 
    simpl in H. 
    discriminate. 
Qed. 

그러나 일반적으로, 아서이가 할 수있는 방법은는 식 사용하는 것입니다 말했듯이 : 관련 방정식을 기억하고, destruct에 옵션을 . 예 :

Theorem example : 
    forall (f : bool -> bool) (b : bool), 
    f (f b) = b. 
Proof. 
    intros. 
    destruct (f true) eqn:?; destruct (f false) eqn:?; destruct b; try congruence.