Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [coq]

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

Filter by
Sorted by
Tagged with
48 votes
6 answers
10k 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 ...
Guy Coder's user avatar
  • 5,101
11 votes
3 answers
1k views

Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml: ...
Stéphane Gimenez's user avatar
23 votes
2 answers
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 ...
Gilles 'SO- stop being evil''s user avatar
10 votes
2 answers
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, ...
user11942's user avatar
  • 161
10 votes
1 answer
359 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-...
paulotorrens's user avatar