Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
Comment importer une preuve d'un fichier.v dans un autre?
2 answers
Mon 2025/08/25
When should ==> be used over ++> for morphisms?
1 answer
Wed 2025/08/20
Why does the conversion rule for CIC apply only to types instead of all terms?
12 answers
Sun 2025/08/17
What should the color of the Rocq Prover language on GitHub be?
3 answers
Mon 2025/07/28
How to formalize dependent setoid morphisms?
5 answers
Wed 2025/07/16
Rocqshop 2025 call for presentations
2 answers
Tue 2025/07/15
Release of Iris 4.4 and std++ 1.12, Announcement of iris-contrib
Wed 2025/07/02
Non-constructive proof
19 answers
Mon 2025/06/30
Announcement: opam-repository (opam.ocaml.org) archiving process
Tue 2025/06/24
VSTTE 2025: Second call for papers (deadline: July 18th)
Wed 2025/06/18
Zulip
Indexed Inductive types - Double negation stable?
Faster setoid rewrite using stdpp's `solve_proper` tactic
Rocqshop '25 informations
Any work done for creating semantic patches for Coq/Rocq?
simple design q about typeclasses
Simplifying adding between N, Z, and nat.
auto + ZArith introduces axioms
Docs of Ltac2: what do you want?
ring tactic for setoids in Type
Formalization of a UTF-8 decoder and encoder
Proof Assistants Stack Exchange
Do 1 step of beta reduction in unfold
2 answers
Mon 2025/08/25
Coercion from atom to atomic formula
1 answer
Tue 2025/08/19
Show that A -> B is a finType when A and B are finTypes
1 answer
Sat 2025/08/16
Function from type class doesn't simplify
1 answer
Fri 2025/08/15
Custom notations: wrong parsing
1 answer
Thu 2025/08/14
How to create an analogue to parent type from OOP
1 answer
Tue 2025/08/12
Error when making CoqProject
2 answers
Fri 2025/08/08
Induction COQ Question
2 answers
Thu 2025/08/07
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
1 answer
Tue 2025/08/05
Alternative to tedious assert-rewrite for trivial operations?
3 answers
Sun 2025/08/03
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
Last CFP - CPP 2026 - Certified Programs and Proofs
Fri 2025/08/29
S-REPLS (Amazon, 29 Oct) - Call for talks and registration
Thu 2025/08/28
Call for Abstracts: Workshop on Natural Formal Mathematics (NatFoM 2025) in Brasilia
Tue 2025/08/26
DataMod 2025 - Final Call for Papers, Extended Deadline
Tue 2025/08/26
PEPM 2026 Call for Papers
Tue 2025/08/26
CfP: Symposium on Functional and Logic Programming (May 26-28, Akita, Japan)
Mon 2025/08/25
Coq for a mathematical game played by Einstein
Sat 2025/08/23
Tenure-track opening in Logic/Verification at Saarland University
Fri 2025/08/22
(CfP) Dafny Workshop at POPL 2026
Wed 2025/08/20
SEFM 2025: call for workshops papers
Tue 2025/08/19
Reddit
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
Need help with proving a Theorem.
6 comments
Sat 2025/03/29
Scottish Programming Languages and Verification Summer School 2025
Fri 2025/03/28
#49 Self-Education in PL - Ryan Brewer
1 comment
Sat 2025/03/15
If you don't understand Fixpoint and Inductive Types, I've created a programming language to help you
2 comments
Thu 2025/03/13
Stack Overflow
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
Providing and using proofs as arguments to a function in Rocq
1 answer
Wed 2025/06/04
Deducing equality from existT equality
2 answers
Mon 2025/05/26
Software Foundations Basics - Theorem lower_grade_lowers need to prove implication Eq = Lt -> Eq = Lt
3 answers
Thu 2025/05/22
How to temporarily disable notations in Coq
2 answers
Fri 2025/05/09
Prove that an element of fin 1 is exactly 0
2 answers
Thu 2025/05/08
