Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Rocq Sharing Analyser (new plugin to print debug info)
Tue 2024/11/05
Release of Iris 3.4 and std++ 1.11
Thu 2024/10/31
Inference of match "return" clause vs. if
3 answers
Thu 2024/10/31
Subtyping variance of dependent product types
2 answers
Wed 2024/10/30
Allowing large elimination
6 answers
Tue 2024/10/29
[Coq Platform release] 2024.10.0 with Coq 8.19.2
Mon 2024/10/28
Assistance Getting Rid of Superfluous Universe levels?
4 answers
Wed 2024/10/23
Is there a public roadmap for the Rocq rename?
3 answers
Fri 2024/10/11
How to wrap bullets within a tactic?
6 answers
Tue 2024/10/08
Why do we need supplemental standard libraries?
7 answers
Mon 2024/10/07
The Coq Club mailing list
POPL 2025 Call for Participation - Early registration: 20 December
Wed 2024/11/20
Tenure-track Openings at Max Planck Institutes in Computer Science
Mon 2024/11/18
PhD and postdoc positions in type theory (start: Oct 2025; location: Nottingham, UK)
Fri 2024/11/15
Final Call for Papers: FORMALISE 2025 - EXTENDED DEADLINES
Tue 2024/11/12
POPL25 Student Volunteers: deadline extension
Tue 2024/11/12
PLDI 2025: Tutorial proposals due Nov 14/24
Fri 2024/11/08
[POPL25] Reminder: Call for student volunteers
Thu 2024/11/07
POPL 2025 Student Research Competition Call for Submissions
1 reply
Thu 2024/11/07
Termination checker rejecting equivalent functions
1 reply
Wed 2024/11/06
PriSC @ POPL'25: Extended deadline
Tue 2024/11/05
Zulip
(
archive
)
Confusing setoid_rewrite successes and failures
Building a list of automation tactics
has_ext tt |-- emp
Forcing resolution of implicit arguments in Eval
Right induction on transitive closure
ring_simplify not reducing "0 = 0 * x" or "0 = x * 0"
Is it possible to prove free theorems?
Impossible to destruct an inductive
functional extensionality in a polymorphic theorem
✔ Type checking fills in wrong implicit value
Proof Assistants Stack Exchange
Coq proving special cases of the law of the exlcuded middle: equalities on inductive types
2 answers
Wed 2024/11/20
Can I in Coq define a recursive function with a notation such that the recursive calls can use it?
1 answer
Wed 2024/11/20
How to target an introduced value set with the set tactic for induction in Coq?
3 answers
Mon 2024/11/18
Deduction theorem in coq
2 answers
Mon 2024/11/18
How does the case (destruct) tactic change the goal?
1 answer
Fri 2024/11/15
atomic tactics : restore previous state if tactic didn't solve the current goal in Coq
2 answers
Thu 2024/11/14
Conclude from 2 * m = 3 * n, that n is divisible by 2
5 answers
Thu 2024/11/14
Tactic proof of even induction
1 answer
Thu 2024/11/14
Prove that a set of formulas proves itself
1 answer
Thu 2024/11/14
Axiom of Choice in COQ
1 answer
Tue 2024/11/12
Stack Overflow
Coq using lemma itself for proof
1 answer
Sun 2024/11/17
How to prove sequential commands C1; C2 can always execute to C2 if we know C1 always terminates?
1 answer
Thu 2024/11/14
Why does Coq solve_in_Union tactic fail directly but works through assertion of identical goal?
1 answer
Wed 2024/10/30
How to prove existence in COQ?
1 answer
Tue 2024/10/15
How to prove if a list `n::l` is an in-order merge of 2 lists `n::l1` `l2`, then `l` is an in-order merge of `l1` and `l2` in Coq?
Wed 2024/10/09
How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))?
2 answers
Sat 2024/10/05
How to return the correct dependent type?
1 answer
Fri 2024/10/04
How to use the rewrite tactic in function arguments
1 answer
Tue 2024/10/01
Lemma cannot be used as a hint
2 answers
Tue 2024/09/24
Unfolding an opaque fixpoint in Coq
2 answers
Fri 2024/09/20
CS Theory Stack Exchange
Finite sets in Coq
1 answer
Thu 2024/10/03
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
Reddit
What are the dangers of using Hilbert's epsilon operator?
2 comments
Fri 2024/09/06
What is a good community for beginner questions?
3 comments
Fri 2024/09/06
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
