Planet Rocq

Link aggregator of discussions about the Rocq interactive theorem prover

Discourse

[VsCoq] Release 2.2.6
Tue 2025/05/20
Eleventh Mathcomp sharing day
Tue 2025/05/20
How do I prove the correctness of my Ceaser Cipher?
20 answers
Tue 2025/05/20
Any good resources on extracting Coq to other languages?
Sun 2025/05/18
Implicit Differentiation in Coq — No Reals, No Limits, Just Proof
1 answer
Tue 2025/05/06
Can't a lemma with a universal conclusion be applied to other premises?
5 answers
Tue 2025/04/29
Constructing the category of categories
10 answers
Mon 2025/04/28
Looking for a Coq Tutor
1 answer
Mon 2025/04/28
First Rocq'n'share meeting
Fri 2025/04/25
Tenth Mathcomp sharing day
Fri 2025/04/25

Zulip

Proof Assistants Stack Exchange

Cannot unify equality types (s1 = s2) and (s1 = s2)%S when s1 s2 : S
2 answers
Fri 2025/05/23
Programming language foundations, Equiv: inversion of ceval hypothesis
1 answer
Thu 2025/05/22
What are some strategies for encoding a topology in Coq?
1 answer
Tue 2025/05/20
Debug autorewrite in Coq
1 answer
Mon 2025/05/19
Lower bounds in type theory proof assistant with ordinals and universes without axioms
Sat 2025/05/17
How to deal with forall in hypothesis?
1 answer
Wed 2025/05/14
Programming language foundations, Equiv: optimize_0plus_aexp_sound
1 answer
Tue 2025/05/13
Coq: Syntax error: illegal begin of toplevel:vernac_toplevel
1 answer
Tue 2025/05/13
Coq: how to invoke an overwritten definition
1 answer
Tue 2025/05/13
Why can't Rocq `auto` solve this simple ancestor relationship?
1 answer
Mon 2025/05/12

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

ITP 2025: Call for workshops
Thu 2025/05/22
Problem with scope of lemmas
2 replies
Thu 2025/05/22
PhD Offer / Formally Verified Compilation of Interactive Software
Thu 2025/05/22
TYPES 2025: Final Call for Participation
Wed 2025/05/21
ESOP 2026 - Second Call for Papers
Tue 2025/05/20
ETAPS 2026 - Call for Satellite Events
Tue 2025/05/20
Call for Contributions: RSSRail 2025: 6th International Conference on Reliability, Safety, and Security of Railway Systems
Mon 2025/05/19
[PPDP 25] Extended Call for Papers
Mon 2025/05/19
FSCD 2025: Call for Participation (early registration deadline: *15 June 2025*)
Mon 2025/05/19
CADE-30 Woodie Bledsoe Awards
Sun 2025/05/18

Reddit

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
Proving type preservation with STLC
5 comments
Wed 2025/02/26
What happened to renaming Coq?
4 comments
Wed 2025/02/19
Isabelle student getting to know with Coq
2 comments
Thu 2025/01/30

Stack Overflow

Software Foundations Basics - Theorem lower_grade_lowers need to prove implication Eq = Lt -> Eq = Lt
3 answers
Thu 2025/05/22
Deducing equality from existT equality
2 answers
Tue 2025/05/20
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
Coq: Boolean Comparison of Integers
2 answers
Fri 2025/05/02
In Coq (or Rocq), can't a lemma with a universal conclusion be applied to other premises?
3 answers
Tue 2025/04/29
Rocq: Transparent aliased definition (that instance solver sees though)
2 answers
Thu 2025/04/24
How can I rewrite or use my IH when Coq won't unify my goal with it?
1 answer
Mon 2025/04/14
How to prove that it is not possible for a Nil process to take a transition? (Pi-calculus in Coq)
1 answer
Fri 2025/04/04
while_true_nonterm in Lean4
1 answer
Thu 2025/03/20