Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Subtyping variance of dependent product types
1 answer
Tue 2024/10/29
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
Coq eats expression parentheses
10 answers
Tue 2024/10/08
Why do we need supplemental standard libraries?
7 answers
Mon 2024/10/07
Proofchat: A TCP client/server chat application written in Coq
10 answers
Thu 2024/10/03
[Postdoc position] Machine Learning for translation between formal mathematics libraries (2nd announcement)
Thu 2024/10/03
The Coq Club mailing list
Call for Papers - Special Issue of JLAMP on Recent Advances on Unification
Mon 2024/10/28
Call for STSMs and ITC conference grants, deadline 24 November 2024
Mon 2024/10/28
Postdoc in Type Theory/Logic, Stockholm Univ. (deadline 4 Nov)
Fri 2024/10/25
PriSC @ POPL'25: 2nd Call for Paper
Mon 2024/10/21
FSCD 2025: Call for Workshop Proposals
Mon 2024/10/21
FSCD 2025: First Call for Papers
Fri 2024/10/18
POPL 2025 Call for Tutorials (deadline extended: Oct 25th, 2024)
Thu 2024/10/17
[TFP 2025 2nd Call for Papers] 25th International Symposium on Trends in Functional Programming (Oxford, UK)
Fri 2024/10/11
1st CfP: SLE 2025 - 18th ACM SIGPLAN International Conference on Software Language Engineering
Thu 2024/10/10
Assistant Professor (Tenure Track) position at ETH Zurich
Wed 2024/10/09
Zulip
(
archive
)
Reduction with compute but not with vm_compute
✔ Doubt with contradiction on subgoal
Subgoals with an arbitrary Prop (`H -> G \/ ~H -> G`)
✔ Infer term type from Definition type
Pain points about sections
string encoding
Printing a string without escaped characters
Extensible automations that *don't* solve the goal?
Existential clause on records
How to find input breaking test?
Proof Assistants Stack Exchange
Axiom of Countable Choice in COQ
1 answer
Mon 2024/10/28
I need help with min problem
1 answer
Thu 2024/10/24
How does Coq guess `i` is decreasing?
2 answers
Tue 2024/10/22
Skolem functions in COQ
2 answers
Mon 2024/10/21
Principle like UIP on Types with Decidable Equality but for Inequality Proofs
1 answer
Sun 2024/10/20
How does the case (destruct) tactic change the goal?
1 answer
Wed 2024/10/16
About the use of command Canonical in Coq for mantaining Record Type information
1 answer
Mon 2024/10/14
How can I generate equalities from an application in Coq?
1 answer
Sat 2024/10/12
Natural deduction in coq: implication introduction
1 answer
Thu 2024/10/03
Inconsistency Principle in Coq
3 answers
Sat 2024/09/21
Stack Overflow
Pigeonhole proof without decidable equality or excluded middle
3 answers
Mon 2024/10/28
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
Proving non-linear equations and inequalities involving rational numbers in Coq
1 answer
Wed 2024/09/18
Ltac for deterministic rewriting/sorting of operands
1 answer
Wed 2024/09/18
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