Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
11
questions
24
votes
4
answers
532
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 ...
- 1,881
34
votes
2
answers
733
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 ...
- 593
4
votes
1
answer
105
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,477
28
votes
2
answers
561
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 ...
- 381
18
votes
1
answer
135
views
When to use coinductive types?
One could define streams in the following manner
...
12
votes
2
answers
168
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 ...
- 354
16
votes
1
answer
230
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 ...
- 165
13
votes
2
answers
198
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
...
- 1,662
10
votes
1
answer
105
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)?
- 201
4
votes
1
answer
95
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
91
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,477