Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
A Website for searching theorems and definitions in Rocq projects
Fri 2026/04/17
CfC: The Rocqshop 2026
Fri 2026/04/17
Rocq Platform minor release 2025.08.3
Thu 2026/04/16
April 20: Proof Assistant Seminar at ENS de Lyon
Wed 2026/04/15
2nd CFP - LFMTP 2026 Logical Frameworks and Meta-Languages: Theory and Practice , Lisbon July 24
Mon 2026/04/13
Call for applications for the first Summer School on Programming Languages, Logic, and Software Security Click to teach Gmail that this conversation is important
Fri 2026/04/10
Using Rocq online?
7 answers
Tue 2026/04/07
Rocq 9.2.0 released
Tue 2026/04/07
FLoC'26 workshop - Tribute to Gilles Dowek - Call for talks
Tue 2026/04/07
Theoretical symmetry between specialize and generalize dependent
2 answers
Wed 2026/04/01
Zulip
Selective simplification for record projections
Cross referencing notations
✔ uconstr in notations
Confusion with notations
Need help understanding "level tolerance" warning
Struggling with an is_in inductive predicate
Interest in a dune-buildable version of Flocq?
ind_dep vs ind_nodep schemes
ssreflect patterns in arbitrary tactics
Creating a tactic that can perform `Search`
Proof Assistants Stack Exchange
Reverse Mathematics: An Avenue Worth Exploring?
2 answers
Mon 2026/04/13
Is there any notion of iterable (native, Tarski...) universe in Rocq?
2 answers
Sun 2026/04/12
Stuck in first order logic proof
1 answer
Sun 2026/04/12
An upgrade from Mathcomp v2.4.0 to v2.5.0 going wrong with rationals
Mon 2026/04/06
Rationals' 1 no more recognized in Mathcomp v2.5.0
1 answer
Mon 2026/04/06
Make [...] explicit in Rocq/vsRocq
1 answer
Sun 2026/04/05
Error when making CoqProject
2 answers
Sun 2026/04/05
Is there a model that contradicts `@eq Type t1 t2 -> @eq Prop t1 t2` or can it be proven?
1 answer
Sat 2026/04/04
Induction COQ Question
2 answers
Sat 2026/04/04
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
1 answer
Thu 2026/04/02
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
Stack Overflow
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
How can one handle dependent-type equality proofs (sigma types) in Coq?
2 answers
Tue 2025/09/09
