수색…
소개
이 섹션에서는 다양한 Coq 전술 및 기법 (케이스 분석, 유도에 의한 증명, 자동 등)을 사용하여 정리를 증명하는 방법에 대한 정보를 제공합니다.
사례 분석의 간단한 예
Coq에서 더 많거나 적게 destruct 시키는 것은 사례 분석에 해당합니다. 유도 가설이 없다는 것을 제외하고는 유도와 유사합니다. 다음은이 전략에 대한 (아주 드문 경우) 예제입니다.
Require Import Coq.Arith.Lt.
Theorem atLeastZero : forall a,
0 <= a.
Proof.
intros.
destruct a. (* Case analysis *)
- reflexivity. (* 0 >= 0 *)
- apply le_0_n. (* S a is always greater than zero *)
Qed.
Modified text is an extract of the original Stack Overflow Documentation
아래 라이선스 CC BY-SA 3.0
와 제휴하지 않음 Stack Overflow