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
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
18 votes
1 answer
135 views

When to use coinductive types?

One could define streams in the following manner ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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)?
user avatar
  • 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? ...
user avatar
  • 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 (...
user avatar
  • 2,477