案例分析的简单例子

在 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.