부울 값에 대한 증명, 거짓 = 참

Question

현재 "소프트웨어 기초"의 5 장에 있지만 몇 가지를 명확히하기 위해 1 장으로 돌아갈 필요가 있음을 느꼈습니다. 특히 내가 소화하지 않은 운동이 있습니다. 우리는 불리언에 대한 결과를 증명하기 위해 두 번 파괴를 사용하라는 요청을 받았습니다. 여기에는 이름과 기타 세부 사항이 변경되었습니다.

H : fb true true = false 
______________________________________(1/1) 
true = false 

두 번째 가설이 거짓 틱 :

Inductive bool: Type := 
|true: bool 
|false: bool. 

Definition fb (b1:bool) (b2:bool) : bool := 
match b1, b2 with 
| false, false => false 
| _, _ => true 
end. 

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
intros [] [] H. 
- rewrite <- H. reflexivity. 
- reflexivity. 
- rewrite <- H. reflexivity. 
- reflexivity. 
Qed. 

언제 처음 틱, 상황과 목표에 모두 넌센스입니다. 세 번째 틱은 첫 번째 틱과 같은 종류입니다. 네 번째 진드기 만이 합리적입니다 :

H : fb false false = false 
______________________________________(1/1) 
false = false 

나는이 모든 것이 효과가 있다는 것을 알고 있습니다. 그러나 나는 우리가 허위의 광야에 대한 진리의 좁은 길을 그만두고 있다는 인상을 가지고있다. 보다 정확하게, AFAIK, 진실 또는 거짓이라는 어떤 진술을 증명하기위한 거짓 가설을 세울 수 있습니다. 여기서 우리는 false = true, OK not를 증명하기 위해 그것을 사용합니다. 그러나 여전히 저를 다소 불편하게 만듭니다. 나는 증거 보조자가 이것을 허용 할 것으로 기대하지 않았을 것이다. 모순에 의한 전형적인 증거에 조금

정성 들여

는

, 나는 무작위로 가설을 선택, 내가 동어 반복이나 모순 중 하나를 찾을 때까지 목표를 도출한다. 나는 가설이 사실인지 거짓인지를 결론 지었다.

true = false 

:

H : fb true true = false 

가 모순되는 목표에 적용 : 경우에, 여기에 1 (경우 3 동일) 어떻게됩니까

는 COQ은 거짓 가설에서 시작

과 결합하여 동어체를 찾습니다.

그건 내가 알고있는 추론의 방법이 아닙니다. 0 = 1로 시작하는 학생의 농담을 회상합니다. 자연수에 대한 불합리한 결과가 입증 될 수 있습니다.

후속 조사

그래서 난 그냥 위의 쓴 것에 대해 생각하고 오늘 아침 내 통근하는 동안. 이제 저는 사례 1과 3이 모순에 의한 적절한 증거라고 믿습니다. 실제로 H는 거짓이며 우리는 거짓이라는 목표를 증명하기 위해 그것을 사용합니다. 가설 (a와 b의 값)은 거부되어야한다. 저를 혼란스럽게 할 수있는 것은 우리가 목표에서부터 시작하여 "뒤로"라는 방식으로 일하는 것입니다. 기본적으로 false -> true은 "폭발의 원리"에서 동어 반복

H : fb true false = false 
______________________________________(1/1) 
false = false 

인 :

나는 읽는 경우 2 미정 조금입니다. 나는 이것이 증명에 직접 사용될 수 있다고 생각하지 않을 것입니다.

오, 잘 모르겠다. 나는 두려운 점이 무엇인지 완전히 이해하고 있지만, Coq에 대한 신뢰는 훼손되지 않았다. 계속해서 5 장으로 돌아 가야합니다. 의견에 감사드립니다.

Answer 1

우선, 자체 포함 된 코드를 제공해 주셔서 감사합니다.

나는 정말로해야 할 일이 가설에서 모순을 유도하는 것이라는 것을 알고있을 때 rewrite을 사용하여 목표를 증명하는 불안을 이해합니다. 그렇다고해서 추론이 정확하지는 않습니다. 그러한 가정하에이 목표를 증명할 수 있다는 것이 사실입니다.

그러나 저는 이것이 증명 스크립트를 정말로 읽을 수 없게한다고 생각합니다. 귀하의 예에서는 가능한 모든 경우를 고려하고 있으며이 네 가지 중에서 세 가지가 불가능합니다. 우리가 당신의 증거를 읽을 때 우리는 그것을 볼 수 없습니다. 당신이 불가능한 경우에 있음을 분명히하기 위해, "보라,이 사건을 배제하기 위해 모순을 증명할 것입니다"라고 말하는 것이 유용한 몇 가지 전술이 있습니다.

그들 중 하나는 exfalso입니다. 현재 목표를 False으로 바꿀 것입니다 (주석에서 @ejgallego가 말한대로 False에서 파생 될 수 있기 때문에).

두 번째 것은 "이제 진술과 그 부정을 증명하려고합니다."(이것은 기본적으로 False를 증명하는 것과 같습니다)라고 말하면서 absurd입니다.

세 번째로 충분하면 귀하의 경우는 discriminate입니다. 가설에서 모순 된 평등을 발견하려고 시도합니다 (예 : true = false).

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
    intros [] [] H. 
    - discriminate. 
    - discriminate. 
    - discriminate. 
    - reflexivity. 
Qed. 

---

지금, 바로 그래서 당신은 discriminate 및 reflexivity 모두 easy 전술에 의해 시도됩니다, 알고있다. 따라서 다음과 같은 증거는 잘 작동합니다 (하지만 무슨 일이 일어나고 있는지 표시되지 않습니다 때문에이 질문의 범위를 벗어나게) :

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
    intros [] [] H; easy. 
Qed. 

이 같은 증거에 대한 문법 설탕입니다 :

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
    now intros [] [] H. 
Qed.