Fixpoint nonzeros (l:natlist) : natlist := match l with | nil => nil | 0 :: t => 1::nonzeros t...
Inductive color: Type := | red | green | blue. Inductive listw : Type := | nil : listw | cons : web...
Давайте определим тип, представляющий наборы: Inductive mySet := | funSet : mySet -> mySet ->...
В главе STLC Основы языка программирования мы находим следующее: (** [idB = \x:Bool. x] *) Notation...
У меня есть схема индукции для вектора, содержащего значение leb (x <= y), Definition...
Я следую основам программного обеспечения книг по работе с Coq. Я в настоящее время нахожусь в...
У меня есть следующий предикат отражения: Require Import mathcomp.ssreflect.all_ssreflect....
У меня есть натуральное число, которое не равно нулю. Я хочу доказать, что если он равен нулю, то...
У меня есть Fixpoint функция f и лемма следующего вида: Lemma L: forall x, f x = true -> P x....
Я хочу сделать индуктивно определенный перечислимый тип в Coq / SSReflect, например, Inductive E:...
Это часть автоматизации, которую я пытаюсь построить для работы с Is_true. У меня есть это Lemma...
Я хочу доказать not A, приняв A и найдя False.Какой самый короткий и самый общий способ...
Я пытаюсь доказать следующую лемму: forall (A B : Type) (f : A -> B) (l : list A) (y : B), In y...
Моя проблема, кажется, распространена, но ни один из найденных ответов не может ее решить.Я следую...
при построении доказательства в кокиде, я не нашел способа сделать шаг, хотя T1; T2; T3; ...; Tn....
Я хочу создать список смешанных типов boolean и nat. Этот список должен содержать элементы...
Я работаю над формализацией свободных селективных аппликативных функторов в Coq, но борюсь с...
Например, Lemma ex_1: exists n, n=1. Proof. показывает одну подцель: exists n : nat, n = 1 команда...
Я пытаюсь формализовать каждое целое число как класс эквивалентности пар натуральных чисел, где...
Мне понадобилась следующая теорема Lemma cons_eq {A}: forall x (l l' : list A), x :: l = x ::...
Я пытаюсь доказать некоторые эквиваленты FOL. У меня проблемы с использованием законов Деморгана...
Пытаясь доказать следующую лемму, я застрял. Обычно теоремы о списках доказываются с помощью...
Играя с упражнениями ностаттера, я обнаружил еще одно странное поведение.Вот код: Inductive...
До этого я редактировал файл IndProp.v из фондов Программного обеспечения.Но как только я поместил...
Я попробовал следующие доказательства, Require Import List Omega. Import ListNotations. Variable X...