Por que Coq tem Prop?

A Coq tem um tipo Prop de proposições irrelevantes à prova que são descartadas durante a extração. Quais são as razões para isso, se usarmos o Coq apenas para provas. Prop é impredicativo, portanto Prop: Prop, no entanto, Coq infere automaticamente os índices do universo e podemos usar o Tipo (i) em qualquer lugar. Parece que Prop complica muito tudo.

Eu li que existem razões filosóficas para separar Set e Prop no livro de Luo, no entanto, não as encontrei no livro. O que eles são?

ℓ k k k ℓ P r o $\mathtt{Prop}$ é muito útil para a extração de programas, pois permite excluir partes do código que são inúteis. Por exemplo, para extrair um algoritmo de classificação, provaríamos a afirmação "para cada lista existe uma lista tal que é ordenado e é uma permutação de ". Se escrevermos isso em Coq e extraímos sem usar , obteremos:$\ell$$k$$k$$k$$\ell$$\mathtt{Prop}$

1. "para todos existe " nos dará um mapa que leva listas para listas,$\ell$$k$sort
2. "tal que seja ordenado" fornecerá uma função que percorre e verifica se está classificada, e$k$verify$k$
3. " é uma permutação de " dará uma permutação que leva a . Observe que não é apenas um mapeamento, mas também o mapeamento inverso, juntamente com programas que verificam se os dois mapas são realmente inversos.ℓ ℓ $k$$\ell$pi$\ell$$k$pi

Embora o material extra não seja totalmente inútil, em muitos aplicativos queremos nos livrar dele e ficar justos sort. Isso pode ser feito se usarmos para declarar " está ordenado" e " é uma permutação de ", mas não "para todos há ". k k ℓ ℓ $\mathtt{Prop}$$k$$k$$\ell$$\ell$$k$

Em geral, uma maneira comum de extrair código é considerar uma declaração no formato que é inserido, é saída e explica o que significa para ser uma saída correta. (No exemplo acima, e são os tipos de lista e é " é ordenado e é uma permutação de .") Se estiver em então extração dá um mapa tal que vale para todosx y ϕ ( x , y ) y A B ϕ ( ℓ , k ) k k ℓ ϕ P r o p f : A → B ϕ ( x , f ( x ) ) x ∈ A ϕ S e t g g ( x ) ϕ ( x $\forall x : A \,.\, \exists y : B \,.\, \phi(x, y)$$x$$y$$\phi(x,y)$$y$$A$$B$$\phi(\ell, k)$$k$$k$$\ell$$\phi$$\mathtt{Prop}$$f : A \to B$$\phi(x, f(x))$$x \in A$ . Se é em então nós também terá uma função tal que é a prova de que detém, para todos . Muitas vezes, a prova é computacionalmente inútil e preferimos nos livrar dela, especialmente quando está aninhada profundamente em alguma outra declaração. nos dá a possibilidade de fazer isso.$\phi$$\mathtt{Set}$$g$$g(x)$x ∈ A P r o $\phi(x, f(x))$$x \in A$$\mathtt{Prop}$

Adicionado em 29/07/2015: Há uma dúvida sobre se poderíamos evitar ao otimizar automaticamente "código inútil extraído". Até certo ponto, podemos fazer isso, por exemplo, todo o código extraído do fragmento negativo da lógica (coisas criadas a partir do tipo vazio, tipo de unidade, produtos) é inútil, pois apenas embaralha a unidade. Mas existem decisões de design genuínas que você precisa tomar ao usar . Aqui está um exemplo simpe, onde significa que estamos em e significa que estamos em . Se extrairmos de P r o p Σ T y p e ∃ P r o p Π n : N Σ b : { 0 , 1 } Σ k : $\mathsf{Prop}$$\mathsf{Prop}$$\Sigma$$\mathsf{Type}$$\exists$$\mathsf{Prop}$n b k Π N : N Σ b : { 0 , 1 } ∃ K :

$\mathrm{Prop}$

é inconsistente. Normalmente, você deseja manter a possibilidade de adicionar o meio excluído, portanto, uma solução é manter uma grande eliminação e tornar o Prop predicativo. O outro é suprimir grande eliminação.

Coq fez os dois! Eles renomearam o predicativo Prop to Set e desativaram grande eliminação no Prop.

A expressividade obtida pela impredicatividade é "tranquilizadora", no sentido em que 99% da matemática "razoável" pode ser formalizada com ela, e sabe-se que ela é consistente em relação à teoria dos conjuntos. Isso torna provável que eles não o enfraquecem para algo como o Agda, que possui apenas universos predicativos.

Mesmo que você não esteja interessado em extrair programas, o fato de Propser impredicativo permite criar alguns modelos que não podem ser construídos usando uma torre predicativa de universos. O IIRC Thorsten Altenkirch tem um modelo do Sistema F usando a impredicatividade da Coq.