Rocq

Rocq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Rocq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

The Association for Computing Machinery awarded Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, and Pierre Castéran with the 2013 ACM Software System Award for Rocq (when it was named Coq).

Overview

When viewed as a programming language, Rocq implements a dependently typed functional programming model; when viewed as a logical system, it implements a higher-order type theory. The development of Rocq has been supported since 1984 by French Institute for Research in Computer Science and Automation (INRIA), in collaboration with many other French and international research institutions. The development of Rocq was initiated by Gérard Huet and Thierry Coquand, and more than 200 people, mainly researchers, have contributed features to the core system since its inception. The implementation team has successively been coordinated by Gérard Huet, Christine Paulin-Mohring, Hugo Herbelin, and Matthieu Sozeau. Rocq is mainly implemented in OCaml with a bit of C. The core system can be extended by way of a plug-in mechanism.

Rocq provides a specification language named Gallina. Programs written in Gallina have the weak normalization property, implying that they always terminate. This is a distinctive property of the language, since infinite loops (non-terminating programs) are common in other programming languages.

As an example of a proof written in Rocq, consider a proof of a lemma which states that taking the successor of a natural number flips its parity. The fold-unfold tactic introduced by Danvy is used to help keep the proof simple.

<span id="mwRg"></span><span class="kn" id="mwRw">From</span> <span class="n" id="mwSA">Stdlib</span> <span class="kn" id="mwSQ">Require</span> <span class="kn" id="mwSg">Import</span> <span class="n" id="mwSw">Arith</span> <span class="n" id="mwTA">Nat</span> <span class="n" id="mwTQ">Bool</span><span class="o" id="mwTg">.</span> <span class="kn" id="mwTw">Fixpoint</span> <span class="n" id="mwUA">is_even</span> <span class="o" id="mwUQ">(</span><span class="n" id="mwUg">n</span> <span class="o" id="mwUw">:</span> <span class="n" id="mwVA">nat</span><span class="o" id="mwVQ">)</span> <span class="o" id="mwVg">:</span> <span class="n" id="mwVw">bool</span> <span class="o" id="mwWA">:=</span> <span class="k" id="mwWQ">match</span> <span class="n" id="mwWg">n</span> <span class="k" id="mwWw">with</span> <span class="o" id="mwXA">|</span> <span class="mi" id="mwXQ">0</span> <span class="o" id="mwXg">=></span> <span class="bp" id="mwXw">true</span> <span class="o" id="mwYA">|</span> <span class="n" id="mwYQ">S</span> <span class="n" id="mwYg">n'</span> <span class="o" id="mwYw">=></span> <span class="n" id="mwZA">negb</span> <span class="o" id="mwZQ">(</span><span class="n" id="mwZg">is_even</span> <span class="n" id="mwZw">n'</span><span class="o" id="mwaA">)</span> <span class="k" id="mwaQ">end</span><span class="o" id="mwag">.</span> <span class="kn" id="mwaw">Lemma</span> <span class="n" id="mwbA">is_even_0</span> <span class="o" id="mwbQ">:</span> <span class="n" id="mwbg">is_even</span> <span class="mi" id="mwbw">0</span> <span class="o" id="mwcA">=</span> <span class="bp" id="mwcQ">true</span><span class="o" id="mwcg">.</span> <span class="kn" id="mwcw">Proof</span><span class="o" id="mwdA">.</span> <span class="kp" id="mwdQ">reflexivity</span><span class="o" id="mwdg">.</span> <span class="kn" id="mwdw">Qed</span><span class="o" id="mweA">.</span> <span class="kn" id="mweQ">Lemma</span> <span class="n" id="mweg">is_even_S</span> <span class="n" id="mwew">n</span> <span class="o" id="mwfA">:</span> <span class="n" id="mwfQ">is_even</span> <span class="o" id="mwfg">(</span><span class="n" id="mwfw">S</span> <span class="n" id="mwgA">n</span><span class="o" id="mwgQ">)</span> <span class="o" id="mwgg">=</span> <span class="n" id="mwgw">negb</span> <span class="o" id="mwhA">(</span><span class="n" id="mwhQ">is_even</span> <span class="n" id="mwhg">n</span><span class="o" id="mwhw">).</span> <span class="kn" id="mwiA">Proof</span><span class="o" id="mwiQ">.</span> <span class="kp" id="mwig">reflexivity</span><span class="o" id="mwiw">.</span> <span class="kn" id="mwjA">Qed</span><span class="o" id="mwjQ">.</span> <span class="kn" id="mwjg">Lemma</span> <span class="n" id="mwjw">successor_flips_evenness</span> <span class="n" id="mwkA">n</span> <span class="o" id="mwkQ">:</span> <span class="n" id="mwkg">is_even</span> <span class="n" id="mwkw">n</span> <span class="o" id="mwlA">=</span> <span class="n" id="mwlQ">negb</span> <span class="o" id="mwlg">(</span><span class="n" id="mwlw">is_even</span> <span class="o" id="mwmA">(</span><span class="n" id="mwmQ">S</span> <span class="n" id="mwmg">n</span><span class="o" id="mwmw">)).</span> <span class="kn" id="mwnA">Proof</span><span class="o" id="mwnQ">.</span> <span class="k" id="mwng">rewrite</span> <span class="n" id="mwnw">is_even_S</span><span class="o" id="mwoA">.</span> <span class="k" id="mwoQ">destruct</span> <span class="o" id="mwog">(</span><span class="n" id="mwow">is_even</span> <span class="n" id="mwpA">n</span><span class="o" id="mwpQ">).</span> <span class="o" id="mwpg">*</span> <span class="k" id="mwpw">simpl</span><span class="o" id="mwqA">.</span> <span class="kp" id="mwqQ">reflexivity</span><span class="o" id="mwqg">.</span> <span class="o" id="mwqw">*</span> <span class="k" id="mwrA">simpl</span><span class="o" id="mwrQ">.</span> <span class="kp" id="mwrg">reflexivity</span><span class="o" id="mwrw">.</span> <span class="kn" id="mwsA">Qed</span><span class="o" id="mwsQ">.</span>

This proof firsts import the definition of booleans and natural numbers from the standard library, and then defines a is_even which is a function returning whether a number is even. Then, three lemmas are proven about this function. The first just restate the defining equations of is_even, and since Rocq knows the equations their proof is very short. The last lemma is proven with a case distinction after first applying the second lemma; the star * demarks that a new sub-case starts there.