Stack Overflow
Stack Overflow

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.

Coq is an interactive theorem prover based on the calculus of inductive constructions.

Resources

2862 questions
94
votes
3 answers

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?
elysefaulkner
  • 973
  • 2
  • 8
  • 8
80
votes
1 answer

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. (* non-strictly positive *) Inductive SwitchNSP…
ichistmeinname
  • 1,480
  • 10
  • 19
70
votes
4 answers

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 the completeness/incompleteness of no real practical…
oxbow_lakes
  • 133,303
  • 56
  • 317
  • 449
47
votes
1 answer

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 that requirement. But seems like coq also has auto…
JRR
  • 6,014
  • 6
  • 39
  • 59
45
votes
2 answers

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 language without Dependent Type (like Haskell), Types…
luochen1990
  • 3,689
  • 1
  • 22
  • 37
41
votes
2 answers

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 distinction between types and terms in a dependently…
Alex
  • 1,184
  • 7
  • 15
33
votes
1 answer

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 things I care about: Easy to install Easy to…
Cristian Garcia
  • 9,630
  • 6
  • 54
  • 75
30
votes
4 answers

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/~bcpierce/sf/Basics.html#lab28 (just below where Case…
andrew cooke
  • 45,717
  • 10
  • 93
  • 143
30
votes
0 answers

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 unknown in that case).
András Kovács
  • 29,931
  • 3
  • 53
  • 99
28
votes
2 answers

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). Firstly, where possible predicates are expressed as…
LogicChains
  • 4,332
  • 2
  • 18
  • 27
28
votes
2 answers

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 : nat, n = q * m + r I recently accomplished that…
minopret
  • 4,726
  • 21
  • 34
26
votes
2 answers

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 nested list of lists because of the sexp). Is there a…
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
26
votes
1 answer

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 its length) of algorithms (computing composition…
Katty J.
  • 686
  • 4
  • 11
25
votes
3 answers

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 similar? Is it advised to use Coq in this way, or…
Olle Härstedt
  • 3,799
  • 1
  • 24
  • 57
25
votes
1 answer

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 typically arises for me when I want to do something like…
Juan A. Navarro
  • 10,595
  • 6
  • 48
  • 52
1
2 3
…
99 100