案例分析的簡單例子
在 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.