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;A Tour of Rocq 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,A Brief History 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.Adam Chlipala. "Certified Programming with Dependent Types": "Library GeneralRec". "Library InductiveTypes".
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 Teorema das quatro cores e extensão SSReflect 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. Seu trabalho levou ao desenvolvimento do pacote SSReflect ("Small Scale Reflection"), que foi uma extensão significativa para o Rocq. 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.
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 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
Categoria:Linguagens de computador Categoria:Software aplicativo Categoria:Matemática computacional Categoria:Linguagens de programação Categoria:Linguagens de programação criadas em 1984