Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
Formalization of various notions of convergence
Sat 2026/05/09
CfC: The Rocqshop 2026
1 answer
Tue 2026/05/05
Milestone Prize for Foundational Work in Formal Verification
Thu 2026/04/30
Horn Clauses for Verification and Synthesis (HCVS), FLOC 2026 - 2nd CFP
Thu 2026/04/23
First release of marble
Wed 2026/04/22
A Website for searching theorems and definitions in Rocq projects
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
Zulip
`destruct` bug?
Performance Debugging/Optimization for Typeclass Resolution
proofs about logic_monad "split"
Hint Rewrites plus Typeclasses
Large induction-recursion and internal Tarski universes
In Ltac2, check if hypothesis is a section variable
✔ Upgrading Rocq to 9.2.0
Weird bug
Nested Inductives Help
defer to previous impl of tactic when overriding with ::=
Proof Assistants Stack Exchange
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
In Rocq, can I unfold a single "let _ := _ in _" at a time?
1 answer
Mon 2026/04/27
Reverse Mathematics: An Avenue Worth Exploring?
2 answers
Mon 2026/04/13
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
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
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
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
