coq
Использование тактики
Поиск…
Вступление
В этом разделе содержится информация о том, как использовать различные методы и методы Coq (анализ случаев, доказательство по индукции, авто и т. Д.) Для доказательства теорем.
Тривиальный пример анализа случая
В Coq destruct более или менее соответствует анализу случая. Это похоже на индукцию, за исключением того, что нет индукционной гипотезы. Вот пример (по общему признанию, довольно тривиальный) этой тактики:
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
Лицензировано согласно CC BY-SA 3.0
Не связан с Stack Overflow