Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
14
questions
25
votes
4
answers
1k
views
What are the differences between MLTT and CIC?
In the theory and design of proof assistants based upon dependent types, I feel like there’s a somewhat cultural divide between the "MLTT" world (with Agda as the main representative proof ...
- 4,098
58
votes
2
answers
5k
views
What are the main differences between Coq and Lean?
Coq and Lean are two of the most common proof assistants out there (but the question of course applies to other proof assistants too).
What are the main differences between Coq and Lean? Ideally it ...
- 898
22
votes
1
answer
754
views
What is the state of coinductive types and reasoning in Coq?
Ever since the work by Gimenez for his PhD thesis, Coq has supported positive coinductive types. For example, the type of always-infinite streams containing elements of type ...
- 385
5
votes
1
answer
142
views
How to implement first-order relational structures in Coq?
I'm trying to define a first-order relational structure in Coq.
I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough.
I also have a ...
- 2,711
16
votes
2
answers
343
views
What are the upsides and downsides of typed vs untyped conversion?
What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"?
Background
Generally speaking, in dependent type ...
- 394
40
votes
3
answers
2k
views
What exactly is setoid hell?
One of the only arguments I've heard about why Lean is better than Coq is that you can construct quotients of built-in structures by default. (In Coq, you apparently have to use Setoids instead of ...
- 501
18
votes
1
answer
265
views
13
votes
2
answers
365
views
Is eta-equality provable in Coq?
Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove
...
- 2,161
11
votes
1
answer
145
views
What are the differences between jsCoq and the versions of Coq that can be downloaded?
I found a site where I can use Coq in my browser: jsCoq Interactive Online System. Are there any major differences between the experience I'm getting on this site and the downloadable version(s)?
- 213
7
votes
2
answers
1k
views
Is it possible to make a proof assistant program based on ZFC?
I heard that many proof assistant programs are made based on the type theory.
For me, as a mathematician, when I met Coq at first, it is difficult to accustomed with it.
So I have a question.
Is it ...
- 357
6
votes
0
answers
170
views
How does one systematically traverse OCaml representations of Coq ASTs terms?
I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language).
My main challenge is to figure out how to do this systematically because I ...
- 199
6
votes
0
answers
72
views
What are Generic Arguments in Coq and how are they structured in their OCaml code?
I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
- 199
4
votes
1
answer
120
views
How can I prove has_esp when using mathcomp.analysis?
How can I prove the following goal (which I believe to be true) using mathcomp.analysis?
...
- 157
3
votes
1
answer
145
views
List of general purpose Coq sublanguages for defining custom tactics
I've been tweaking the Coq plugin template recently to try to get a feel for writing custom Coq tactics in OCaml.
It's tricky. You need to define an .mlg file (...
- 2,711