# Miscellaneous

**URL:** https://discourse.rocq-prover.org/c/miscellaneous/10.md

[Latest](https://discourse.rocq-prover.org/latest.md) · [Categories](https://discourse.rocq-prover.org/categories.md) · [Tags](https://discourse.rocq-prover.org/tags.md)

---

## [About the Miscellaneous category](https://discourse.rocq-prover.org/t/about-the-miscellaneous-category/17)

<div class="topic-metadata">

**Author:** [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Replies:** 0\
**Last updated:** [February 10, 2019, 9:59pm UTC](https://discourse.rocq-prover.org/t/about-the-miscellaneous-category/17 "2019-02-10T21:59:35Z")

</div>

Topics that don’t fit elsewhere: questions about type theory, links to discuss, comments on Discourse, the Rocq community… Write to rocq+miscellaneous@discoursemail.com to start a new topic in this category via e-mail.

---

## [News about the "sherlocoq" service?](https://discourse.rocq-prover.org/t/news-about-the-sherlocoq-service/3130)

<div class="topic-metadata">

**Author:** [@erikmd](https://discourse.rocq-prover.org/u/erikmd)\
**Replies:** 1\
**Last updated:** [October 8, 2026, 12:39am UTC](https://discourse.rocq-prover.org/t/news-about-the-sherlocoq-service/3130 "2026-10-08T00:39:14Z")

</div>

Dear all, I came across the Sherlocode service at the following URL: which allows one to “Search across 17 million lines of OCaml available on opam”. It also says: "NEW: also available for Coq with Sherlocoq!" Unfo…

---

## [Formalization of various notions of convergence](https://discourse.rocq-prover.org/t/formalization-of-various-notions-of-convergence/3028)

<div class="topic-metadata">

**Author:** [@LLyaudet](https://discourse.rocq-prover.org/u/LLyaudet)\
**Replies:** 0\
**Last updated:** [May 9, 2026, 7:25pm UTC](https://discourse.rocq-prover.org/t/formalization-of-various-notions-of-convergence/3028 "2026-05-09T19:25:38Z")

</div>

Hello, I wrote a note on notions of convergence of sequences of functions in mathematics. My goal was to see by myself if many definitions were possible. I did found quite a few definitions at the end. Maybe the appr…

---

## [Theoretical symmetry between specialize and generalize dependent](https://discourse.rocq-prover.org/t/theoretical-symmetry-between-specialize-and-generalize-dependent/3006)

<div class="topic-metadata">

**Author:** [@qvd808](https://discourse.rocq-prover.org/u/qvd808)\
**Replies:** 2\
**Last updated:** [April 1, 2026, 6:09pm UTC](https://discourse.rocq-prover.org/t/theoretical-symmetry-between-specialize-and-generalize-dependent/3006 "2026-04-01T18:09:31Z")

</div>

Hi all, I am currently following “Software Foundations” to learn Rocq, and I came across “specialize” and “generalize dependent.” One seems to remove a quantifier and the other seems to add one. I found this interesting…

---

## [Missing \`stack-compiler\` folder if the SF4 book](https://discourse.rocq-prover.org/t/missing-stack-compiler-folder-if-the-sf4-book/2957)

<div class="topic-metadata">

**Author:** [@gugo](https://discourse.rocq-prover.org/u/gugo)\
**Replies:** 0\
**Last updated:** [March 4, 2026, 10:33am UTC](https://discourse.rocq-prover.org/t/missing-stack-compiler-folder-if-the-sf4-book/2957 "2026-03-04T10:33:30Z")

</div>

Hey, I am currently studying the SF books in my free time and I can’t find the stack-compiler folder mentioned in chapter QuickChickTool.v for the fourth Software Foundations book: QuickChick: Property-Based Testing in R…

---

## [Beginner: stuck on simple proof with negation](https://discourse.rocq-prover.org/t/beginner-stuck-on-simple-proof-with-negation/2886)

<div class="topic-metadata">

**Author:** [@ReiHakiri](https://discourse.rocq-prover.org/u/ReiHakiri)\
**Replies:** 4\
**Last updated:** [December 20, 2025, 3:10pm UTC](https://discourse.rocq-prover.org/t/beginner-stuck-on-simple-proof-with-negation/2886 "2025-12-20T15:10:46Z")

</div>

Hello, I just started learning Coq and I’m trying to prove the following thm. \\neg \\exists n: nat, \\forall m: nat, n = m Here’s my attempt: Theorem attempt: ~ exists n: nat, forall m: nat, n = m. Proof. unfold not…

---

## [Why does the conversion rule for CIC apply only to types instead of all terms?](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790)

<div class="topic-metadata">

**Author:** [@sskeirik](https://discourse.rocq-prover.org/u/sskeirik)\
**Replies:** 11\
**Last updated:** [August 16, 2025, 10:21pm UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790 "2025-08-16T22:21:20Z")

</div>

I’m currently learning Rocq and working my way through the typing rules. One thing that stuck out to me while I was reading the rules is: the convertibility rules are defined for terms in general; however, the convers…

---

## [What should the color of the Rocq Prover language on GitHub be?](https://discourse.rocq-prover.org/t/what-should-the-color-of-the-rocq-prover-language-on-github-be/2779)

<div class="topic-metadata">

**Author:** [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Replies:** 3\
**Last updated:** [July 28, 2025, 8:04am UTC](https://discourse.rocq-prover.org/t/what-should-the-color-of-the-rocq-prover-language-on-github-be/2779 "2025-07-28T08:04:04Z")

</div>

Since this GitHub Linguist pull request was released, GitHub correctly detects .v files as Rocq Prover code. However, for now, we haven’t changed the color of the language. The color is currently inherited from the one o…

---

## [How to formalize dependent setoid morphisms?](https://discourse.rocq-prover.org/t/how-to-formalize-dependent-setoid-morphisms/2759)

<div class="topic-metadata">

**Author:** [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Replies:** 5\
**Last updated:** [July 16, 2025, 3:00pm UTC](https://discourse.rocq-prover.org/t/how-to-formalize-dependent-setoid-morphisms/2759 "2025-07-16T15:00:04Z")

</div>

At the bottom of the post you can find a formalization of “setoids” and “setoid morphisms” (nothing fancy except it’s u-polymorphic: but I am still on Coq 8.18 – and please don’t mind the naming too much, this is all sti…

---

## [Implicit Differentiation in Coq — No Reals, No Limits, Just Proof](https://discourse.rocq-prover.org/t/implicit-differentiation-in-coq-no-reals-no-limits-just-proof/2689)

<div class="topic-metadata">

**Author:** [@heliocoeur](https://discourse.rocq-prover.org/u/heliocoeur)\
**Replies:** 1\
**Last updated:** [May 6, 2025, 3:21pm UTC](https://discourse.rocq-prover.org/t/implicit-differentiation-in-coq-no-reals-no-limits-just-proof/2689 "2025-05-06T15:21:07Z")

</div>

A Constructive, Symbolic Theory of Implicit Differentiation in Coq Overview: This development presents a fully formal, self-contained theory of symbolic differentiation and implicit derivatives, built entirely within t…

---

## [Constructing the category of categories](https://discourse.rocq-prover.org/t/constructing-the-category-of-categories/2652)

<div class="topic-metadata">

**Author:** [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Replies:** 10\
**Last updated:** [April 28, 2025, 7:42pm UTC](https://discourse.rocq-prover.org/t/constructing-the-category-of-categories/2652 "2025-04-28T19:42:15Z")

</div>

\[Posting in Misc since this is more of a mathematics question than a Rocq-specific question.\] This is an excerpt of a development of a “theory of categories”, where I get stuck at defining the category of categories, ak…

---

## [Looking for a Coq Tutor](https://discourse.rocq-prover.org/t/looking-for-a-coq-tutor/2661)

<div class="topic-metadata">

**Author:** [@zamojtel](https://discourse.rocq-prover.org/u/zamojtel)\
**Replies:** 1\
**Last updated:** [April 28, 2025, 1:46pm UTC](https://discourse.rocq-prover.org/t/looking-for-a-coq-tutor/2661 "2025-04-28T13:46:05Z")

</div>

Hi everyone, I’m currently studying Computer Science, and this semester we’re covering Coq in my Advanced Functional Programming class. It’s completely new to me and I’m finding it difficult to keep up with the course m…

---

## [Internships in software verification](https://discourse.rocq-prover.org/t/internships-in-software-verification/2594)

<div class="topic-metadata">

**Author:** [@uussieerr](https://discourse.rocq-prover.org/u/uussieerr)\
**Replies:** 0\
**Last updated:** [April 7, 2025, 11:03am UTC](https://discourse.rocq-prover.org/t/internships-in-software-verification/2594 "2025-04-07T11:03:04Z")

</div>

I graduated from the university with a degree in computer science with PL related courses. I have some experience working in a company that deals with things related to programming languages ​​in general. There I was wri…

---

## [A logo that Rocqs](https://discourse.rocq-prover.org/t/a-logo-that-rocqs/2489)

<div class="topic-metadata">

**Author:** [@Melrok](https://discourse.rocq-prover.org/u/Melrok)\
**Replies:** 0\
**Last updated:** [December 11, 2024, 2:41pm UTC](https://discourse.rocq-prover.org/t/a-logo-that-rocqs/2489 "2024-12-11T14:41:45Z")

</div>

As I explained in the 3rd december Coq Call, I drafted a logo for Rocq and want to make it available for the community. So here it is! (there’s also a second draft) I decided to use the CC-by license, so everyone ca…

---

## [Are dependent types necessary for modelling F Omega](https://discourse.rocq-prover.org/t/are-dependent-types-necessary-for-modelling-f-omega/2422)

<div class="topic-metadata">

**Author:** [@yiyunliu](https://discourse.rocq-prover.org/u/yiyunliu)\
**Replies:** 0\
**Last updated:** [September 6, 2024, 4:30pm UTC](https://discourse.rocq-prover.org/t/are-dependent-types-necessary-for-modelling-f-omega/2422 "2024-09-06T16:30:36Z")

</div>

Tangentially related to this old post: Why dependent type theory? It is well-known that SN for impredicative System F requires an impredicative metalanguage, but I started to wonder if SN for impredicative System Fω (im…

---

## [Why are then no clearly-visible signs of the Coq-\>Rocq rename?](https://discourse.rocq-prover.org/t/why-are-then-no-clearly-visible-signs-of-the-coq-rocq-rename/2369)

<div class="topic-metadata">

**Author:** [@gasche](https://discourse.rocq-prover.org/u/gasche)\
**Replies:** 4\
**Last updated:** [July 5, 2024, 3:34pm UTC](https://discourse.rocq-prover.org/t/why-are-then-no-clearly-visible-signs-of-the-coq-rocq-rename/2369 "2024-07-05T15:34:24Z")

</div>

A few days ago I told someone that Coq is getting renamed into Rocq. They are not active in the community so they hadn’t heard. They were surprised and a bit skeptical at first, so they searched for the project homepage c…

---

## [Looking for Advice on Codifying Theoretical Math in Coq](https://discourse.rocq-prover.org/t/looking-for-advice-on-codifying-theoretical-math-in-coq/2331)

<div class="topic-metadata">

**Author:** [@Joyes](https://discourse.rocq-prover.org/u/Joyes)\
**Replies:** 1\
**Last updated:** [July 4, 2024, 9:52am UTC](https://discourse.rocq-prover.org/t/looking-for-advice-on-codifying-theoretical-math-in-coq/2331 "2024-07-04T09:52:27Z")

</div>

Hello Everyone :hugs:, I could appreciate some advice from more seasoned users as I work on a project that includes formalising multiple mathematical conclusions using Coq proof assistance. My primary area of expertise…

---

## [Why Am I Unable to See My Post?](https://discourse.rocq-prover.org/t/why-am-i-unable-to-see-my-post/2335)

<div class="topic-metadata">

**Author:** [@Joyes](https://discourse.rocq-prover.org/u/Joyes)\
**Replies:** 1\
**Last updated:** [July 4, 2024, 6:30am UTC](https://discourse.rocq-prover.org/t/why-am-i-unable-to-see-my-post/2335 "2024-07-04T06:30:42Z")

</div>

Hello, I recently posted a thread: https://discourse.rocq-prover.org/t/looking-for-advice-on-codifying-theoretical-math-in-coq/2331/1 I got a notification that left me disappointed as it shows my content is spam. I don’t …

---

## [Coq's Cumulativity](https://discourse.rocq-prover.org/t/coqs-cumulativity/2334)

<div class="topic-metadata">

**Author:** [@Ailrun](https://discourse.rocq-prover.org/u/Ailrun)\
**Replies:** 2\
**Last updated:** [June 22, 2024, 7:33pm UTC](https://discourse.rocq-prover.org/t/coqs-cumulativity/2334 "2024-06-22T19:33:08Z")

</div>

While taking a look at the Coq’s (or CIC’s) subtyping rules, I noticed that for pi type, the rule does not allow contravariant subtyping for the argument. Is there a reason to not have this? (Like causing inconsistency …

---

## [Old Critical Bug described as affecting virtual machine but also triggers on other conversion machines](https://discourse.rocq-prover.org/t/old-critical-bug-described-as-affecting-virtual-machine-but-also-triggers-on-other-conversion-machines/2316)

<div class="topic-metadata">

**Author:** [@chluebi](https://discourse.rocq-prover.org/u/chluebi)\
**Replies:** 4\
**Last updated:** [June 5, 2024, 3:26pm UTC](https://discourse.rocq-prover.org/t/old-critical-bug-described-as-affecting-virtual-machine-but-also-triggers-on-other-conversion-machines/2316 "2024-06-05T15:26:33Z")

</div>

I am currently doing work on reproducing old coq inconsistency bugs about the conversion machines. Specifically I am currently working on reproducing https://github.com/coq/coq/issues/11321 which in the critical bugs doc…

---

## [Proof verifier design](https://discourse.rocq-prover.org/t/proof-verifier-design/2290)

<div class="topic-metadata">

**Author:** [@stewbasic](https://discourse.rocq-prover.org/u/stewbasic)\
**Replies:** 3\
**Last updated:** [May 19, 2024, 7:03am UTC](https://discourse.rocq-prover.org/t/proof-verifier-design/2290 "2024-05-19T07:03:06Z")

</div>

I have some thoughts about how to design a proof verifier, and want to get feedback (eg why existing systems don’t do things this way, or if there are some that do). LCF-style proof systems generally have a small logica…

---

## [Coqide: What settings can I set in the gtk.css?](https://discourse.rocq-prover.org/t/coqide-what-settings-can-i-set-in-the-gtk-css/2269)

<div class="topic-metadata">

**Author:** [@wolly](https://discourse.rocq-prover.org/u/wolly)\
**Replies:** 3\
**Last updated:** [May 9, 2024, 5:45pm UTC](https://discourse.rocq-prover.org/t/coqide-what-settings-can-i-set-in-the-gtk-css/2269 "2024-05-09T17:45:33Z")

</div>

Hello all, Firstly this is my first time using this forum - whilst I’ve read the guidelines I don’t have a working model of the de facto rules for good behavior / interactions here, so please let me know if I’m being un…

---

## [Developing a proven, secure communication protocol from scratch](https://discourse.rocq-prover.org/t/developing-a-proven-secure-communication-protocol-from-scratch/1988)

<div class="topic-metadata">

**Author:** [@hmltn2](https://discourse.rocq-prover.org/u/hmltn2)\
**Replies:** 5\
**Last updated:** [April 10, 2024, 5:25pm UTC](https://discourse.rocq-prover.org/t/developing-a-proven-secure-communication-protocol-from-scratch/1988 "2024-04-10T17:25:47Z")

</div>

Here is the content of my recent stack overflow post discussing what I intend to begin working on, immediately: Formally verified email or communication? This question is contextualized by having an account hacked whic…

---

## [ChatGPT can help translate between Coq and Lean](https://discourse.rocq-prover.org/t/chatgpt-can-help-translate-between-coq-and-lean/2203)

<div class="topic-metadata">

**Author:** [@tenedor](https://discourse.rocq-prover.org/u/tenedor)\
**Replies:** 0\
**Last updated:** [February 13, 2024, 6:06pm UTC](https://discourse.rocq-prover.org/t/chatgpt-can-help-translate-between-coq-and-lean/2203 "2024-02-13T18:06:42Z")

</div>

I ran some simple experiments that may be of interest to folks here: porting between Coq and Lean Cross-posted to Lean Zulip: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/t…

---

## [Notes from the CoqPL 2024 Q/A session](https://discourse.rocq-prover.org/t/notes-from-the-coqpl-2024-q-a-session/2183)

<div class="topic-metadata">

**Author:** [@gasche](https://discourse.rocq-prover.org/u/gasche)\
**Replies:** 9\
**Last updated:** [January 29, 2024, 9:38pm UTC](https://discourse.rocq-prover.org/t/notes-from-the-coqpl-2024-q-a-session/2183 "2024-01-29T21:38:45Z")

</div>

CoqPL 2024 (see call for presentations) had a Q/A session with Coq developers (@ejgallego, @ybertot, @rtetley, @mattam82) and the audience in the room. Below are my notes of the questions and answers. Q: on the rename,…

---

## [Is there a full documentation of Coq's grammar?](https://discourse.rocq-prover.org/t/is-there-a-full-documentation-of-coqs-grammar/647)

<div class="topic-metadata">

**Author:** [@qawbecrdtey](https://discourse.rocq-prover.org/u/qawbecrdtey)\
**Replies:** 15\
**Last updated:** [December 18, 2023, 7:05am UTC](https://discourse.rocq-prover.org/t/is-there-a-full-documentation-of-coqs-grammar/647 "2023-12-18T07:05:16Z")

</div>

Looking for the grammar at the doc requires too much time. Is there a nice page or pdf that full grammar of coq is listed?

---

## [How do each of the three main lambda calculus features impact what coq can represent?](https://discourse.rocq-prover.org/t/how-do-each-of-the-three-main-lambda-calculus-features-impact-what-coq-can-represent/2077)

<div class="topic-metadata">

**Author:** [@caverill](https://discourse.rocq-prover.org/u/caverill)\
**Replies:** 4\
**Last updated:** [October 20, 2023, 12:58am UTC](https://discourse.rocq-prover.org/t/how-do-each-of-the-three-main-lambda-calculus-features-impact-what-coq-can-represent/2077 "2023-10-20T00:58:35Z")

</div>

We know that the CoC is essentially a calculus combining dependent typing, parametric polymorphism, and type constructors. What exactly do each of these three give us in terms of representation power when we’re writing t…

---

## [Is it possible to get parentheses' positions or an operator's associativity from an AST?](https://discourse.rocq-prover.org/t/is-it-possible-to-get-parentheses-positions-or-an-operators-associativity-from-an-ast/2018)

<div class="topic-metadata">

**Author:** [@toku-sa-n](https://discourse.rocq-prover.org/u/toku-sa-n)\
**Replies:** 3\
**Last updated:** [August 27, 2023, 2:55pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-get-parentheses-positions-or-an-operators-associativity-from-an-ast/2018 "2023-08-27T14:55:35Z")

</div>

Hi. While I was writing a Coq formatter, I encountered a problem of not being able to get information of parentheses. Consider the following Theorem (from Induction: Proof by Induction in Software Foundation). Theorem …

---

## [Why is Coq consistent? What is the intended semantics?](https://discourse.rocq-prover.org/t/why-is-coq-consistent-what-is-the-intended-semantics/347)

<div class="topic-metadata">

**Author:** [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Replies:** 21\
**Last updated:** [September 27, 2019, 10:40am UTC](https://discourse.rocq-prover.org/t/why-is-coq-consistent-what-is-the-intended-semantics/347 "2019-09-27T10:40:18Z")

</div>

This seems to be missing from the faq. I have a fairly good idea of the answer, but was surprised not to find this documented (in one place). Am I overlooking something?

---

## [Need coq tutor](https://discourse.rocq-prover.org/t/need-coq-tutor/1873)

<div class="topic-metadata">

**Author:** [@Rani\_Deol](https://discourse.rocq-prover.org/u/Rani_Deol)\
**Replies:** 2\
**Last updated:** [April 22, 2023, 7:56pm UTC](https://discourse.rocq-prover.org/t/need-coq-tutor/1873 "2023-04-22T19:56:34Z")

</div>

Hello there I have a unique request. My son is taking fourth year computer science course at university in Vancouver British Columbia canada. Professor has chosen coq language to study for the class. My son finds it dif…

[Next page](https://discourse.rocq-prover.org/c/miscellaneous/10.md?page=1)