Questions tagged [coq]

Coq is a formal proof management system. It is often referred to as a proof assistant.

Filter by
Sorted by
Tagged with
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 ...
Meven Lennon-Bertrand's user avatar
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 ...
Ricky's user avatar
  • 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 ...
palmskog's user avatar
  • 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 ...
Greg Nisbet's user avatar
  • 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 ...
Blaisorblade's user avatar
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 ...
setholopolus's user avatar
18 votes
1 answer
265 views

When to use coinductive types?

One could define streams in the following manner ...
Agnishom Chattopadhyay's user avatar
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 ...
Couchy's user avatar
  • 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)?
Laurel's user avatar
  • 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 ...
with-forest's user avatar
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 ...
Charlie Parker's user avatar
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 ...
Charlie Parker's user avatar
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? ...
lyfeng's user avatar
  • 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 (...
Greg Nisbet's user avatar
  • 2,711