Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
Tree-sitter grammar for Rocq (release 0.2.0)
Mon 2026/08/10
MITACS Undergrad Research Internships - 2027 Applications Open
Fri 2026/08/07
Rocq Platform release 2026.07.0 with Rocq 9.1
Thu 2026/08/06
JFLA2027 : Premier appel à communications
3 answers
Wed 2026/08/05
Rocq 9.3+rc1 is out
2 answers
Tue 2026/07/28
Tree-sitter grammar for Rocq
Mon 2026/07/27
Surveying kernel vulnerabilities via non-proof term ways
1 answer
Fri 2026/07/24
NWPT 2026, Second Call for Contributions
Tue 2026/07/21
Stepping through a rocq script programatically?
1 answer
Fri 2026/07/10
Seventeenth Mathcomp sharing day
Wed 2026/07/08
Zulip
AI agents for writing proofs
Essential mailing lists for Rocq users
New Schemes for List
Is it possible to optionally import a file?
✔ Why does (tac1||tac2) fail but ((tac1)||(tac2)) succeed?
Tree-sitter grammar for Rocq (pre-release 0.2.0)
Standard Binary Relations between two distinct types/sets?
Set-typed `sig`
Way to do `setoid_rewrite` (or similar) using a HintDB?
Inconsistency reporting process
Proof Assistants Stack Exchange
An upgrade from Mathcomp v2.4.0 to v2.5.0 going wrong with rationals
1 answer
Sat 2026/08/15
Error when making CoqProject
2 answers
Mon 2026/08/03
Is there a model that contradicts `@eq Type t1 t2 -> @eq Prop t1 t2` or can it be proven?
1 answer
Sun 2026/08/02
Induction COQ Question
2 answers
Sun 2026/08/02
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
1 answer
Fri 2026/07/31
Declaring builders with Hierarchy Builder (Rocq)
1 answer
Thu 2026/07/16
Formalizing "finite or infinite" in Coq/Rocq
5 answers
Thu 2026/07/16
What is the best way to learn Iris completely independently
3 answers
Thu 2026/07/16
Coq - Overloading over multiple parameters with canonical structures
1 answer
Tue 2026/07/14
Mutual inductive proposition to define permutations with parity can't find decreasing argument of fix
2 answers
Tue 2026/07/14
CS Theory Stack Exchange
Is injectivity of constructors for (large) inductive types in Prop, such as squashing, consistent?
Mon 2026/04/27
Finite sets in Coq
1 answer
Fri 2025/01/31
Representations of Planar Graphs in Coq
2 answers
Wed 2025/01/08
Simple Coq simplification question
1 answer
Fri 2024/06/07
What should a proof of correctness for a typechecker actually be proving?
3 answers
Thu 2024/06/06
Formalization of matching logic (logic behind K Framework)
3 answers
Wed 2023/08/16
Notation problem
1 answer
Thu 2023/06/01
Can I define nested mutually dependent types in Coq?
1 answer
Sat 2023/05/13
Defining finite sets inductively in a proof assistant?
1 answer
Tue 2023/04/25
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
3 answers
Thu 2023/03/23
Stack Overflow
Trouble with well-foundedness proofs
Sat 2026/07/11
How to get the fully qualified name of a Rocq tactic?
2 answers
Wed 2026/06/24
Is it possible to convert all higher-order logic and dependent type in Lean/Isabelle/Coq into first-order logic?
1 answer
Wed 2026/05/20
Which vector library to use in coq?
2 answers
Sun 2026/03/22
Can we prove equal subcases have equal induction hypotheses in recursion principle?
6 answers
Tue 2026/02/24
Coq (Rocq) standard library function for converting nat to string?
1 answer
Wed 2026/02/11
Equality of type with equal indices do not typecheck
3 answers
Wed 2026/01/28
How to prove manually (using calc) a Dafny lemma with an existential variable?
3 answers
Sun 2026/01/25
Kind of issue with two-steps recursion
2 answers
Fri 2026/01/09
How to scrutinize a `match` term with return type `a=b -> c`
1 answer
Mon 2025/10/20
