Следующий код взят из perm.v библиотеки Ssreflect Coq. Я хочу знать, что это за результат. Lemma perm_invK s : cancel (fun x => iinv (perm_onto s x)) s. Proof. by move=> x /=; rewrite f_iinv. Qed.

Я успешно установил Coq 8.6 и CoqIDE в Linux (Ubuntu 17.04). Однако я не знаю, что нужно делать, чтобы добавить SSReflect и MathComp к этой установке. Все ссылки, которые я проверил, показались мне очень запутанными. У кого-нибудь есть прямой и...

Я использую Coq (версии 8.5-6), установленный с Nix. Я хочу установить ssreflect, желательно также с Nix. Единственная информация, которую я нашел об этом, находится здесь . Однако речь идет не об установке ssreflect, а просто о его испытании....

В настоящее время я играю с красно-черными деревьями в Coq и хотел бы оснастить списки nat порядком, чтобы их можно было хранить в красно-черном дереве с помощью модуля MSetRBT . По этой причине я определил seq_lt , как показано: Fixpoint...

Используя ssreflect в следующей лемме: From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype. Lemma nat_dec n m: (m <= n) -> (~~ (m <= n)) -> False. Proof. intros A notA. (* auto. *) red in A. red in notA. (*...

У меня есть два finType с биекцией между ними. На данный момент мне нужно то, что они имеют одинаковую мощность. Однако я не могу найти ни эту лемму, ни другие леммы, с помощью которых можно было бы легко доказать это утверждение. Мне кажется,...

Каков наилучший способ переписать \sum_(i...) (F i - G i) как (\sum_(i...) F i - \sum_(i...) G i) для порядковых номеров с bigop , предполагая, что аннулированные потоки управляются должным образом? Точнее, в отношении этих нижних потоков меня...