Uma breve introdução ao Rocq Prover e seus fundamentos

Introdução

Ferramentas de prova automática baseadas na noção semântica de satisfatibilidade, como é o caso dos SAT solvers e SMT solvers, funcionam procurando um modelo para uma fórmula. As ferramentas baseadas nesta abordagem não são mais do que procedimentos de decisão que produzem uma resposta “SAT / UNSAT / UNKNOWN”. Para testar a validade de uma fórmula $\phi$ usando estas ferramentas, introduzimos a sua negação $\neg \phi$ e se obtivermos como resposta SAT ficamos a saber que a fórmula não é válida (pois foi encontrado um modelo para a sua negação). Se a resposta for UNSAT temos a garantia que a fórmula $\phi$ é válida (pois não há nenhum modelo para a sua negação), mas não é dada nenhuma justificação. Se a fórmula $\phi$ for “complexa” haverá uma forte probabilidade de a resposta ser UNKNOWN.

Há um outro grupo de ferramentas de prova que seguem uma abordagem alternativa à lógica, chamada “dedutiva”, que é focada na relação de dedução induzida nas fórmulas por um sistema de regras de inferência (sistema de prova). Estas ferramentas têm por objectivo provar a validade de uma fórmula com base nessas regras, construindo uma derivação (árvore de prova) que justifica a sua validade. Neste processo é usual o utilizador conduzir a prova (embora possa utilizar muitas estratégias automáticas), pelo que este tipo de ferramentas costumam ser chamadas de Interactive Theorem Provers ou Proof Assistants.

Num assistente de prova, o utilizador, após formalizar as noções primitivas da teoria (em estudo), desenvolve as provas interativamente (por meio de táticas de prova), e quando uma prova é finalizada um termo (ou script) de prova é criado. A utilização destas ferramentas tem-se popularizado muito e, embora acarrete um custo inicial de aprendizagem de utilização, mostra-se muito vantajosa nos seguintes aspectos: ajuda a lidar com problemas de grande dimensão; impede que se descurem detalhes; permite o arquivamento das provas e a reutilização de resultados já provados.

A idoneidade de um assistente de prova é naturalmente uma característica essencial, para qual contribui chamado o Critério de Bruijn: “os objectos de prova gerados devem poder ser verificados por um algoritmo simples”. Vamos estudar um assistente de prova que segue este critério — The Rocq Prover.

O Rocq (anteriormente denominado Coq) é um assistente de prova que está em desenvolvimento contínuo há mais de 40 anos. Recebeu o ACM Software System Award em 2013, assim como o ACM SIGPLAN Programming Languages Software Award e, em 2022 o Open Science Free Software Award.

O Rocq/Coq tem sido usado em vários projetos de verificação emblemáticos (de que são exemplos o compilador de C certificado CompCert e o projecto Verified Software Toolchain para verificação de programas C) e serviu para a formalização do teorema das quatro cores (entre muitas outras formalizações matemáticas).

O Rocq Prover é baseado num formalismo que é, simultameamente, uma lógica muito expressiva e uma linguagem de programação ricamente tipificada – Calculus of Inductive Constructions (CIC) - actualmente apresentado como PCUIC — Predicative, Polymorphic, Cumulative CIC. O seu funcionamento tem por base a correspondência “proposições-como-tipos” e “provas-como-programas”, numa lógica de ordem superior intuicionista.

Antes de nos focarmos no sistema Rocq vamos fazer uma breve apresentação de alguns tópicos importantes na compreensão do seu funcionamento.

Dedução Natural

