Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Call for volunteer maintainers of CoqIDE
Fri 2023/06/02
Deadline Extension: CfP 2023 Coq workshop, May 30th
Fri 2023/05/26
2nd Call for presentations: 2023 Coq workshop
Tue 2023/05/16
MathComp 2.0.0 released
Mon 2023/05/15
Help to criate my first proof
1 answer
Fri 2023/05/12
MathComp 1.17.0 released
Wed 2023/05/10
How to do simple structural coercion
4 answers
Mon 2023/05/08
Anonymous example
1 answer
Sun 2023/05/07
Is there a way to extract ASTs from the Coq compiler?
1 answer
Thu 2023/05/04
2023 Coq workshop call for presentations
Tue 2023/04/25
The Coq Club mailing list
Call for volunteer maintainers of CoqIDE
Fri 2023/06/02
Call for Participation -- LFMTP 2023
Fri 2023/06/02
TyDe 2023 - Second Call for Papers and Deadline Extension
Fri 2023/06/02
Call for Papers: JFP Special Issue on Program Calculation
Tue 2023/05/30
UNIF 2023 Call for Participation
Sat 2023/05/27
[ICTAC 2023] Second call for papers – deadline 16 June 2023
Fri 2023/05/26
Deadline Extension: CfP 2023 Coq workshop, May 30th
Fri 2023/05/26
Turning Non-Primitive Recursive Function into Primitive Recursive Function
15 replies
Wed 2023/05/24
GPCE 2023 Call for Papers (with complete committee information)
Tue 2023/05/23
GPCE 2023 Call for Papers
Tue 2023/05/23
Zulip
(
archive
)
Syntax error in nested records?
Lattices, Order, Abstract Interpretation
Noisy printing with name mangling light
Commands Fail and Succeed
use of bool symtry
✔ Simple question about removing duplicates from a list
Denotational semantics without excluded middle
How to simplify ?
✔ Implicit coercions for length-indexed list
Why not binary nats ?
Proof Assistants Stack Exchange
Debug autorewrite in Coq
1 answer
Tue 2023/05/30
How to prove basic lemmas about divisibility in Coq?
2 answers
Sat 2023/05/27
Rewriting with heterogeneous equality (JMeq)
1 answer
Thu 2023/05/25
Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?
1 answer
Wed 2023/05/24
Dependent sum and equality with Coq
1 answer
Mon 2023/05/22
stuck trying to prove sublist of list
1 answer
Sun 2023/05/21
How to abstract over function arity in Lean and Coq?
2 answers
Thu 2023/05/18
Organizing a Coq proof
1 answer
Thu 2023/05/18
How to deduce this equality based on the fact that these two terms must be the same?
1 answer
Thu 2023/05/18
I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq
4 answers
Wed 2023/05/17
Stack Overflow
How to teach `crush` to unfold definitions?
Fri 2023/06/02
How to parse coq statements from a coq .v file the official way?
Fri 2023/06/02
Including header / footer in a file generated by extraction
Fri 2023/06/02
Implementing variable replacement in a boolean polynomial function in Coq
1 answer
Thu 2023/06/01
Set type Variable to a concrete type inside a definition
2 answers
Mon 2023/05/29
Is there a way for Coq to recall it already proved a property for the same element in the same proof?
1 answer
Mon 2023/05/29
Replace element in Coq list
2 answers
Sat 2023/05/20
How to use a proof about a datatype within the same datatype definition in Coq?
Sat 2023/05/20
How should the excluded middle be used in the proof of the pigeonhole principle?
1 answer
Thu 2023/05/18
Importing a Module in Coq
2 answers
Tue 2023/05/16
CS Theory Stack Exchange
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
Defining functions on non-inductive types using LEM in Coq
1 answer
Fri 2022/01/21
Prove proof irrelevance in Coq?
1 answer
Fri 2021/10/29
How does axiom K contradict univalence?
2 answers
Sun 2021/09/26
Reddit
How to completely derive an Inductive Type from the set of CiC rules?
3 comments
Wed 2023/05/03
Require some help
4 comments
Tue 2023/05/02
Papers on the interactivity of Coq / Interactive Theorem Provers
5 comments
Tue 2023/04/25
Question on professionals/experts
6 comments
Sat 2023/04/08
Good ways to model subtyping
2 comments
Sun 2023/03/26
Software Foundations in Coq - Michael Ryan Clarkson
Sun 2023/03/26
Do we have a tutorial or a book which teaches coq without tactics, how to build proofs with lambdas in the CoC way?
8 comments
Thu 2023/03/23
Cannot Determine Decreasing Argument for Fix
19 comments
Thu 2023/03/09
How to prove theorems in coq in pure lambdas without tactic language?
8 comments
Fri 2023/03/03
Type Theory Forall #28 - Formally Verifying Smart Contracts using Coq, Pruvendo
Wed 2023/02/15
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
