coq
Usando le tattiche

C++ F# Git Haskell Language JavaScript latex GNU/Linux Python Language Regular Expressions vim
Ricerca…


introduzione

Questa sezione include informazioni su come utilizzare varie tattiche e tecniche di Coq (analisi dei casi, prove per induzione, auto, ecc.) Per dimostrare i teoremi.

Esempio banale di un'analisi del caso

In Coq, destruct corrisponde più o meno all'analisi di un caso. È simile all'induzione, tranne che non esiste un'ipotesi di induzione. Ecco un esempio (certamente piuttosto banale) di questa tattica: 

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
Autorizzato sotto CC BY-SA 3.0
Non affiliato con Stack Overflow