Я пытаюсь использовать плагин CoqIDE для vim, который нашел на этой странице. Я поместил файл coq_IDE.vim в папку ~ / .vim / ftplugin. Мой текущий файл .vimrc: set showcmd set number imap hl <Esc> filetype plugin on Но когда я...

Я установил Coqide 8.5 с nix . К сожалению, текст черный на всех панелях; нет никакой подсветки синтаксиса (в остальном 8.5 кажется большим улучшением по сравнению с 8.4, который я тоже установил). Я также получаю следующее: (coqide:17272):...

Я новичок в Coq, работаю над написанием теоретико-множественных доказательств. Я понял, что скобки опущены, и мне трудно читать формулу. Например, 1 subgoal A, B : {set T} H : B \subset A ______________________________________(1/1) A :\: A :|:...

Я хочу раскрасить определенную команду и тактику в другой цвет, например. Я хочу, чтобы команды «Печать» и «Найти» были серыми, а «индукция» - каким-то особым цветом, отличным от других тактик. Возможно ли это в ProofGeneral? Если это не...

Я изменил привязку клавиш согласно: https://github.com/coq/coq/wiki/Configuration-of-CoqIDE но теперь я не могу вернуть их в норму. Как мне вернуть их в состояние по умолчанию? Обратите внимание, что Coq уже изменил файл, и я не могу...

В этой ссылке на документ есть полезные теоремы о делении. Я попытался импортировать его с помощью Require Import в CoqIDE 8.9.0, однако, хотя импорт прошел успешно, следующий код не работает с The reference div_lt_upper_bound was not found in...

Пытаюсь доказать eqb_neq : Theorem eqb_neq : forall x y : nat, x =? y = false <-> x <> y. Это мой текущий статус подтверждения: Во время доказательства я дошел до последнего шага, на котором мне просто нужно доказать...

Для определения и следующей теоремы Inductive le : nat -> nat -> Prop := | le_n (n : nat) : le n n | le_S (n m : nat) (H : le n m) : le n (S m). Theorem Sn_le_Sm__n_le_m2 : forall n m, S n <= S m -> n <= m....

Я написал этот Индуктивный предикат и часть доказательства его (сильной) спецификации: Inductive SumPairs : (nat*nat) -> list (nat*nat) -> Prop := | sp_base : SumPairs (0,0) nil | sp_step : forall (l0:list (nat*nat)) (n0 n1: nat)...