# Why does Coq have Prop?

Coq has a type Prop of proof irrelevant propositions which are discarded during extraction. What are the reason for having this if we use Coq only for proofs. Prop is impredicative, so Prop : Prop, however, Coq automatically infers universe indexes and we can use Type(i) instead everywhere. It seems Prop complicates everything a lot.

I read that there're philosophical reasons for separating Set and Prop in Luo's book, however, I didn't find them in the book. What are they?

-
“if we use Coq only for proofs”: I think you've identified a key point here. Coq isn't used only for proofs. – Gilles Mar 31 '14 at 14:48

$\mathtt{Prop}$ is very useful for program extraction because it allows us to delete parts of code that are useless. For example, to extract a sorting algorithm we would prove the statement "for every list $\ell$ there is a list $k$ such that $k$ is ordered and $k$ is a permutatiom of $\ell$". If we write this down in Coq and extract without using $\mathtt{Prop}$, we will get:

1. "for all $\ell$ there is $k$" will give us a map sort which takes lists to lists,
2. "such that $k$ is ordered" will give a funciton verify which runs through $k$ and checks that it is sorted, and
3. "$k$ is a permutation of $\ell$" will give a permutation pi which takes $\ell$ to $k$. Note that pi is not just a mapping, but also the inverse mapping together with programs verifying that the two maps really are inverses.

While the extra stuff is not totally useless, in many applications we want to get rid of it and keep just sort. This can be accomplished if we use $\mathtt{Prop}$ to state "$k$ is ordered" and "$k$ is a permutation of $\ell$", but not "for all $\ell$ there is $k$".

In general, a common way to extract code is to consider a statement of the form $\forall x : A \,.\, \exists y : B \,.\, \phi(x, y)$ where $x$ is input, $y$ is output, and $\phi(x,y)$ explains what it means for $y$ to be a correct output. (In the above example $A$ and $B$ are the types of lists and $\phi(\ell, k)$ is "$k$ is ordered and $k$ is a permutation of $\ell$.") If $\phi$ is in $\mathtt{Prop}$ then extraction gives a map $f : A \to B$ such that $\phi(x, f(x))$ holds for all $x \in A$. If $\phi$ is in $\mathtt{Set}$ then we also get a function $g$ such that $g(x)$ is the proof that $\phi(x, f(x))$ holds, for all $x \in A$. Often the proof is computationally useless and we prefer to get rid of it, especially when it is nested deeply inside some other statement. $\mathtt{Prop}$ gives us the possibility to do so.

Added 2015-07-29: There is a question whether we could avoid $\mathsf{Prop}$ altogether by automatically optimizing away "useless extracted code". To some extent we can do that, for instance all code extracted from the negative fragment of logic (stuff built from the empty type, unit type, products) is useless as it just shuffles around the unit. But there are genuine design decisions one has to make when using $\mathsf{Prop}$. Here is a simpe example, where $\Sigma$ means that we are in $\mathsf{Type}$ and $\exists$ means we are in $\mathsf{Prop}$. If we extract from $$\Pi_{n : \mathbb{N}} \Sigma_{b : \{0,1\}} \Sigma_{k : \mathbb{N}} \; n = 2 \cdot k + b$$ we will get a program which decomposes $n$ into its lowest bit $b$ and the remaining bits $k$, i.e., it computes everything. If we extract from $$\Pi_{n : \mathbb{N}} \Sigma_{b : \{0,1\}} \exists_{k : \mathbb{N}} \; n = 2 \cdot k + b$$ then the program will only compute the lowest bit $b$. The machine cannot tell which is the correct one, the user has to tell it what he wants.

-
I'm slightly confused. Are you saying that without $\mathtt{Prop}$ it'd be impossible to recognize in the extracted program that $g(x)$ doesn't contribute to the output (i.e. that it merely verifies it)? Are there scenarios where one wouldn't be able to pull out such useless code through the usual means available to code optimizers? – user Jul 24 '15 at 7:13
The extracted code produces higher-order functions. A code optimizer cannot tell whether these will be used in a useful way. So yes, unless there is some mechanism to indicate which parts of code are "useless", you can't tell. – Andrej Bauer Jul 26 '15 at 19:11
I'm sorry, but I'm having trouble coming up with an example that can't be optimized away over multiple passes starting from the desired output and working backwards (albeit with global optimization). Do you have any particular examples? – user Jul 27 '15 at 10:49
Yes, the sorting example presented in my answer. How can you tell that verify is useless? – Andrej Bauer Jul 28 '15 at 8:29
Ah, okay. Using $\mathtt{Prop}$ as a way of specifying design decisions makes a lot more sense to me than as a way of deleting useless code. – user Jul 29 '15 at 18:12

Even if you are not interested in extracting programs, the fact that Prop is impredicative allows you to build some models which you can't build using a predicative tower of universes. IIRC Thorsten Altenkirch has a model of System F using Coq's impredicativity.

-

$\mathrm{Prop}$ is impredicative, which create a very expressive proof system. However it is "too" expressive in the following sense:

$$\mathrm{impredicative\ Prop} + \mathrm{large\ elimination} + \mathrm{excluded\ middle}$$

is inconsistent. Usually you want to keep the possibility to add the excluded middle, so one solution is to keep large elimination and make Prop predicative. The other is to suppress large elimination.

Coq did both! They renamed the predicative Prop to Set, and disabled large elimination in Prop.

The expressiveness gained by impredicativity is "reassuring" in the sense 99% of "reasonable" mathematics can be formalized with it, and it is known to be consistent relative to set theory. This makes it likely they won't weaken it to something like Agda, which only has predicative universes.

-
Oh and I forgot to mention: it is not the case that Prop : Prop, that would be inconsistent. Rather quantifications over all propositions is again a proposition. – cody Apr 1 '14 at 21:31