Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
A Question on Defining Mutually Inductive Types with Universe Polymorphism
2 answers
Mon 2024/08/12
[VsCoq 2] Release 2.1.7
Wed 2024/08/07
Tactic to apply double negation elimination or excluded middle when goal is False
1 answer
Mon 2024/07/29
Showing falsity in a 'le' exercise from 'IndProp'
1 answer
Fri 2024/07/26
Verified Extraction for Coq 8.19
Tue 2024/07/23
ANN: docker-coq: Bump to Debian 12 (& opam 2.2.0)
Mon 2024/07/22
Tactic to fill a hypothesis of some term in the context
6 answers
Sat 2024/07/20
Coq Platform Docs: a documentation project for Coq and its Platform
Thu 2024/07/18
PhD opportunity: Coq Formalisation of Differentiable Logics
Sat 2024/07/13
[VsCoq] Release 2.1.4
Mon 2024/07/08
The Coq Club mailing list
Research positions in Systems Software Verification
Wed 2024/08/14
POPL 2025 Call for Tutorials
Thu 2024/08/08
IFL 2024 Final call for papers, extended submission deadline.
Mon 2024/08/05
subset-as-sigma-type VS subset-as-predicate
1 reply
Sat 2024/08/03
[Call for Participation] Women in Formal Methods (WiFM-2024) Colocated with CICM-2024
Thu 2024/08/01
Call for Participation: Third Workshop on Formal Verification of Physical Systems (FVPS-2024) - Colocated with CICM-2024
Wed 2024/07/31
HTML output that remembers proof states step by step
3 replies
Tue 2024/07/30
Call for Participation, Functional Software Architecture (Sep 6, Milan)
Mon 2024/07/29
ETAPS 2025 1st joint call for papers
Mon 2024/07/29
PhD Symposium iFM 2024 - Call for Papers
Sat 2024/07/27
Zulip
(
archive
)
✔ Unification behavior with noinit
Possible memory leak in coqtop and coqc
✔ Stating theorem to make the type-checker happy
`case` vs `dependent destruction`
Apply change in a term
✔ Viewing standard library documentation offline
Equations "with" syntax
Equations: Common arguments
`eq_sym` makes me feel stupid
Alectryon usage question
Proof Assistants Stack Exchange
Induction COQ Question
2 answers
Mon 2024/08/12
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
1 answer
Fri 2024/08/09
Accessing nested typeclasses elegantly
1 answer
Fri 2024/08/09
Strict implicit arguments in Coq
1 answer
Thu 2024/08/08
How do I apply a lemma to both sides of an equality hypothesis?
2 answers
Tue 2024/08/06
How to apply the same tactic to multiple match patterns in Ltac
Fri 2024/08/02
STLC substitution behaviour with lambda body normalisation
Wed 2024/07/31
What is a simple example of transforming some Objects / Arrows in visual, categorical definition into actual Coq code. An MWE recipe that is
1 answer
Tue 2024/07/30
Can some existing proof assistant, in its current state of the art, encode this small theory about a twin prime counting function?
1 answer
Mon 2024/07/29
Coq - Overloading over multiple parameters with canonical structures
1 answer
Wed 2024/07/24
Stack Overflow
Why this Fixpoint definition of `half` for list doesn't work?
2 answers
Wed 2024/08/14
Exposing local pointers in trace and producing load event in case of non-volatile load in CompCert
Tue 2024/08/13
"Recursion must act on a single discriminating argument." Doesn't recursion act on both in this recursive definition of subtraction?
1 answer
Thu 2024/08/08
How to prove `A =~ Star re -> B =~ Star re -> A ++ B =~ Star re.` in Coq
Sat 2024/08/03
I have been stuck on MApp for pumping lemma
2 answers
Sat 2024/08/03
Wrong Typeclass Instance used in Coq Proof
1 answer
Wed 2024/07/31
Ltac matches applications of constructors of a type
1 answer
Mon 2024/07/29
Coq's Search command and modules
1 answer
Mon 2024/07/29
Try to understand SSReflect's "have" and square bracket
Thu 2024/07/25
Coq : transitivity fails on list intermediate term
Thu 2024/07/25
CS Theory Stack Exchange
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
What exactly is "large elimination"?
2 answers
Tue 2022/11/15
A Coq question : How to prove the image of the two same valued variables under a function are same?
1 answer
Sun 2022/07/10
Reddit
Proof terms constructed by things like injection, tactic, etc
4 comments
Wed 2024/08/07
Reviews of "Programming Language Foundations" (Volume II of SF series)
6 comments
Mon 2024/08/05
subset-as-sigma-type VS subset-as-predicate
Fri 2024/08/02
"Theorems are types, and their proofs are programs that type-check at the corresponding type"?
7 comments
Fri 2024/08/02
Trudging through Software Foundations Vol 1 / Formal Verification Research
8 comments
Sun 2024/07/28
How to autogenerate a hypothesis name (H1) in "assert (H1 := term)" in Ltac2?
2 comments
Fri 2024/07/26
How does a cumputer understand Fixpoint?
5 comments
Tue 2024/07/23
How to replace ("pose proof") with ("refine" + "let ... in")
7 comments
Mon 2024/07/22
How to Print and normalize the proof object?
4 comments
Tue 2024/07/16
Where is the source file where the "unfold" tactic is defined?
2 comments
Fri 2024/07/12
Coq News
Coq Platform 2021.02.0 is out
Fri 2021/02/26
Coq 8.13.1 is out
Mon 2021/02/22
Coq 8.13.0 is out
Thu 2021/01/07
Coq 8.12.2 is out
Fri 2020/12/11
Coq 8.13+beta1 is out
Mon 2020/12/07
Coq 8.12.1 is out
Mon 2020/11/16
Coq 8.12.0 is out
Mon 2020/07/27
Coq 8.12+beta1 is out
Wed 2020/06/17
Coq 8.11.2 is out
Tue 2020/06/09
Coq 8.11.1 is out
Fri 2020/04/24