Я пытаюсь понять, как комбинированные тактики ssreflect должны быть «декомпозированы» (или как они складываются в первую очередь). Одна из моих проблем - понять порядок и ассоциативность татикалов. Иногда мне кажется, что порядок идет справа...

Я изучаю Coq и пытаюсь доказать изоморфизм между равенством Мартин-Лофа и равенством пути индукции. Я определил два равенства следующим образом. Module MartinLof. Axiom eq : forall A, A -> A -> Prop. Axiom refl : forall A, forall x : A,...

Я пытаюсь разобраться с каноническими структурами в ssreflect. Я взял два фрагмента кода из здесь . Я принесу кусочки для бул и опционов. Section BoolFinType. Lemma bool_enumP : Finite.axiom [:: true; false]. Proof. by case. Qed....

Coq 8.7 объединяет популярную библиотеку Ssreflect. Следовательно, его библиотеки можно импортировать следующим образом: From Coq Require Import ssreflect ssrfun ssrbool. Однако, когда я пытаюсь импортировать ssrnat он жалуется, что это...

РЕДАКТИРОВАТЬ: я сделал пример более минимальным, введя структуру, которая дополняет элемент, перенося доказательство принадлежности указанного элемента к набору: Structure elem_and_in_proof {T : finType} (s : {set T}) := {el :> T ; Helin : el...

У меня есть функция f, которая принимает x типа fintype A и доказательство P x, чтобы вернуть элемент fintype B. Я хочу вернуть finset f x для всех x, удовлетворяющих P, что можно записать так: From mathcomp Require Import ssreflect ssrbool...

Имея эту лемму Lemma my_lemma n : n %/ 4 * 4 + n %% 4 * 5 - n %% 4 * 4 = n. Proof. (* ? *) (* n %/ 4 * 4 + n %% 4 = n. *) symmetry. apply: divn_eq n 4. Qed. Как преобразовать n %% 4 * 5 - n %% 4 * 4 в n %% 4 ? Тогда в будет кусок...