coq
Tactiek gebruiken

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


Invoering

Deze sectie bevat informatie over het gebruik van verschillende Coq-tactieken en -technieken (case-analyse, bewijs door inductie, auto, enz.) Om stellingen te bewijzen.

Triviaal voorbeeld van een case-analyse

In Coq komt destruct min of meer overeen met een case-analyse. Het is vergelijkbaar met inductie, behalve dat er geen inductiehypothese is. Hier is een (weliswaar nogal triviaal) voorbeeld van deze tactiek: 

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
Licentie onder CC BY-SA 3.0
Niet aangesloten bij Stack Overflow