Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
News Rocq Platform Docs
1 answer
Tue 2026/05/26
TyDe 2026 - Call for Papers
Wed 2026/05/20
Call for Presentations: ML Family Workshop 2026
Wed 2026/05/20
Sixteenth Mathcomp sharing day
Mon 2026/05/18
NWPT 2026, First Call for Papers
Mon 2026/05/18
Formalization of various notions of convergence
Sat 2026/05/09
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
Zulip
Behaviour of tactic progress
An error in ch. Equiv of vol. 2 (PLF) of the SF series
Implicit arguments in an abbreviation
Controlling Location of Rewriting (mimic Lean's `conv`?)
✔ "true" expected to have type "nat"!?
✔ Missing induction hypothesis
Alias to eq in PeanoNat
✔ Error importing from PLF in vol. 2 of Software Foundations
Apply fail negation
`Proper` signatures that ignore arguments?
Proof Assistants Stack Exchange
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
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
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
