Planet Rocq

Link aggregator of discussions about the Rocq interactive theorem prover

Discourse

CfC: DIALOCO Workshop
Thu 2026/03/05
13th Workshop on Horn Clauses for Verification and Synthesis (HCVS)
Thu 2026/03/05
Missing `stack-compiler` folder if the SF4 book
Wed 2026/03/04
Twelfth Workshop on MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING, Saturday 18th July 2026, Lisbon
Tue 2026/03/03
Package Release : Small Inversions
Mon 2026/03/02
Proof assistants for Teaching Proof and Proving 2026, Orsay, 29 June - 3 July 2026
Sat 2026/02/28
Workshop on Theorem proving components for Educational software ThEdu26 at FLoC, Lisbon, 19 July
Sat 2026/02/28
Rocq Platform minor release 2025.08.2
Thu 2026/02/26
Fifteenth Mathcomp sharing day
Mon 2026/02/23
Rocq Proof Assistant Tutoring
Sun 2026/02/15

Zulip

Proof Assistants Stack Exchange

Coq ssreflect - rewrite inside \big
1 answer
Thu 2026/03/05
Stuck proving the induction hypothesis of multiplication on natural numbers mul_n_S?
Sat 2026/02/28
Defining and Instantiating Functors with Partially Defined Members
1 answer
Wed 2026/02/25
Construct the sum of reals indexing on a finType
1 answer
Tue 2026/02/24
Reverse Mathematics: An Avenue Worth Exploring?
1 answer
Sun 2026/02/22
What strategy should I learn to generalize my observations?
1 answer
Mon 2026/02/16
What is exactly _pattern_value_ in Rocq?
Thu 2026/02/12
Loss of information when performing induction on a relation between a variable and a value
2 answers
Wed 2026/02/11
f_equal failing to help proving record equality
2 answers
Mon 2026/02/09
About the use of command Canonical in Coq for mantaining Record Type information
1 answer
Fri 2026/02/06

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

Reddit

Is Chlipala's book Certified Programming with Dependent Types a good start?
5 comments
Wed 2026/02/04
Why do some Stdlib theorems leave open the possibility of negative naturals?
6 comments
Mon 2026/01/19
Ok I don't get this.
1 comment
Wed 2026/01/07
How can i rewrite expressions?
4 comments
Mon 2026/01/05
Rocq doesn't find a word-for-word copy-paste from the goal
2 comments
Tue 2025/11/11
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
4 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

Stack Overflow

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
How can one translate a Coq proof using Nat to rationals (Rat)?
1 answer
Tue 2025/09/09