People who code: we want your input. Take the Survey

Questions tagged [coq]

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

Filter by
Sorted by
Tagged with
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 ...
11
votes
3answers
885 views

Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml: ...
10
votes
1answer
294 views

Why are recursive types needed as primitives for proofs in dependent type systems?

I'm relatively new to type theory and dependent programming. I've been studying the calculus of constructions (CoC) and other pure type systems. I'm particularly interested in using it as a proof-...
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, ...
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 ...