Planet Rocq

Discourse

• Compiler and Verification Engineer Positions at Cryspen
  2 answers
  Wed 2026/01/21
• Post-doc position at Inria Rennes on AI and formal methods
  Tue 2026/01/20
• Assistant professor position at Télécom Paris "Formal Methods at the crossroads of Hardware and Software"
  Fri 2026/01/09
• Security Foundations (new volume of Software Foundations)
  Thu 2026/01/08
• Issues with Require from stdpp
  9 answers
  Tue 2026/01/06
• Recursive inductive notation and incremental type checking
  1 answer
  Sun 2026/01/04
• Rocq and mathcomp from Homebrew do not work well
  2 answers
  Wed 2025/12/31
• Local Sequence tactial and Incorrect number of goals
  1 answer
  Tue 2025/12/23
• Beginner: stuck on simple proof with negation
  4 answers
  Sat 2025/12/20
• Tuareg-mode doesn't really work for mlg file
  1 answer
  Sat 2025/12/20

Zulip

• Best practices for auto
• Experiment: local import `let Import` in terms
• QuickChick function type counterexample
• Difference match and destruct
• destruct tactic on parameterised inductive types
• Injection and Discriminate by definition ?
• Debugging gallina programs
• ✔ Parameters vs Fields in typeclasses
• Fixpoint apply a fixpoint, yielding dependent type
• How to Use Lemmas with Existential Quantifiers Easily

Proof Assistants Stack Exchange

• How should I decode a universe inconsistency error?
  2 answers
  Tue 2026/01/20
• Debug autorewrite in Coq
  1 answer
  Wed 2026/01/14
• Is there a way to coerce some specific type constructor X: Type -> Type into Type in Rocq?
  1 answer
  Thu 2026/01/08
• An issue with generalized rewriting in Rocq
  2 answers
  Wed 2026/01/07
• Equality with dependent types in rocq
  1 answer
  Tue 2025/12/30
• 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

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

Reddit

• Why do some Stdlib theorems leave open the possibility of negative naturals?
  6 comments
  Mon 2026/01/19
• Ok I don't get this.
  1 comment
  Wed 2026/01/07
• How can i rewrite expressions?
  4 comments
  Mon 2026/01/05
• 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

Stack Overflow

• How to prove manually (using calc) a Dafny lemma with an existential variable?
  2 answers
  Thu 2026/01/22
• 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
• 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