Raciocínio Indutivo no Rocq Prover

A indução é uma técnica que nos permite definir e raciocinar com objectos que são estruturados (de uma forma bem fundada) e finitos (embora arbitrariamente grandes). A indução explora a natureza finita e estruturada desses objectos para superar a sua complexidade arbitrária.

Quando um conjunto é definido indutivamente, entendemos que ele é “construído de baixo para cima” por um conjunto de construtores básicos. Os elementos de tal conjunto podem ser decompostos de forma única em “elementos menores” de maneira bem fundada. Isto dá-nos princípios de prova por indução e a possibilidade de definir de funções à custa de recursores.

Tipos Indutivos em Rocq

Podemos definir um novo tipo $T$ indutivamente, declarando os seus construtores com os respectivos tipos, que devem ter a forma: $\tau_{1} \to \ldots \to \tau_{n} \to T$ , com $n\geq 0$, onde $T$ pode apenas ocorrer em posições positivas de $\tau_i$.

Os construtores (que são as regras de introdução do tipo $T$) são formas canónicas de construir um elemento do tipo $T$. Portanto, os seus habitantes são os objetos que podem ser obtidos por um número finito de aplicações dos construtores do tipo. O tipo $T$ definido é, assim, o menor conjunto fechado para as suas regras de introdução.

Para programar e raciocinar sobre um tipo indutivo, é necessário dispor de meios para analisar os seus elementos. As regras de eliminação dos tipos indutivos expressam formas de utilizar objetos desse tipo para definir objetos de outros tipos, estando associadas a novas regras computacionais.

Quando um tipo indutivo $T$ é definido, a teoria de tipos gera automaticamente um esquema de prova por indução e um esquema de recursão primitiva. O tipo indutivo vem equipado com um recursor (uma constante $\mathbf{R}T$) que codifica o _princípio de indução estrutural sobre esse tipo indutivo, e que pode ser utilizado para definir funções e provar propriedades sobre esse tipo. As regras de computação associadas ao recursor $\mathbf{R}_T$) definem um esquema recursivo seguro para programação (i.e., que não introduz não terminação).

Para ilustrar esta ideias, vamos tomar o exemplo dos números naturais, com os seus dois construtores: o zero, O, e o sucessor, S.

A regra de tipo para o recursor $\mathbf{R}_\mathbb{N}$ e respectivas regras de computação são as seguintes.

Com este recursor é possível definir um princípio de prova por indução e um princípio de recursão primitiva.

O esquema de prova por indução pode ser obtido do recursor definindo $P$ como sendo do tipo $\mathbb{N}\to \mathsf{Prop}$.

Este é o conhecido princípio de indução sobre números naturais, que permite provar propriedades da forma $\forall n: \mathbb{N}. (P n)$, por indução em $n$.

O esquema de recursão primitivo pode ser obtido configurando $P : \mathbb{N} \to \mathsf{Set}$.

Podemos definir funções usando a recursão primitiva

Esta abordagem oferece uma maneira segura de usar recursão sem introduzir termos que não terminam.

Vejamos como a declaração do tipo indutivo nat introduz no ambiente do sistema Rocq, não apenas os construtores O e S, mas também os eliminadores (nat_rect, nat_ind e nat_rec) apresentados acima.

Análise de Casos e Recursão Geral

Codificar funções recursivas em termos de constantes de eliminação é uma maneira segura de expressar recursão (i.e., sem introduzir objetos não normalizáveis), mas está muito longe da forma como costumamos programar. Em vez disso, geralmente usamos recursão geral e análise de casos.

A análise de casos fornece uma regra de eliminação para tipos indutivos. Por exemplo, sendo $n: \mathbb{N}$, podemos definir um objecto $(\mathsf{match \ } n \mathsf{\ with \ } { 0 \Rightarrow b1 | (S x) \Rightarrow b2})$ do tipo σ dependendo do construtor que for usado para introduzir $n$.

As linguagens de programação funcional admitem recursão geral, permitindo que funções recursivas sejam definidas por meio de concordância de padrões e um operador de ponto fixo geral para codificar chamadas recursivas.

Por exemplo, a função double pode também ser definida do seguinte modo.

É claro que esta abordagem abre as portas para a introdução de objectos não normalizáveis.

A não terminação do processo de computação num sistema com tipos dependentes (de termos) tem impacto na decidibilidade do algoritmo type-checking (que é central ao sistema Rocq), devido à verificação da conversibilidade entre tipos que pode exigir computação com funções recursivas.

Em Rocq não é permitido definir funções que não terminam.

• Uma maneira usual de garantir a terminação de expressões de ponto fixo é impor restrições sintáticas, restringindo todas as chamadas recursivas a serem aplicadas a termos estruturalmente menores que o argumento formal da função.
• Outra forma de garantir terminação é aceitar uma função de medida (de indução) que especifique como a medida do argumento decresce entre chamadas recursivas.

Definições Indutivas

No Rocq Prover as definições indutivas estão por todo o lado. Por exemplo, as operadores relacionais e as próprias conectivas lógicas estão definidas como tipos indutivos. Vejamos alguns exemplos.

Vetores de comprimento n sobre o tipo A

Vejamos o exemplo das sequências de comprimento n de elementos do tipo A.

Note-se a diferença entre os dois parâmetros A e n:

