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 maio 1989; há 37 anos (versão 4.10)
Lançamento estável	9.2.0[1]
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).

Quando visto como uma linguagem de programação, o Rocq implementa um modelo de programação funcional tipada dependentemente;^[2] 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,^[3] 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.^[4]

Rocq fornece uma linguagem de especificação chamada Gallina.^[5] 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.^[6]

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^[7] é 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.

Georges Gonthier da Microsoft Research em Cambridge, Inglaterra e Benjamin Werner do INRIA usaram o Rocq para criar uma prova verificável do teorema das quatro cores, que foi concluída em 2002.^[8] Seu trabalho levou ao desenvolvimento do pacote SSReflect ("Small Scale Reflection"), que foi uma extensão significativa para o Rocq.^[9] Apesar do nome, a maioria das funcionalidades adicionadas ao Rocq pelo SSReflect são de propósito geral e não se limitam ao estilo de prova computacional reflexiva. Estas funcionalidades incluem:

• Adição de notações convenientes para pattern matching irrefutável e refutável, em tipos indutivos com um ou dois construtores
• Argumentos implícitos para funções aplicadas a zero argumentos, o que é útil ao programar com funções de ordem superior
• Argumentos anônimos concisos
• Uma tática `set` melhorada com casamento mais poderoso
• Suporte para reflexão

SSReflect é distribuído como parte da distribuição principal do Rocq desde o Coq 8.7.^[10]

• 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.^[11]
• Teorema de Feit–Thompson: prova formal usando Rocq foi concluída em setembro de 2012.^[12]
• 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.^[13][14]

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.^[15] 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.^[16] Por exemplo, a seguinte prova estabelece uma igualdade complexa no anel dos inteiros em apenas uma linha de prova:^[17]

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").^[18][19] Outros procedimentos de decisão foram desenvolvidos como bibliotecas, incluindo um para álgebra de Kleene^[20] e outro para certos objetivos geométricos.^[21]

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.^[22] 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.^[23] 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.^[24] A renomeação oficial ocorreu com o lançamento do Rocq 9.0 em março de 2025.^[25] 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.^[26]

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

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

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

• «Página oficial»