coq => Utiliser la tactique

Introduction

Cette section comprend des informations sur l'utilisation de diverses tactiques et techniques Coq (analyse de cas, preuve par induction, auto, etc.) pour prouver des théorèmes.

Exemple trivial d'une analyse de cas

En Coq, la destruct plus ou moins correspond à une analyse de cas. Il est similaire à l'induction sauf qu'il n'y a pas d'hypothèse d'induction. Voici un exemple (certes plutôt trivial) de cette tactique:

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

Sous licence CC BY-SA 3.0

Non affilié à Stack Overflow

coq
Utiliser la tactique

Recherche…

Introduction

Exemple trivial d'une analyse de cas