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.