Coq

The Rocq Prover
Uma sessão de prova interativa no CoqIDE, mostrando o script de prova à esquerda e o estado da prova à direita.
Autores	Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, Pierre Castéran
Desenvolvedores	INRIA, École Polytechnique, University of Paris-Sud, Paris Diderot University, CNRS, ENS Lyon
Lançamento inicial	1 de maio de 1989; há 37 anos (1989-05-01) (versão 4.10)
Lançamento estável	9.2.0
Repositório	github.com/rocq-prover/rocq
Escrito em	OCaml
Sistema operacional	Multiplataforma
Tipo	Assistente de prova
Licença	LGPLv2.1
Website	rocq-prover.org

O Rocq Prover (anteriormente chamado de Coq) é um provador de teoremas interativo lançado pela primeira vez em 1989. Ele permite a expressão de afirmações matemáticas, a verificação mecânica de provas dessas afirmações, auxilia na localização de provas formais usando rotinas de automação de prova e na extração de um programa certificado a partir da prova construtiva de sua especificação formal.

Rocq trabalha dentro da teoria do cálculo das construções indutivas, uma derivada do cálculo das construções. Rocq não é um provador automatizado de teoremas, mas inclui táticas de automação de prova (procedimentos) e vários procedimentos de decisão.

A Association for Computing Machinery concedeu a Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot e Pierre Castéran o ACM Software System Award de 2013 pelo Rocq (quando ainda era chamado de Coq).

Visão geral

Quando visto como uma linguagem de programação, o Rocq implementa um modelo de programação funcional tipada dependentemente; quando visto como um sistema lógico, ele implementa uma teoria de tipos de ordem superior. O desenvolvimento do Rocq tem sido apoiado desde 1984 pelo French Institute for Research in Computer Science and Automation (INRIA), em colaboração com muitas outras instituições de pesquisa francesas e internacionais. O desenvolvimento do Rocq foi iniciado por Gérard Huet e Thierry Coquand, e mais de 200 pessoas, principalmente pesquisadores, contribuíram com funcionalidades para o sistema central desde seu início. A equipe de implementação foi sucessivamente coordenada por Gérard Huet, Christine Paulin-Mohring, Hugo Herbelin e Matthieu Sozeau. Rocq é implementado principalmente em OCaml com um pouco de C. O sistema central pode ser estendido por meio de um mecanismo de plug-in.

Rocq fornece uma linguagem de especificação chamada Gallina. Programas escritos em Gallina têm a propriedade de normalização fraca, implicando que eles sempre terminam. Esta é uma propriedade distintiva da linguagem, já que loops infinitos (programas que não terminam) são comuns em outras linguagens de programação.

Como exemplo de uma prova escrita em Rocq, considere uma prova de um lema que afirma que tomar o sucessor de um número natural inverte sua paridade. A tática fold-unfold introduzida por Danvy é usada para ajudar a manter a prova simples.

From Stdlib Require Import Arith Nat Bool.

Fixpoint is_even (n : nat) : bool :=
  match n with
  | 0 => true
  | S n' => negb (is_even n')
  end.

Lemma is_even_0 :
  is_even 0 = true.
Proof. reflexivity. Qed.

Lemma is_even_S n :
  is_even (S n) = negb (is_even n).
Proof. reflexivity. Qed.

Lemma successor_flips_evenness n :
  is_even n = negb (is_even (S n)).
Proof.
  rewrite is_even_S.
  destruct (is_even n).
  * simpl. reflexivity.
  * simpl. reflexivity.
Qed.

Esta prova primeiro importa a definição de booleanos e números naturais da biblioteca padrão e então define uma função `is_even` que retorna se um número é par. Em seguida, três lemas são provados sobre esta função. O primeiro apenas reafirma as equações definidoras de `is_even` e, como o Rocq conhece as equações, sua prova é muito curta. O último lema é provado com uma distinção de caso após primeiro aplicar o segundo lema; o asterisco `*` demarca que um novo subcaso começa ali.

Usos notáveis

Outras aplicações

• CompCert: um compilador otimizador para quase toda a linguagem de programação C que é amplamente programado e provado correto em Rocq.
• Estrutura de dados de conjuntos disjuntos: prova de correção em Rocq foi publicada em 2007.
• Teorema de Feit–Thompson: prova formal usando Rocq foi concluída em setembro de 2012.
• Busy beaver: O valor do vencedor busy beaver de 5 estados foi descoberto por Heiner Marxen e Jürgen Buntrock em 1989, mas só foi provado ser o quinto busy beaver vencedor — estilizado como BB(5) — em 2024 usando uma prova em Rocq.

Linguagem de táticas

Além de construir termos Gallina explicitamente, Rocq suporta o uso de táticas escritas na linguagem embutida Ltac ou em OCaml. Essas táticas automatizam a construção de provas, realizando etapas triviais ou óbvias nas provas. Várias táticas implementam procedimentos de decisão para várias teorias. Por exemplo, a tática "ring" decide a teoria da igualdade módulo anel ou semianel axiomas via reescrita associativa-comutativa. Por exemplo, a seguinte prova estabelece uma igualdade complexa no anel dos inteiros em apenas uma linha de prova:

Require Import ZArith.
Open Scope Z_scope.
Goal forall a b c:Z,
    (a + b + c) ^ 2 =
     a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
  intros; ring.
Qed.

Procedimentos de decisão embutidos também estão disponíveis para a teoria vazia ("congruence"), lógica proposicional ("tauto"), aritmética linear de inteiros sem quantificadores ("lia") e aritmética linear racional/real ("lra"). Outros procedimentos de decisão foram desenvolvidos como bibliotecas, incluindo um para álgebra de Kleene e outro para certos objetivos geométricos.

Nome

O antigo nome Coq significa 'galo' em francês e é um jogo de palavras com o nome de Thierry Coquand, cálculo das construções ou CoC, e deriva de uma tradição francesa de nomear ferramentas de pesquisa e desenvolvimento com nomes de animais. Até 1991, Coquand estava implementando uma linguagem chamada cálculo das construções e era simplesmente chamada de CoC então. Em 1991, uma nova implementação baseada no cálculo estendido das construções indutivas foi iniciada e o nome mudou de CoC para Coq em referência indireta a Coquand, que desenvolveu o cálculo das construções juntamente com Gérard Huet e contribuiu para o cálculo das construções indutivas com Christine Paulin-Mohring. Em 11 de outubro de 2023, a equipe de desenvolvimento anunciou que o Coq seria renomeado para The Rocq Prover nos meses seguintes, e começou a atualizar a base de código, o site e as ferramentas relacionadas. A renomeação oficial ocorreu com o lançamento do Rocq 9.0 em março de 2025. O novo nome refere-se ao Inria Rocquencourt, onde o sistema foi desenvolvido pela primeira vez, e está relacionado à ave mítica Roc, o que permite manter as referências a aves do nome anterior.

Prêmios

• 2022 Open Science Award for Open Source Research Software na categoria "Científica e Técnica"

Ver também

• Cálculo das construções
• Correspondência de Curry-Howard
• Teoria de tipos intuicionista
• Lista de assistentes de prova

Referências

Ligações externas

O Commons possui uma categoria com imagens e outros ficheiros sobre Coq

• «Página oficial»