• A é um parâmetro geral, comum a todas as regras de introdução;
• n é um índice, que é instanciado de forma diferente nas regras de introdução.

O tipo do construtor Vcons é uma função dependente.

Relações

Em Rocq, a igualdade entre dois habitantes x e y do mesmo tipo A, denotada x = y, é definida como uma família de predicados recursivos “ser igual a x”, parametrizados tanto por x quanto por seu tipo A. Esta família de tipos possui apenas uma regra de introdução, que corresponde à reflexividade.

O princípio de indução gerado é o seguinte:

Note que a sintaxe “x = y” é uma notação alternativa de “eq x y”, e que o parâmetro A está implícito, pois pode ser inferido de x.

Outras relações também são introduzidas como uma família indutiva de proposições. Por exemplo, a relação de ordem n ≤ m nos números naturais é definida da seguinte forma:

Esta definição introduz a relação binária n ≤ m como a família de predicados unários “ser maior ou igual a um dado n”, parametrizado por n. Note como n é um parâmetro geral, enquanto o segundo argumento de le é um índice. Uma notação alternativa para “le x y” é “x <= y”.

Repare como os constructores deste tipo indutivo podem ser vistos como as regras de introdução para a relação “<=” no sistema de prova. Na verdade, um objeto do tipo n ≤ m nada mais é do que uma prova construída usando os construtores le_n e le_S.

Conectivas Lógicas

No sistema Rocq, a maioria das conectivos lógicas são definidas como tipos indutivos. As excepções são: as conectivas ⇒ e ∀ que são diretamente representados pelos tipos → e Π; a negação que é definida como a implicação do absurdo; e a equivalência que é definida como a conjunção de duas implicações.

Os construtores são as regras de introdução. O princípio da indução fornece as regras de eliminação. Todas as regras da lógica intuicionista (que vimos na aula passada) são deriváveis.

Sessão Laboratorial

Vamos começar por realçar alguns aspectos práticos do Rocq Prover que são relevantes para a sua utilização.

Poderá experimentar o que a seguir se explica, correndo no Rocq PRover o ficheiro lesson2a.v e analisando as respostas obtidas.

Notation, Overloading and Interpretation scopes

Para simplificar a escrita de expressões, o Coq permite introduzir notações alternativas através do comando Notation. Algumas notações podem ser sobrecarregadas. O comando Locate permite encontrar a função escondida atrás de uma notação.

Para lidar com a sobrecarga, o sistema Rocq fornece uma noção de interpretation scopes, que definem como as notações são interpretadas.

Os scopes podem ser abertos e vários scopes podem estar abertos ao mesmo tempo. Quando uma determinada notação tem diversas interpretações, o scope aberto mais recentemente tem precedência.

Pode-se usar a sintaxe (term)%key para vincular a interpretação do term ao scope key.

Arguments Implícitos

Em muitos termos algumas informações de tipo são redundantes, pois podem ser inferidas do restante termo. Um subtermo pode ser substituído pelo símbolo _ se puder ser inferido de outras partes do termo.

O mecanismo de argumentos implícitos permite evitar usar _ nas expressões Rocq. Podemos activar este mecanismo correndo o comando Set Implicit Arguments.

Como pode constatar ao correr estas definições, os argumentos que podem ser inferidos são automaticamente determinados e declarados como argumentos implícitos quando uma função é definida.

Além disso,

Bibliotecas do Rocq

O Rocq Prover disponibiliza um vasto conjunto de bibliotecas sobre variadissimos tipos de dados e suas proriedades

A biblioteca standard do Rocq disponibiliza um conjunto de módulos diretamente acessíveis através do comando From Stdlib Require Import.

Pesquisa de Propriedades

No desenvolvimento de provas podemos usar propriedades que estão disponíveis no ambiente de prova. Os comandos que nos permitem fazer pesquinas dessas propriedades são naturalmente úteis. Alguns exemplos:

• Search – Este comando pode ser utilizado para filtrar o contexto local e global, de modo a recuperar objetos cujo nome ou tipo satisfaça um conjunto de condições.

• SearchPattern – Mostra o nome e o tipo de todos os teoremas do contexto atual que correspondem a um determinado padrão.

• SearchRewrite – Mostra o nome e o tipo de todos os teoremas do contexto atual cuja conclusão é uma igualdade em que um dos lados corresponde a um determinado padrão.

Desenvolvimento de Provas

O sistema Rocq fornece um enorme conjunto de táticas de prova, combinadores de táticas e comandos, que poderão ser consultados (em todos os seus detalhes e variantes) na sua documentação. Destacamos abaixo algumas das mais relevantes.

No ficheiro lesson2b.v vai encontrar muitos exemplos comentados e algumas provas para completar. Carregue este ficheiro no Rocq Prover, analise atentamente os exemplos e resolva os exercícios propostos.

Exercícios: Encontrará exercícios adicionais em Rocq(2).pdf.

Táticas básicas

Táticas para lidar com as conectivas lógicas

Táticas para lidar com igualdade

Táticas para lidar com a conversão de termos

Táticas para raciocínio indutivo

Mais algumas táticas e comandos úteis

Combinadores de táticas

As táticas podem ser combinadas em táticas mais poderosas usando combinadores de táticas (tacticals)

Táticas automáticas

As táticas automáticas utilizam repositórios de teoremas, e é possível gerir estes repositórios para controlar automação das táticas.