Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
[Postdoc position] Machine Learning for translation between formal mathematics libraries
1 answer
Fri 2024/06/14
Proving obvious logic
1 answer
Tue 2024/06/11
Coq 8.19.2
Mon 2024/06/10
Learning to write Coq plugins - what is the purpose of .mlg files?
5 answers
Fri 2024/06/07
Making use of a definition inside a proof
4 answers
Wed 2024/06/05
Old Critical Bug described as affecting virtual machine but also triggers on other conversion machines
4 answers
Wed 2024/06/05
Rewrite variable value in hypothesis
1 answer
Mon 2024/06/03
Idea for a collaborative Coq
6 answers
Sat 2024/06/01
[ANN] coq-lsp 0.1.9
Fri 2024/05/31
Polymorphic seq
1 answer
Fri 2024/05/24
The Coq Club mailing list
Postdoc position Machine Learning translation between formal math libraries
Fri 2024/06/14
ITP 2024 Call for Participation (September 9-14 2024, Tbilisi, Georgia)
Thu 2024/06/13
POPL 2025: Call for Workshops and Co-located Events
Thu 2024/06/13
[Second Call for Papers] Formal Verification of Physical Systems (FVPS-2024) Extended Deadline: June 16, 2024
Wed 2024/06/12
Coq 8.19.2
Mon 2024/06/10
Second Call for Submissions to the Doctoral Program - 17th Conference on Intelligent Computer Mathematics - CICM 2024 - Extended Deadline: June 20, 2024
Mon 2024/06/10
[Second Call for Papers] Women in Formal Methods (WiFM-2024)
Mon 2024/06/10
18th International Conference on Reachability Problems - RP'24
Sat 2024/06/08
19th International Conference on Integrated Formal Methods - iFM 2024
Sat 2024/06/08
Call for Papers: SPLASH 2024 Student Research Competition
Fri 2024/06/07
Zulip
(
archive
)
Predicative Prop
Limitations of Modules
List all identifiers defined in Coq files
Mutually recursive indexed inductive definition
simpl, no (visual) effect; reflexivity, no more goals (???)
Default tactic when creating a type
✔ Inductive type with lists
Cumulativity Weak Constraints
Question on subterms matching [Very Basic]
Obligations of fails
Proof Assistants Stack Exchange
Lower bounds in type theory proof assistant with ordinals and universes without axioms
Fri 2024/06/14
Coq equivalent of Lean's `nth_rewrite`
Fri 2024/06/14
Using if-then-else in Program Definition's obligation
1 answer
Thu 2024/06/13
Coq cannot `simple apply reflexivity` in custom tactic
1 answer
Thu 2024/06/13
Proof General tell Coq where a physical path is
1 answer
Wed 2024/06/12
Intuitive understanding of limits of `intuition` tactic in Coq
Wed 2024/06/12
Problems with dependent sums
1 answer
Tue 2024/06/11
Changing workflow from coq_makefile to Dune, unable to view built project in a toplevel
1 answer
Mon 2024/06/10
Equivalence Relations COQ
1 answer
Mon 2024/06/10
Tools like leanblueprint for other proof assistants, especially Coq?
3 answers
Mon 2024/06/10
Stack Overflow
Frama-C with Coq interactive prover
Fri 2024/06/14
How to use lambda functions in COQ
1 answer
Fri 2024/06/14
Is there a lightweight way to define a mutable dictionary that can return all of its keys in Coq?
2 answers
Wed 2024/06/12
How to match implication without prior intros?
Mon 2024/06/10
How can I prove that theorem in coq: (x | a) -> (x | b) -> x <= (gcd a b)?
2 answers
Sat 2024/06/08
Constructing proof terms inside a recursive function
1 answer
Fri 2024/06/07
Coq notation defined inside a module expecting type without module prefix
1 answer
Tue 2024/06/04
How does one implement Coq?
1 answer
Thu 2024/05/30
Beta-reduction after delta-reduction in unfold tactic
1 answer
Mon 2024/05/27
Convert list to vector in coq
2 answers
Sun 2024/05/26
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
Coq, NixOS setup
Wed 2024/05/29
Required Formal Logic Books for Coq?
4 comments
Thu 2024/05/23
Required Functional Programming Experience Before Learning Coq?
24 comments
Sun 2024/05/19
Required Math for Coq?
10 comments
Sun 2024/05/19
Help with inversion over equivalence relations.
5 comments
Thu 2024/05/02
Making Coq more readable
11 comments
Thu 2024/05/02
I have an exam soon and this is a example of a task, is there a easy way to do this, like i heard people solve this kind of task with tauto?
1 comment
Sun 2024/04/21
Classes in Coq
2 comments
Mon 2024/04/15
Defining Operational Semantics of Loops in Coq?
Sun 2024/04/07
Help: Constructing Theorem
6 comments
Sun 2024/03/17
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