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 ...
- 31.2k
20
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....
- 30.1k
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 ...
- 371
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 ...
- 3,499
13
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 ...
- 82.2k
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 ...
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 ...
- 12.1k
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.
...
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 ...
- 14.7k
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 ...
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 ...
- 1,190
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 ...
- 31.2k
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.
...
- 31.2k
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 ...
- 31.2k
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 ...
- 14.7k
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 ...
- 31.2k
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. ...
- 176
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 ...
- 12.1k
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 ...
- 166
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 ...
- 507
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, ...
- 371
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 ...
- 3,499
4
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 ...
- 2,328
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.
- 131
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 ...
- 12.1k
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 ...
- 137
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 ...
- 508
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 ...
- 8,332
3
votes
Accepted
on coq: Why is the proof complete after proving only for one induction when we have more than one variable?
You do not have to prove things by induction. For example, you can prove $\forall n : \mathbb{N} \,.\, n = n$ without induction by applying reflexivity. In your proof, we use induction on $a$, but ...
- 31.2k
2
votes
Understanding the definition of Positivity Constraints in Coq
Take $l = k = 0$, the matrix of $b_{ij}$'s has size $0 \times 0$, hence we do not have to defined any $b_{ij}$, and take $g = \mathbf{nat}$.
- 31.2k
Only top scored, non community-wiki answers of a minimum length are eligible