Planet Rocq

Link aggregator of discussions about the Rocq interactive theorem prover

Discourse

Problem with Ltac2 Notation and Control.enter
3 answers
Tue 2026/06/09
Blockchain formal verification @ category labs
Sat 2026/06/06
Richard Bird Distinguished Dissertation Award
Wed 2026/06/03
Rocq'n'Share 2026: happening in one month!
Sat 2026/05/30
News Rocq Platform Docs
2 answers
Fri 2026/05/29
PLMW @ ICFP call for funding applications
Fri 2026/05/29
Permanent researcher position at Mines Paris - PSL
Fri 2026/05/29
Technical Associate positoin at the AI for Math Fund
Fri 2026/05/29
TyDe 2026 - Call for Papers
Wed 2026/05/20
Call for Presentations: ML Family Workshop 2026
Wed 2026/05/20

Zulip

Proof Assistants Stack Exchange

What strategy should I learn to generalize my observations?
1 answer
Tue 2026/06/16
Transplanting rocq library files from one computer to another
2 answers
Thu 2026/06/11
Isar-style proofs for Rocq or Lean?
1 answer
Sat 2026/06/06
About the use of command Canonical in Coq for mantaining Record Type information
1 answer
Sat 2026/06/06
In Rocq, can I unfold a single "let _ := _ in _" at a time?
1 answer
Wed 2026/05/27
Formalizing "finite or infinite" in Coq
5 answers
Sat 2026/05/23
Debug autorewrite in Coq
1 answer
Thu 2026/05/14
Is there any notion of iterable (native, Tarski...) universe in Rocq?
2 answers
Thu 2026/05/07
Make [...] explicit in Rocq/vsRocq
1 answer
Tue 2026/05/05
Reverse Mathematics: An Avenue Worth Exploring?
2 answers
Mon 2026/04/13

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

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
How to deal with potentially-aliased arguments in VST?
1 answer
Sat 2025/09/13
How can one handle by case analysis a boolP expression in Coq/ssreflect?
2 answers
Wed 2025/09/10