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

Why does Coq include let-expressions in its core language

It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v ...
Andrej Bauer's user avatar
  • 30.8k
20 votes
Accepted

Is possible to prove undecidability of the halting problem in Coq?

You're exactly right that the halting problem is an example of the second kind of "proof by contradiction" - it's really just a negative statement. Suppose ...
Tej Chajed's user avatar
19 votes

What is different between Set and Type in Coq?

Coq has 4 "big" types: Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types....
Joey Eremondi's user avatar
15 votes
Accepted

Proving tautology with coq

You cannot prove it in "vanilla" Coq, because it is based on intuitionistic logic: From a proof-theoretic perspective, intuitionistic logic is a restriction of classical logic in which the law of ...
Anton Trunov's user avatar
  • 3,479
12 votes
Accepted

Monadic Second Order Logic for Dummies

What is second order logic in contrast to first order logic? What is monadic vs non monadic logic? Monadic second-order logic is first-order logic plus quantification over sets. So, as well as ...
David Richerby's user avatar
9 votes
Accepted

What does instantiating existential variables with out of scope variable imply?

When you do an existential introduction, you are saying there is some term $t$, which is represented by the unification variable ?x, such that $P(t)\to Q$. You then ...
Derek Elkins left SE's user avatar
9 votes
Accepted

In Coq, what does it mean to have an inductive type where the right-hand side of ":" is Prop?

Inductive types are similar to Haskell's data, but they are more general. An inductive definition in Set describes a way to ...
Gilles 'SO- stop being evil''s user avatar
8 votes
Accepted

How does this use of "apply" in Coq work?

You can ask Coq to show you its proof object. Before Qed, type Show Proof. ...
Gilles 'SO- stop being evil''s user avatar
7 votes
Accepted

Proof of equality with destructuring let...in

You can destruct not only on variables, but on expressions like f n as well. So, this will get you a solution: ...
Anton Trunov's user avatar
  • 3,479
7 votes

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

I'm not an expert, but I'll share what I understood so far with an example. Let's consider the boolean type in CoC, using its standard encoding: $$ \begin{array}{l} \mathbb{B} = \Pi_{\tau:*} \tau \to ...
chi's user avatar
  • 14.6k
7 votes

What is the runtime/time complexity of Coq’s (Dependent) Type Inference?

There are actually two questions here. Is the Coq type system decidable? Long answer short, we hope so, as in it would be a bug if it were not. It is not a universal requirement for a type theory to ...
Pierre-Marie Pédrot's user avatar
6 votes

How does one know what statements in Coq require Induction?

Coq allows one to prove mathematical theorems in a completely formal way. At first, this copes with our experience of doing maths, which is far more informal. Most of the time, people doing maths are ...
chi's user avatar
  • 14.6k
6 votes
Accepted

What types are propositions?

The original conception of propositions-as-types did not distinguish propositions and types at all: all types are propositions. Under this view, we may indeed speak of different proofs of a ...
Andrej Bauer's user avatar
  • 30.8k
6 votes
Accepted

positivity condition in Coq/CIC

The positivity condition is not there just so that "programs terminate", as you put it (what programs?), but to make sure the type is well defined in the first place. The inductive definitions define ...
Andrej Bauer's user avatar
  • 30.8k
6 votes
Accepted

How CompCert "proves" different things in its codebase

I am not very sure what you are asking, and I am also not sure that you have the background to understand CompCert. It seems that you are still confused by some basic concepts in Coq. I would suggest ...
xuq01's user avatar
  • 1,190
6 votes

Proving tautology with coq

As others informed you, your tautology is not a tautology unless you assume classical logic. But since you're doing tautologies on decidable truth values, you could use ...
Andrej Bauer's user avatar
  • 30.8k
6 votes

I don't know how to prove a simple theorem used with fixpoint in Coq

You are making your life difficult by defining things in convoluted ways. Here's how a better definition of the same thing makes the proof easy. ...
Andrej Bauer's user avatar
  • 30.8k
6 votes
Accepted

Building non-classical logics in Agda & Coq

You can define many non-classical logics in Coq (and I assume Agda too), even if they are incompatible with the logic of your proof assistant, but you need to define the concept of inference yourself. ...
Ana Borges's user avatar
5 votes

Type Theory and Principia Mathematica Part IV "Relation Arithmetic"

relational databases are among the highest value, most researched applications of computer science James, what do relational databases have to do with the question? And why have you tagged this q ...
AntC's user avatar
  • 487
5 votes

Proof of equality with destructuring let...in

You could also consider a more equational proof that will avoid/encapsulate the destruction: ...
ejgallego's user avatar
  • 201
5 votes
Accepted

How to prove T Z = Z for binary representation of natural numbers in Coq

to show that bin_to_nat is the inverse of nat_to_bin I need to prove that T Z = Z No, you ...
Zimm i48's user avatar
  • 166
5 votes

How does one know what statements in Coq require Induction?

As the others have mentioned, in Coq's standard library (or typical presentations of naturals in Coq), naturals are defined inductively, usually a la Peano. We could make other choices, e.g. one could ...
Derek Elkins left SE's user avatar
4 votes
Accepted

Proving parametricity for Gallina functions

My belief has always been that you cannot prove such free theorems from within Gallina about Gallina terms, but I don't have a definite reason why. I certainly can't imagine how this proof would work, ...
Tej Chajed's user avatar
4 votes
Accepted

I don't know how to prove a simple theorem used with fixpoint in Coq

First of all, let's simplify f just a little bit, keeping the special case when it doesn't let the trailing /\ True to appear in ...
Anton Trunov's user avatar
  • 3,479
3 votes

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

Check this out! http://coq.io/opam/coq-markov.8.5.0.html. A library for Markov's inequality built on mathematical probability theory.
user48801's user avatar
  • 131
3 votes

For proof automation in Coq, when is it appropriate to use canonical structures or Equations instead of Ltac?

Choosing how to structure your development based on what proof automation you're using seems backwards. First you decide what functions and definitions you want to prove theorems about, then you ...
Jason Gross's user avatar
3 votes

How does one know what statements in Coq require Induction?

I want to share my own experience of learning Coq and theorem proving in general. Most of the time, the proof of a statement largely depends on the recursive structure of the function or operation at ...
Bubbler's user avatar
  • 406
3 votes

How does one know what statements in Coq require Induction?

To see how you can prove something about natural numbers, you must know what you know about natural numbers. Usually, we learn all sorts of 'basic facts' about numbers in high school that are pretty ...
Discrete lizard's user avatar
  • 8,248
3 votes
Accepted

Proving with co-induction principles

What likely makes it confusing is that you are doing very different things in inductive versus coinductive cases. This is somewhat alluded to by Chlipala's reference to "infinite proofs"1. (Another ...
Derek Elkins left SE's user avatar
3 votes
Accepted

When can the coinduction hypothesis be used?

First, let me recall least and greatest fixed points for $\subseteq$. We are working relative to some set $U$, the universe. In the case of (co)inductive definitions, $U$ is the set of all terms. A ...
kne's user avatar
  • 2,254

Only top scored, non community-wiki answers of a minimum length are eligible