A dedução natural é uma formalização do raciocínio matemático, introduzida por Gerhard Gentzen na primeira metade do século XX como uma representação “natural” de derivações lógicas. O sistema de prova é constituído por um conjunto de regras. Para cada conectiva lógica existem “regras de introdução” (onde a conectiva aparece na conclusão da regra) e “regras de eliminação” (onde a conectiva aparece nas premissas da regra. Vamos apresentar aqui o conjunto de regras de dedução natural para a lógica de primeira ordem clássica, usando sequentes.

• Um sequente é um juízo da forma $\Gamma \vdash \phi$, onde $\Gamma$ é um conjunto de fórmulas (o contexto) e $\phi$ uma fórmula (a conclusão do sequente).
• O juízo $\Gamma \vdash \phi$ deve ler-se: ”$\phi$ pode ser deduzida do conjunto de hipóteses $\Gamma$”, ou ”$\phi$ é uma consequência de $\Gamma$”.

O uso de sequentes permite uma representação clara do cancelamento de hipóteses, e o Rocq usa sequentes na apresentação do estado da prova.

As regras para as conectivas proposicionais são as seguintes:

Exemplo de uma árvore de prova desenvolvida em retrocesso, em forma de tabela:

As provas desenvolvidas num assistente de prova são também em retrocesso. Seguem o método conhecido como “goal directed proof”:

1. O utilizador insere a fórmula que deseja provar.
2. O sistema exibe a fórmula a ser provada, com o contexto de factos locais que podem ser usados para esta prova.
3. O utilizador insere um comando (uma regra básica ou uma tática) para decompor o objetivo de prova em objetivos mais simples.
4. O sistema exibe a lista de fórmulas que ainda precisam ser provadas.
5. Quando não restarem mais fórmulas para provar, prova está completa e poderá ser guardada.

As regras para os quantificadores têm condições laterais que têm que ser satisfeitas. Estas podem ser descritas utilizando a operação sintática de substituição:

Exemplo de uma árvore de prova (repare que quando a regra de $\exists_E$ é aplicada, uma nova variável $x_0$ é introduzida):

A prova por redução ao absurdo está codificada na regra RAA (reductio ad absurdum) e é o que dá a esta lógica uma caracter “clássico”. Com ela podemos, por exemplo, provar o “princípio do meio excluído”.

Porém, há um ramo da lógica que rejeita este princípio.

Lógica Clássica vs Lógica Intuicionista

A compreensão clássica da lógica é baseada na noção de verdade. A verdade de uma afirmação é “absoluta” e independente de qualquer raciocínio. Portanto, as afirmações são verdadeiras ou falsas, e a proposição $(A \vee \neg A)$ deve ser válida independentemente do significado de $A$.

A lógica intuicionista (ou construtiva) é um ramo da lógica formal que rejeita este princípio orientador. Baseia-se na noção de prova. O julgamento sobre uma afirmação baseia-se na existência de uma prova (ou “construção”) dessa afirmação. Para que $(A \vee \neg A)$ seja válida é necessário ter uma prova de $A$ ou uma prova de $\neg A$ (mostrando que assumir uma prova de $A$ conduz a uma contradição).

Provas por redução ao absurdo, ou usando a lei do meio excluído, não são construtivas/intuicionistas. Mas, se retirarmos a regra RAA ao sistema de prova acima apresentado, o sistema deixa de ser clássico e passa a ser intuicionista.

Tudo o que se prova no sistema intuicionista, também se prova na lógica clássica. Contudo, como era de esperar, há algumas tautologias da lógica clássica que não são válidas na lógica intuicionista. Por exemplo,

Tradicionalmente, a lógica clássica é definida pela extensão da lógica intuicionista com uma das seguintes leis: lei de redução ao absurdo, lei da dupla negação, lei do meio excluído ou lei de Pierce.

Proposições como Tipos

A interpretação das proposições como tipos estabelece uma relação precisa entre a lógica intuicionista e o lambda calculus:

• uma proposição $A$ é vista como um tipo (o tipo das suas provas);
• uma prova de $A$ é vista como um termo do tipo $A$.

Portanto, uma proposição $A$ é demonstrável apenas no caso do tipo $A$ ser habitado, e o mecanismo de type checking pode ser usado para verificar uma prova.

A decidibilidade do type checking está, portanto, no cerne dos assistentes de prova fundamentados nestes princípios, como é o caso do Rocq. No final do desenvolvimento de uma prova, o termo de prova é verificado quanto ao tipo e o tipo é comparado com o objetivo de prova original. É esta característica que faz com que o Rocq cumpra o Critério de Bruijn, uma vez que o algoritmo de type checking é simples e robusto.

Esta analogia entre lógica formal e cálculo computacional foi estabelecida por Haskell Curry e William Howard. O isomorfismo de Curry-Howard estabelece uma correspondência entre a dedução natural para a lógica intuicionista e o lambda calculus.

Lambda Calculus

O lambda calculus (introduzido na década de 1930 por Alonzo Church) é um sistema formal para expressar computação, baseado na construção de funções (pelo mecanismo de abstração) e na aplicação de funções (pelo mecanismo de substituição de variáveis). O lambda calculus tipificado introduz uma disciplina de tipos sobre os termos. Os tipos são entidades de natureza sintática associadas aos lambda termos. A natureza concreta dos tipos depende do cálculo lambda em causa. Estes calculi estão na base das linguagens funcionais de programação e da teoria da prova via o isomorfismo das “proposições como tipos”.

Na sua versão mais simples, $\lambda_\rightarrow$, a sintaxe do lambda calculus tipificado é a seguinte:

O termo $(\lambda x:\tau . e)$ representa a função de parâmetro $x$, de tipo $\tau$, e corpo $e$, e o termo $(a b)$ denota a aplicação da função $a$ ao argumento $b$.

Para evitar a proliferação de parêntesis, são usadas as seguintes convenções:

• a construção de tipo $\to$ é associativa à direita;
• a aplicação é associativa à esquerda;
• o alcance da abstração $\lambda$ estende-se para a direita tanto quanto possível.

No sistema de tipos deste calculus, as funções são classificadas com tipos simples que determinam o tipo de seus argumentos e o tipo dos valores que produzem, e podem ser aplicadas apenas a argumentos do tipo apropriado. Para descrever as regras de tipo é necessária uma noção de contexto para declarar as variáveis livres (isto é, que não estão a ser abstraidas por um $\lambda$). Neste caso, um contexto é um conjunto $\Gamma$ de declarações de variáveis e usamos a seguinte sintaxe: $\quad \Gamma ::= \quad . | \Gamma, x : \tau$

Um termo $a$ diz-se “bem tipificado” (ou “bem tipado”) se existirem $\Gamma$ e $\sigma$ tal que $\Gamma \vdash a : \sigma$.

Aqui está um exemplo de uma árvore derivação para um juízo de tipo.

Num termo, uma variável que está abstraída por um $\lambda$ diz-se ligada, caso contrário diz-se livre. $\mathsf{FV}(e)$ denota o conjunto das variáveis livres do termo $e$. Por exemplo, em $(\lambda x: \tau. y x)$, a variável $x$ é ligada e a $y$ é livre. Naturalmente que o nome das variáveis ligadas não é importante, e podemos renomea-las com novos nomes (conversão- $\alpha$), desde que não colidam com nomes de variáveis livres em uso. Por exemplo: $(\lambda x: \tau. y x) =(\lambda z: \tau. y z)$.

Os termos são manipulados por uma regra de computação ($\beta$-redução) que indica como calcular o valor de uma função para um dado argumento, e que se baseia na noção de substituição. Na aplicação de uma substituição a um termo, contamos com a convenção das variáveis: “todas as variáveis ligadas são escolhidas para serem diferentes das variáveis livres”. Assim, a acção de uma substituição num termo é definida com possíveis renomeações das variáveis ligadas.

Geralmente há mais do que uma maneira de realizar cálculos.

Um termo diz-se uma forma normal se não contém redexes, e diz-se fortemente normalizável se qualquer sequência de redução conduzir sempre a uma forma normal. Das várias estratégias de redução destacam-se duas:

• call-by-value (selecionar o redex mais à esquerda e mais interno).
• call-by-name (selecionar o redex mais à esquerda e mais externo)

Propriedades deste sistema:

• Unicidade de tipos: $\quad$ Se $\Gamma \vdash a : \sigma~$ e $\Gamma \vdash a : \tau$, então $\sigma = \tau$.
• Inferência de tipos: $\quad$ Pode-se deduzir automaticamente o tipo (se existir) de um termo num dado contexto.
• Preservação de tipos: $\quad$ Se $\Gamma \vdash a : \sigma$ e $a \rightarrow_\beta\, b$, então $\Gamma \vdash b : \sigma$.
• Normalização forte: $\quad$ Se $\Gamma \vdash a : \sigma$, então $a$ é fortemente normalizável.
• Confluência: $\quad$ Se $a \equiv_\beta\, b$, então $a \twoheadrightarrow_\beta\, e$ e $b \twoheadrightarrow_\beta\, e$, para algum termo $e
• Substituição: $\quad$ Se $\Gamma, x:\tau \vdash a : \sigma$ e $\Gamma \vdash b:\tau$ , então $\Gamma \vdash a[b/x] : \sigma$.
• Enfraquecimento: $\quad$ Se $\Gamma \vdash a : \sigma$ e $\Gamma\subseteq \Gamma’$, então $\Gamma’ \vdash a : \sigma$.
• Fortalecimento: $\quad$ Se $\Gamma, x:\tau \vdash a : \sigma$ e $x\not\in\mathsf{FV}(a)$, então $\Gamma \vdash a : \sigma$.

O Isomorfismo de Curry-Howard

O isomorfismo de Curry-Howard estabelece uma correspondência entre a dedução natural para a lógica intuicionista e o lambda calculus.

Este isomorfismo, apresentado aqui na sua versão mais simples, pode ser levado para o patamar mais elevado da lógica de ordem superior (onde é possível quantificar sobre funções e sobre predicados). Na apresentação destes lambda calculi, em vez de termos duas categorias distintas de expressões (termos e tipos), temos uma categoria única de expressões, que são chamadas de pseudo-termos.

Aqui podemos ter tipos dependentes (de termos). Note como na aplicação de uma função dependente $M$ a um termo $N$, o tipo de $M\,N$ é afectado pelo termo $N$ através de uma subtituição.

Existe um conjunto de sorts (constantes que denotam os universos do sistema de tipos) organizadas hierarquicamente e regras de tipo que determinam que tipos de funções dependentes se podem construir e em que sort eles habitam.

The Rocq Prover

O Rocq é um assistente de prova baseado no Cálculo de Construções Inductivas Polimórfico e Cumulativo (PCUIC), uma teoria de tipos ordem superior com tipos indutivos. Os mecanismos de eliminação dos tipos indutivos (recursores e princípios de indução) são gerados automaticamente a partir das definições indutivas. O sistema Rocq está assente na correspondência “proposições-como-tipos”. A linguagem das provas é uma linguagem de programação. Trabalha com lógica intuicionista, onde uma prova é uma construção que produz testemunhas para declarações existenciais e provas efectivas para as disjunções, o que permite fazer extração de programas a partir da sua especificação.

Existe uma hierarquia bem fundada de sorts que tem na base:

• Prop - proposições lógicas.
• SProp - proposições lógicas estritas (semelhante a Prop, mas sem acesso às provas).
• Set - conjuntos pequenos (tipos cujos valores não envolvem outros tipos).

Type é o sort dos tipos de dados e estrutura matemáticas bem formadas (na realidade há uma hierarquia de Type(i), i=1,2,…)

O sistema Rocq é constituido por:

• Uma linguagem de especificação (baseada no PCUIC) — Gallina — que permite desenvolver teorias matemáticas e escrever especificações de programas.

• Uma linguagem de comandos — Vernacular — que permite:
  • Definir estruturas de dados, funções ou predicados;
  • Enunciar teoremas matemáticos e especificações de software;
  • Desenvolver interativamente provas formais destes teoremas;
  • Verificar estas provas por computador através de um “núcleo” de certificação relativamente pequeno (Critério de Bruijn);
  • Extrair programas certificados para linguagens como OCaml, Haskell ou Scheme.
• Uma linguagem de tácticas — Ltac — que permite ao utilizador definir as suas próprias estratégias de prova.

Ilustramos a sintaxe da linguagem Gallina com estes pequenos exemplos:

O ambiente (lista de declarações e definições) em que as expressões são avaliadas e tipificadas é constituído por um ambiente global (eventualmente carregado de bibliotecas, e que vai sendo depois enriquecido pelo utilizador) e um contexto local.

O sistema Rocq possui um mecanismo de blocos Section id … End id que permite manipular o contexto local (expandindo-o e contraindo-o).

Vejamos um exemplo em que abrimos uma secção EX, declaramos localmente um conjunto A, um predicado P e uma proposição Q, e de seguida lançamos um lema para prova e aplicamos táticas para o provar, criando um termo de prova. No final, com o comando Qed, o identificador example é definido com este termo de prova e adicionado ao contexto local.

Podemos ver o termo com o comando Print.

que corresponde ao seguinte lambda termo e juízo de tipo:

Ao fechar a secção EX as variáveis declaradas localmente na secção são abstraídas no termo de prova.

Táticas associadas às conectivas da lógica de primeira ordem.

Mais algumas táticas.

A teoria de tipos do Rocq tem diversas construções sintácticas e respectivas regras de redução que são aplicadas na avaliação do termos.

A avaliação de termos é feita com o comando Eval.

Sessão Laboratorial

A Rocq Platform combina o Rocq Prover com um conjunto de packages para estender as suas funcionalidades.

O Rocq Prover possui um IDE independente chamado RocqIDE, que é distribuído como parte da Rocq Platform. Sugerimos que use este IDE. Alternativamente, pode correr o Rocq Prover a partir do Emacs, do VS Code ou do Vim.

O ficheiro lesson1.v contém muitos exemplos comentados e algumas provas para completar. Carregue este ficheiro no sistema Rocq, analise atentamente os exemplos e resolva os exercícios propostos.

Encontrará exercícios adicionais em Rocq(1).pdf.