Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
Call for Nominations: OOPSLA 2026 Artifact Evaluation Committee
2 answers
Fri 2025/10/31
RocqPL call for presentation
1 answer
Fri 2025/10/24
Rocq 9.1.0 released
Tue 2025/10/14
How can Coq accept an unsound proof if the kernel is correct? (failure modes, examples, and mitigations)
13 answers
Wed 2025/10/08
AI for formal math researcher at Mistral AI
Thu 2025/10/02
Twelfth Mathcomp sharing day
Thu 2025/09/18
[ANN] coq-lsp 0.2.4
Wed 2025/09/17
EuroProofNet Workshop on Proof Libraries 15-16 September 2025
Sun 2025/09/14
Comment importer une preuve d'un fichier.v dans un autre?
2 answers
Mon 2025/08/25
When should ==> be used over ++> for morphisms?
1 answer
Wed 2025/08/20
Zulip
firstorder fails on simple example
✔ Fix on SProp in Type not allowed
Zenodo link for 9.1.0
✔ Need help to get Rocq and proof general working on Nixos
Lowering Ind from Type to Prop
Trouble installing `vscoq-language-server` on WSL (Ubuntu)
✔ Induction Scheme can't start with letins
Trouble understanding sequencing and match
How to properly depend on Rocq in opam files?
SpecTec translation into Rocq
Proof Assistants Stack Exchange
Create a “constant” to avoid writing the same expression several times in tactics
1 answer
Thu 2025/10/30
Defining and Instantiating Functors with Partially Defined Members
1 answer
Tue 2025/10/28
Is there a way to rename parameters when including/reusing a module type in Coq?
1 answer
Mon 2025/10/27
Conditional probability in Mathcomp?
3 answers
Sat 2025/10/25
Loss of information when performing induction on a relation between a variable and a value
2 answers
Fri 2025/10/24
Discriminate the cartesian product in Rocq
1 answer
Wed 2025/10/22
What strategy should I learn to generalize my observations?
1 answer
Sun 2025/10/19
How does the universe-level constraint solver of Rocq work?
1 answer
Fri 2025/10/17
About the use of command Canonical in Coq for mantaining Record Type information
1 answer
Thu 2025/10/09
How can Coq accept an unsound proof if the kernel is correct? (failure modes, examples, and mitigations)
1 answer
Tue 2025/10/07
CS Theory Stack Exchange
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
Why does Coq have Prop?
4 answers
Fri 2022/12/09
The Coq Club mailing list
PLMW@POPL 26 Call for scholarship applications
Wed 2025/10/29
TPSA26 - Deadline Extension
Mon 2025/10/27
Coq-Club is closing down - Join us on Discourse and/or Zulip!
Mon 2025/10/27
Standard library reorganization after update to rocq.
3 replies
Sun 2025/10/26
Existential variable
3 replies
Wed 2025/10/22
2nd CfP: Functional and Logic Programming (FLOPS) (Deadline Dec 8)
Wed 2025/10/22
TYPES 2026 Call for Contributions
Mon 2025/10/20
ANU 33rd Logic Summer School, 1–12 December 2025
Mon 2025/10/20
ECOOP'26 Call for Papers
Fri 2025/10/17
Seeking participants for proof assistant experiment
Thu 2025/10/16
Reddit
Need help to understand coinductive proofs.
2 comments
Fri 2025/10/31
Has anyone done Certified Programming with Dependent Types recently?
6 comments
Wed 2025/10/29
One directional rewrite axiom
3 comments
Sun 2025/10/19
Are IA used for formalizing proofs?
2 comments
Thu 2025/07/24
Why is it permittable to pass Prop where Set is expected?
1 comment
Sun 2025/07/06
Hints for proving proof rule for Hoare REPEAT command?
1 comment
Thu 2025/06/12
Any good resources on how to add a target for Coq Extraction?
Sun 2025/05/18
When will this sub be renamed?
6 comments
Thu 2025/04/24
The statistics of the first 3 volumes of Software Foundations: lines of code & number of exercises
3 comments
Sun 2025/04/06
Need help with proving a Theorem.
6 comments
Sat 2025/03/29
Stack Overflow
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
How can one handle dependent-type equality proofs (sigma types) in Coq?
2 answers
Tue 2025/09/09
How can one translate a Coq proof using Nat to rationals (Rat)?
1 answer
Tue 2025/09/09
Coq convert non exist to forall statement
3 answers
Wed 2025/08/27
Unexpected message about "decreasing argument of fix"
2 answers
Wed 2025/08/13
I have been stuck on MApp for pumping lemma
3 answers
Sun 2025/07/27
How to understand `(elimTF andP top)`?
1 answer
Fri 2025/06/27
What is the origin of the names of I and tt?
1 answer
Thu 2025/06/12
