coq
Taktiken verwenden

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


Einführung

In diesem Abschnitt finden Sie Informationen zur Verwendung verschiedener Coq-Taktiken und -Techniken (Fallanalyse, Induktionsnachweis, Auto usw.), um Theoreme zu beweisen.

Triviales Beispiel für eine Fallanalyse

In Coq entspricht destruct mehr oder weniger einer Fallanalyse. Es ist der Induktion ähnlich, außer dass es keine Induktionshypothese gibt. Hier ist ein (zugegebenermaßen eher triviales) Beispiel dieser Taktik: 

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
Lizenziert unter CC BY-SA 3.0
Nicht angeschlossen an Stack Overflow