Pourquoi Coq a Prop?

Coq a le type Prop de preuve des propositions non pertinentes qui sont rejetées lors de l'extraction. Quelle est la raison de cela si nous utilisons Coq uniquement pour les preuves. Prop est imprédicatif, donc Prop: Prop, cependant, Coq déduit automatiquement les index d'univers et nous pouvons utiliser le type (i) à la place partout. Il semble que Prop complique beaucoup tout.

J'ai lu qu'il y avait des raisons philosophiques pour séparer Set et Prop dans le livre de Luo, cependant, je ne les ai pas trouvées dans le livre. Que sont-ils?

est très utile pour l'extraction de programme car il nous permet de supprimer des parties de code inutiles. Par exemple, pour extraire un algorithmetri nous prouvons la déclaration « pour chaque liste ℓ il y a une liste k tel que k est ordonnée et k est un permutatiom de ℓ ». Si nous écrivons ceci en Coq et extrayons sans utiliser P r o p , nous aurons:$\mathtt{Prop}$$\ell$$k$$k$$k$$\ell$$\mathtt{Prop}$

1. « pour tous il y a k » nous donnera une carte qui prend des listes de listes,$\ell$$k$sort
2. "tel que soit ordonné" donnera une fonction qui traverse$k$verify et vérifie qu'elle est triée, et$k$
3. « est une permutation de ℓ » donnera une permutation qui prend ℓ à k . Notez qu'il ne s'agit pas simplement d'une cartographie, mais également d'une cartographie inverse et de programmes vérifiant que les deux cartes sont réellement des inverses.$k$$\ell$pi$\ell$$k$pi

Bien que le contenu supplémentaire ne soit pas totalement inutile, dans de nombreuses applications, nous souhaitons nous en débarrasser et le conserver sort. Ceci peut être accompli si nous utilisons à l' état « k est ordonnée » et « k est une permutation de ℓ », mais pas « pour tous ℓ il y a k ».$\mathtt{Prop}$$k$$k$$\ell$$\ell$$k$

En général, une manière commune au code extrait est de considérer une déclaration de la forme $\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.

$\mathsf{Prop}$$\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

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

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.

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.