サーチ…
前書き
このセクションでは、様々な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