Questions tagged [coq]
Coq is a formal proof management system, semi-interactive theorem prover and functional programming language. Coq is used for software verification, the formalization of programming languages, the formalization of mathematical theorems, teaching, and more. Due to the interactive nature of Coq, we recommend questions to link to executable examples at https://x80.org/collacoq/ if deemed appropriate.
2,953
questions
98
votes
3
answers
18k
views
What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq?
Does Isabelle/HOL proof assistant have any weaknesses and strengths compared to Coq?
- 1,013
80
votes
1
answer
2k
views
Why is my definition not allowed because of strict positivity?
I have the following two definitions that result in two different error messages.
The first definition is declined because of strict positivity and the second one because of a universe inconsistency.
(...
- 1,480
73
votes
4
answers
12k
views
What are the practical limitations of a non-turing complete language like Coq?
As there are non-Turing complete languages out there, and given I didn't study Comp Sci at university, could someone explain something that a Turing-incomplete language (like Coq) cannot do?
Or is ...
- 134k
48
votes
1
answer
7k
views
Difference between Z3 and coq
I am wondering if someone can tell me the difference between Z3 and coq? Seems to me that coq is a proof assistant in that it requires the user to fill in the proof steps, whereas Z3 does not have ...
- 6,122
45
votes
2
answers
2k
views
How do we overcome the compile time and runtime gap when programming in a Dependently Typed Language?
I'm told that in dependent type system, "types" and "values" is mixed, and we can treat both of them as "terms" instead.
But there is something I can't understand: in a strongly typed programming ...
- 3,775
44
votes
2
answers
5k
views
Difference between type parameters and indices?
I am new to dependent types and am confused about the difference between the two. It seems people usually say a type is parameterized by another type and indexed by some value. But isn't there no ...
- 1,234
33
votes
1
answer
10k
views
Differences between Coq and Agda
What are each of these programs designed for and what does each offer other the other? Also, are both systems consistent, and moreover, are they based on some foundational mathematical theory?
Two ...
- 9,756
31
votes
0
answers
401
views
Compatibility of impredicative Set and function extensionality
The Coq FAQ says that function extensionality is consistent with predicative Set. It's not fully clear to me from this whether it's consistent with impredicative Set (or maybe the consistency is ...
- 30k
30
votes
4
answers
9k
views
What does `true = false` mean in Coq?
[I am not sure this is appropriate for stack overflow, but there are many other Coq questions here so perhaps someone can help.]
I am working through the following from http://www.cis.upenn.edu/~...
- 46.6k
29
votes
2
answers
5k
views
Can I extract a Coq proof as a Haskell function?
Ever since I learned a little bit of Coq I wanted to learn to write a Coq proof of the so-called division algorithm that is actually a logical proposition: forall n m : nat, exists q : nat, exists r : ...
- 4,806
28
votes
2
answers
2k
views
Why haven't newer dependently typed languages adopted SSReflect's approach?
There are two conventions I've found in Coq's SSReflect extension that seem particularly useful but which I haven't seen widely adopted in newer dependently-typed languages (Lean, Agda, Idris).
...
- 4,382
26
votes
1
answer
6k
views
Introduce previously proved theorem as hypothesis
Suppose that I have already proved some theorem in coq, and later I want to introduce it as a hypothesis in the proof of another theorem. Is there a succinct way to do this?
The need for this ...
- 10.9k
26
votes
1
answer
1k
views
On representations of permutations
I would like to have an inductive type to describe permutations and their action on some containers. It is clear that depending on the description of this type the definition complexity (in terms of ...
- 686
26
votes
2
answers
935
views
Converting Coq term in AST form to polish notation using Python
Say I have an arbitrary Coq Term (in AST format using s-expressions/sexp) for example:
n = n + n
and I want to automatically convert it to:
= n + n n
by traversing the AST tree (which is simple a ...
- 5,961
25
votes
3
answers
5k
views
Can Coq be used (easily) as a model checker?
As the title says, can Coq be used as a model checker? Can I mix model checking with Coq proving? Is this usual? Google talks about a "µ-calculus", does anyone have experience with this or something ...
- 3,916