Пытаясь понять ответ @keep_learning, я пошагово прошел этот код: Inductive nostutter {X:Type} :...
Глубоко погружаясь в test_nostutter_1 упражнения, я нашел способ решить это без повторов: Example...
Когда сопоставление с образцом (с match goal with) в определенной пользователем тактике, мы можем...
Авторы книги предоставили доказательства некоторых модульных тестов для упражнений на ностальтеру....
Lemma re_not_empty_correct : forall T (re : @reg_exp T), (exists s, s =~ re) <-> re_not_empty...
У меня есть простая лемма для списков, которая гласит: n::l = [n]++l, доказательство которого...
Как можно создать правильный конечный автомат (без способа построить его недопустимым образом) в...
Мне нужно доказать: 256 * (x / 256) <= 256 * x / 256 или, в более общем смысле, forall a b c : N...
В этой ссылке документа есть полезные теоремы о делении.Я попытался импортировать его, используя...
У меня есть следующая функция Haskell, которая выводит все возможные способы разделения списка:...
Я получаю следующую ошибку, когда звоню setoid_rewrite (kron_1_r U) по цели U == U ⊗ I 1 (где ==...
Require Import PeanoNat. Check PeanoNat.Nat.add_assoc. Вывод: Nat.add_assoc : forall n m p : nat, n...
Я вижу другой синтаксис Coq для определения лемм.Например, Lemma plus_n_O: forall n:nat, n = n + 0....
Я успешно установил coq 8.9.1 и coq-quickchick 1.1.0 с opam 2.0.4 , и я программирую на emacs 26.1
У меня проблема с платформой тестирования QuickChick.Предположим, у меня есть такой тип: Inductive...
Давайте определим два вспомогательных типа: Inductive AB : Set := A | B. Inductive XY : Set := X |...
Играя с теоремой leb_complete из IndProp, я обнаружил следующую странность: Theorem leb_complete :...
Я не могу сказать, в каких ситуациях мне следует использовать Theorem вместо Lemma или наоборот....
У меня есть тип записи с большим количеством полей: Record r : Set := R { field1 : nat; field2 :...
Я столкнулся с проблемой, для решения которой требовалась взаимная рекурсия.Я не мог сделать это в...
Я хочу установить VST 2.3 с coq 8.8.1, чтобы узнать объем VC на основе программного обеспечения. но...
Стандартная библиотека Coq имеет два подмножества модулей классов, один из которых привязан к Coq
data _∈_ {X : Set} (x : X) : (xs : List X) → Set where here! : {xs : List X} → x ∈ x ∷ xs there :...
Существует ли отношение равенства или неравенства между Type и Set в Coq? Я изучаю систему типов...
Для этого типа: Record Version := mkVersion { major : nat; minor : nat; branch : {b:nat| b > 0...