coq
Korzystanie z taktyki

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


Wprowadzenie

Ta sekcja zawiera informacje o tym, jak używać różnych taktyk i technik Coqa (analiza przypadku, dowód przez indukcję, auto itp.) W celu udowodnienia twierdzeń.

Trywialny przykład analizy przypadku

W Coq, destruct mniej więcej odpowiada analizie przypadku. Jest podobny do indukcji, z tą różnicą, że nie istnieje hipoteza indukcji. Oto (co prawda dość trywialny) przykład tej taktyki: 

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
Licencjonowany na podstawie CC BY-SA 3.0
Nie związany z Stack Overflow