Questions tagged [coq]

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

Filter by
Sorted by
Tagged with
0
votes
0answers
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 ...
4
votes
2answers
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 ...
1
vote
0answers
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 ...
17
votes
4answers
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 ...
3
votes
1answer
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 ...
5
votes
1answer
1k views

Euclidean Algorithm in Coq

Question How do I write more intuitive proofs of the two following results in Coq? ...
10
votes
2answers
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, ...
5
votes
1answer
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 ...
8
votes
2answers
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 ...
11
votes
3answers
885 views

Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml: ...
46
votes
6answers
9k views

Learning Automated Theorem Proving

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Note that these topics are not easily digested ...
22
votes
2answers
3k views

Recursive definitions over an inductive type with nested components

Consider an inductive type which has some recursive occurrences in a nested, but strictly positive location. For example, trees with finite branching with nodes using a generic list data structure to ...

1
2