Planet Coq

Link aggregator of discussions about the Coq interactive theorem prover

Discourse

Print Module [Type] lacks types
Sun 2022/08/14
Is there a solution for the problematic induction hypotheses generated using eqn:H?
9 answers
Fri 2022/08/12
Speed of Program Instance
Fri 2022/08/12
Choosing between SProp and axiomatic proof irrelevance
9 answers
Thu 2022/08/11
"Correct" way to structure modules
2 answers
Tue 2022/08/09
Coq Community Survey 2022 Results: Part II
Wed 2022/08/03
The reference omega was not found in the current environment
2 answers
Mon 2022/08/01
Is it possible to suppose the falsity of the goal and prove False in Coq?
5 answers
Thu 2022/07/28
Reusing values from inductive relation
2 answers
Sun 2022/07/24
Print the curried version of a function (i.e. explicitly printing the functions as an explicit chain)
2 answers
Sat 2022/07/23

The Coq Club mailing list

Dual of Well Founded Induction in CoInductive World
Sun 2022/08/14
PhD student in Computing Science on the topic of efficient and provably correct execution environments
Fri 2022/08/05
Simplifying pattern matching
6 replies
Fri 2022/08/05
Call for participation: EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs
Thu 2022/08/04
recompiling coq libraries on recompiling coq
Sun 2022/07/31
13th International School on Rewriting (ISR 2022), September 19-24, 2022, Tbilisi, Georgia - Registration Open
Sun 2022/07/31
Registration open: ICTAC autumn school, September 26-30, Tbilisi, Georgia
Sun 2022/07/31
PhD and Postdoctoral positions in Formal Methods for AI
Sun 2022/07/31
Call for Participation -- Mathematics of Program Construction 2022
Tue 2022/07/26
New lecture in FME Teaching Tutorials series on July 29, at 3 pm CEST: Prof. Erika Abraham (RWTH Aachen University, Germany) on "Automatic exercise generation for satisfiability checking"
Thu 2022/07/21

Zulip (archive)

Proof Assistants Stack Exchange

Learning Math Proof via Proof Assistants
2 answers
Sat 2022/08/13
Can I prove this axiom without using excluded-middle property?
1 answer
Thu 2022/08/11
When I destruct record, can I make a hypothesis name without 0?
2 answers
Wed 2022/08/10
Is there a tactic in Coq to make a hypothesis from applying two hypotheses?
2 answers
Mon 2022/08/08
Coq: can `tauto` be used to prove classical tautologies?
Sun 2022/08/07
Non-dependent implicit argument instantiation in Coq's reference manual does not work
1 answer
Thu 2022/08/04
A problem similar to intermediate value problem
1 answer
Wed 2022/08/03
How can I prove this theorem with induction in Coq?
4 answers
Wed 2022/08/03
Unexpected eta expansion in constant definition
Tue 2022/08/02
Define a function using another function
1 answer
Tue 2022/08/02

Stack Overflow

Get stuck at the `MStarApp` case of Software Fundation's pumping Lemma
Thu 2022/08/11
How to use a definition in Coq?
2 answers
Tue 2022/08/09
What is the best practice for installing external dependencies in a Coq project?
1 answer
Mon 2022/08/08
Prove equality with eq_rect without UIP
1 answer
Mon 2022/08/08
How does one access the dependent type unification algorithm from Coq's internals -- especially the one from apply and the substitution solution?
1 answer
Sat 2022/07/30
I have been stuck on MApp for pumping lemma
1 answer
Fri 2022/07/29
Holding greater or equal relation between two terms
Fri 2022/07/29
Coq: Simpl in match pattern when having an inequality hypothesis
1 answer
Thu 2022/07/28
Coq: rewriting under a pointwise_relation
1 answer
Thu 2022/07/28
How does one compute/create a concrete/actual string in coq to pass to functions or store in a variable/identifier?
3 answers
Wed 2022/07/27

CS Theory Stack Exchange

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
Does the order of declarations in an inductive type matter?
3 answers
Sat 2021/09/25
How would I go about learning the underlying theory of the Coq proof assistant?
4 answers
Wed 2021/08/18
Why does Coq have Prop?
4 answers
Fri 2021/04/09
Dependent eliminator for empty type in intensional Martin-Löf type theory
1 answer
Sun 2021/03/28
Defining inductive types in intensional type theory purely in terms of type-theoretic data
1 answer
Fri 2021/03/19
Impredicativity + large eliminations (with no excluded middle) in Coq
1 answer
Thu 2021/03/04

Reddit

How does one access the dependent type unification algorithm from Coq's internals -- especially the one from apply and the substitution solution?
1 comment
Fri 2022/07/15
Type Theory Forall Podcast - Experience Report Learning Coq
Sat 2022/06/04
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
3 comments
Mon 2022/05/30
The reference info was not found in the current environment.
2 comments
Thu 2022/05/19
Coq make failing on Omega
2 comments
Thu 2022/05/19
Type Theory Forall Episode #17 The Lost Elegance of Computation - Conal Elliott
Tue 2022/05/10
Hey, at risk of making a tired question, I could use a little help with something that I'm finding myself stuck on as an of-two-days proof assistant and Coq user. ∀x : ℕ, 3 | (x + 5x). Specifically, what's got me is showing that ∀x y z : ℕ, (z|x and z|y) -> z|(x + y). Attempt in post body.
8 comments
Mon 2022/05/09
Got stuck in proving the malloc/free example
Sat 2022/05/07
Adding a Field
1 comment
Wed 2022/04/27
Coq Hexadecimal Addition
1 comment
Tue 2022/04/19

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