# Questions tagged [coq]

Coq is an interactive theorem prover based on the Calculus of Inductive Constructions.

62 questions
Filter by
Sorted by
Tagged with
145 views

### Coq: default values for vectors

Let's say there is a vector of length $n$: Require Import Vector. Variable T:Type. Variable n:nat. Variable v:t T n. "list" gives a function "nth" that demands a ...
365 views

### Coq — non-terminating programs [duplicate]

People usually say Coq does not allow writing non-terminating functions. I have a question regarding that. Does Coq allow writing exactly all terminating functions? In other words, what are the ...
96 views

### Representing inductive types

I implemented dependently typed lambda calculus in the spirit of this article: http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf The calculus, works and I experimented with it and like it. However, I ...
390 views

### Has Anyone Actually Created a System that Writes Computer Programs from specification?

Has anyone ever actually written a system (software or detailed explanation on paper with simple examples) that generates computer programs? I input $Prime(x) \wedge x<10$ and it creates a program ...
143 views

### Is this a well founded inductive type? Can I express this in Coq?

the standard List type in Coq can be expressed as: Inductive List (A:Set) : Set := nil : List A | cons : A -> List A -> List A. as I understand, W-type ...
1k views

### Euclidean Algorithm in Coq

Question How do I write more intuitive proofs of the two following results in Coq? ...
2k views

### Theorem Proofs in Coq

Background I am learning assistance, Coq, on my own. So far, I have completed reading Yves Bertot's Coq in a Hurry. Now, my goal is to prove some basic results concerning the natural numbers, ...
1k views

### What is the difference between “definition” and “inductive” in Coq?

In Coq, you can use two different kinds of keywords to do definitions--Inductive and Definition. I do not understand the difference between an inductive and a definition, or when it is appropriate to ...
1k views

### Does there exist any work on creating a Real Number/Probability Theory Framework in COQ?

COQ is an interactive theorem prover that uses the calculus of inductive constructions, i.e. it relies heavily on inductive types. Using those, discrete structures like natural numbers, rational ...
885 views

### Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml: ...