Share Your Experience: Take the 2024 Developer Survey

# Tag Info

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 ...
• 30.8k
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 ...
• 371

### 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....
• 29.8k
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 ...
• 3,479
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 ...
• 81.8k
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 ...
• 12.1k
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 ...
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. ...
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: ...
• 3,479

### 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 ...
• 14.6k

### 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 ...

### 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 ...
• 14.6k
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 ...
• 30.8k
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 ...
• 30.8k
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 ...
• 1,190

### 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 ...
• 30.8k

### 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. ...
• 30.8k
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. ...
• 176

### 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 ...
• 487

### Proof of equality with destructuring let...in

You could also consider a more equational proof that will avoid/encapsulate the destruction: ...
• 201
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 ...
• 166

### 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 ...
• 12.1k
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, ...
• 371
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 ...
• 3,479

### 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.
• 131

### 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 ...
• 137

### 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 ...
• 406

### 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 ...
• 8,248
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 ...
• 12.1k
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 ...