Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
New proof assistant working group at ENS de Lyon
1 answer
Sat 2025/12/13
Post doc position available at University of North Carolina Charlotte, USA
Tue 2025/12/09
UK home fees PhD position in Mathematically Structured Programming at Strathclyde
2 answers
Sun 2025/12/07
How to refer a hypothesis in an assert?
1 answer
Sun 2025/12/07
First release of `rocqblueprint` tool for building formalization blueprints
Fri 2025/12/05
FMBC CFP
Tue 2025/12/02
PhD positions in Automated and Foundational Verification at ISTA
Thu 2025/11/27
"Numerical Computations and Proofs: from Proof-Assistants to Aerospace Applications" (habil. defense, December 1st)
1 answer
Mon 2025/11/24
Thirteenth Mathcomp sharing day
Mon 2025/11/24
MathComp 2.5.0 released
Mon 2025/11/17
Zulip
Design Qs for Language Formalization Preliminaries
✔ Using stdpp's gmap with a custom key
✔ Missing NoDup Lemma in StdLib
How to ask a question?
✔ `constructor` and `apply` tactics rewrite too aggressively
✔ equations install via nix-shell
✔ opam installation of 9.1.0
Rocq Logo
New feature: automatically generated goal names
✔ How to remove space in notation
Proof Assistants Stack Exchange
2-nd order logics: princess and tiger problem from Smullyan
2 answers
Sat 2025/12/13
Is there a website where I can open Rocq online?
2 answers
Fri 2025/12/12
Textbook references for using Coq for higher math
1 answer
Mon 2025/12/08
Error when making CoqProject
2 answers
Sat 2025/12/06
Is there a model that contradicts `@eq Type t1 t2 -> @eq Prop t1 t2` or can it be proven?
1 answer
Fri 2025/12/05
Induction COQ Question
2 answers
Fri 2025/12/05
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
1 answer
Wed 2025/12/03
Mathcomp's all_ssreflect prevents from compiling
3 answers
Mon 2025/11/17
Coq - Overloading over multiple parameters with canonical structures
1 answer
Sun 2025/11/16
What is the standard equivalent of an Ltac match in lean4?
1 answer
Thu 2025/11/13
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
PhD position at University of New South Wales (UNSW) Sydney
Fri 2025/11/28
Jonathan Bowen to give the Peter Landin Semantics Seminar: 4 December 2025, BCS London office and on Zoom
Wed 2025/11/26
FME Teaching Tutorial on November 28, 2025 @ 10 am CET: Prof Graeme Smith, University of Queensland, Australia, on "Autograding weakest precondition proofs and Dafny specifications"
Fri 2025/11/21
Four Assistant/Associate Professor positions in Computing at Imperial College London - deadline 15th December
Thu 2025/11/20
CfP: SLE 2026 - 19th ACM SIGPLAN International Conference on Software Language Engineering
Thu 2025/11/20
FMBC 2026 - First Call for Papers
1 reply
Thu 2025/11/20
ECOOP 2026: Call for AEC members
Wed 2025/11/19
TYPES 2025: Post-proceedings Final Call for Papers
Mon 2025/11/17
Multiple Postdoc and PhD positions in Melbourne
Fri 2025/11/14
Computability in Europe - CiE 2026, July 27-31. First Call for Papers
Fri 2025/11/14
Reddit
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
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
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
