Questions tagged [coq]
Coq is an interactive theorem prover.
59
questions
10
votes
3
answers
407
views
Does the order of declarations in an inductive type matter?
I was wondering if the order of declarations of an inductive type can matter.
For example in Coq you can define Nat either by:
...
17
votes
3
answers
1k
views
What is the role of predicativity in inductive definitions in type theory?
We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A :...
- 175
44
votes
4
answers
4k
views
How would I go about learning the underlying theory of the Coq proof assistant?
I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
user788
23
votes
1
answer
4k
views
Prove proof irrelevance in Coq?
Is there a way to prove the following theorem in Coq?
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
EDIT: An attempt to give a brief ...
- 2,745
23
votes
1
answer
2k
views
Where is the proof that Coq + Excluded Middle is consistent
I've seen (and heard) it claimed that it is safe to add the classical axiom of excluded middle to Coq, but I can not seem to find a paper supporting this claim. The papers I see listed on the Coq wiki ...
- 1,670
2
votes
2
answers
272
views
formalizing a statement about the expressive power of programming languages wrt divergence
In the Coq'Art book the authors mention in passing that any language that can calculate all computable functions must also be able to express diverging computations.
Or in other words, there can be no ...
- 123
14
votes
1
answer
5k
views
How to define a function inductively on two arguments in Coq?
How can I convince Coq that the recursive function given below terminates?
The function takes two inductive arguments.
Intuitively, the recursion terminates because either argument is decomposed.
...
- 953
52
votes
3
answers
6k
views
Shallow versus Deep Embeddings
When encoding a logic into a proof assistant such as Coq or Isabelle, a choice needs to be made between using a shallow and a deep embedding. In a shallow embedding logical formulas are written ...
- 16.6k
15
votes
2
answers
1k
views
Eliminating cofix in Coq proof
While trying to prove some basic properties using coinductive types in Coq, I keep running into the following problem and I cannot get around it. I've distilled the problem into a simple Coq script as ...
- 16.6k