coq => Usando Tactics

Introducción

Esta sección incluye información sobre cómo usar varias tácticas y técnicas de Coq (análisis de casos, prueba por inducción, auto, etc.) para probar teoremas.

Ejemplo trivial de un análisis de caso.

En Coq, destruct más o menos corresponde a un análisis de caso. Es similar a la inducción, excepto que no hay hipótesis de inducción. Aquí hay un ejemplo de esta táctica (aunque bastante trivial):

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

Licenciado bajo CC BY-SA 3.0

No afiliado a Stack Overflow

coq
Usando Tactics

Buscar..

Introducción

Ejemplo trivial de un análisis de caso.