어떻게하면 Coq 가설 'd = d + 1'에서 '거짓'과 확장으로 무엇을 증명할 수 있습니까?

Question

Goal forall (d : nat), d + 1 = d -> False. 
Proof. 
    intros d H. 
Abort.  

False을 H에서 어떻게 증명할 수 있습니까? inversion H이 복제 중입니다.

Answer 1

당신이 당신의 컨텍스트에서 모순을 도출 할 몇 가지 유용한 보조 정리를 발견 할 수있는 방법이다. 우선 우리가 그렇지 않으면 Search 명령은 그 보조 정리를 발견 할 수 없습니다,이를 포함하는 모듈을 가져와야 :

Require Import Coq.Arith.Arith. 

우리는 우리가 필요로 정확히 보조 정리가있는 경우의 확인하자 (리콜은 x <> y는 표기법이다

Search (?x + _ <> ?x). 

운이 시간 : A -> False에 대한 not (eq x y) 및 not A 스탠드)합니다. 좋습니다, 덧셈은 교환 적입니다. 이렇게하면 되겠습니다.

Search (_ + ?x <> ?x). 

다시는 아무것도 아닙니다. 그러나 우리는 확실히 그런 일이 있어야합니다

마지막으로

Search (S ?x <> ?x). 

우리가 다음 보조 정리 :

Nat.neq_succ_diag_l: forall n : nat, S n <> n 

우리가 같이 사용할 수 있습니다

Require Import Coq.Arith.Arith. 

Goal forall (d : nat), d + 1 = d -> False. 
Proof. 
    intros d H. 
    rewrite Nat.add_comm in H. 
    now apply Nat.neq_succ_diag_l in H. 
Qed. 

Answer 2

증명은 d 유도에 의해 다음과 사용

eq_add_S 
    : forall n m : nat, S n = S m -> n = m 

베이스 케이스 반전하여 False 리드 0 = 1이며,이 경우에 체결. 귀납적 인 경우는 유도 가설로 d + 1 = d -> False이고 목표로는 S d + 1 = S d -> False입니다. 우리는 x + 1 = y + 1 -> x + y이 eq_add_S임을 알고 있습니다. 그래서 우리는 우리의 목표를 다시 쓰고 유도 가설을 적용합니다.

완전한 증거 : 여기

Goal forall (d : nat), d + 1 = d -> False. 
Proof. 
    induction d. 
    intros. 
    - inversion H. 
    - intros H. 
    erewrite <- eq_add_S in H; eauto. 
Qed.