쌍

Question

내가 형 TR 두 쌍의에서 다음 정리를 증명하려는

의 평등을 확인하는 방법 : 지금은

Definition s:= nat. 

Definition d:= nat. 

Definition c:= nat. 

Definition p:= nat. 

Inductive rt: Set := 

    |al : rt 
    |bl : rt. 

Definition TR: Set := 
    rt* s*d* c* p. 

Implicit Types m n : TR. 

Theorem eq_TR_dec : forall n m, {n = m} + {n <> m}. 

을,이 정리의 증명은 인트로의 n으로 시작한다. n을 파괴하라. m을 파괴하라. 그러나 나는이 정리를 증명하는 가장 좋은 전술을 이해할 수 없다. 어떻게하면이 정리를 증명할 수 있을까요? 감사합니다

Answer 1

의견에 언급 된대로 decide equality을 사용하면 이러한 목표를 기본적으로 해결할 수 있습니다. 자세한 내용은 here 문서를 확인하십시오.

이 경우

, 다만 필요에 따라 그것을 몇 번을 적용하고 그것을 작동 :

Theorem eq_TR_dec : forall n m, {n = m} + {n <> m}. 
Proof. 
    decide equality. 
    - decide equality. 
    - decide equality. 
    * decide equality. 
    * decide equality. 
     + decide equality. 
     + { 
     decide equality. 
     - decide equality. 
     - decide equality. 
     } 
Qed. 

하거나 사용하여 더 많은을 repeat tactic (또한 eponier의 의견에 했나요로), 기본적으로 subgoal에 reccursively (적용되는 생성)가 실패 할 때까지 당신이 그것을주는 전술 : 우리가 여기 만 decide equality 충분한 시간을 적용 해결해야 할 첫 번째 경우에서 보았 듯이

Theorem eq_TR_dec : forall n m, {n = m} + {n <> m}. 
Proof. 
    repeat decide equality. 
Qed. 

, 그래서 repeat 특히 효율적입니다!