VOOZH about

URL: https://rocq-prover.org/

⇱ Welcome to a World of Rocq

👁 Rocq logo
👁 Rocq logo

A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more.

The Rocq Prover was formerly known as the Coq Proof Assistant (see more on the name evolution).

A short introduction to the Rocq Prover

The Rocq Prover is an interactive theorem prover, or proof assistant. This means that it is designed to develop mathematical proofs, and especially to write formal specifications: programs and proofs that programs comply to their specifications. An interesting additional feature of Rocq is that it can automatically extract executable programs from specifications, as either OCaml or Haskell source code. 
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
Fixpoint fac n :=
 match n with
 | 0 => 1
 | S n' => n * fac n'
 end.
= 120
: nat
n: nat
fac (S n) = S n * fac n
n: nat
fac (S n) = S n * fac n
reflexivity.Qed.
n: nat
fac n > 0
n: nat
fac n > 0
fac 0 > 0
n: nat
IHn: fac n > 0
fac (S n) > 0
fac 0 > 0
1 > 0
lia.
n: nat
IHn: fac n > 0
fac (S n) > 0
n: nat
IHn: fac n > 0
S n * fac n > 0
lia.Qed.
[Loading ML file extraction_plugin.cmxs (using legacy method) ... done]
Extraction Language OCaml.
(** val fac : nat -> nat **)

let rec fac n = match n with
| O -> S O
| S n' -> mul n (fac n')

Trusted in Academia and Industry

These organisations and companies rely on Rocq every day — along with hundreds of other researchers and engineers.

The Rocq Prover has been recognised by the ACM for their prestigious Software System Award.

The recipients of the awards are thanking all developers who contributed to the success of the Rocq Prover, the users who illustrated how to use Rocq for so many impressive projects in formal certification, programming, logic, formalization of mathematics and teaching as well as the whole surrounding scientific community in proof theory, type theory, programming languages, interactive theorem proving.

RELIABILITY

A Foundationally Sound, Trustworthy Formal Language and Implementation

Rocq's highly expressive type system and proof language enable fully mechanised verification of programs with respect to strong specifications in a wide variety of languages. Through the Curry-Howard lens, it simultaneously provides a rich logic and foundational computational theory for mathematical developments, supported by a flexible proof environment. Its well-studied core type theory, resulting from over 40 years of research, is implemented in a well-delimited kernel using the performant and safe OCaml programming language, providing the highest possible guarantees on mechanised artifacts. The core type theory is itself formalised in Rocq in the MetaRocq project, a verified reference checker is proven correct and complete with respect to this specification and can be extracted to reduce the trusted code base of any formalization to the specification of Rocq's theory and the user specification.

DIVERSITY OF APPLICATIONS
From Low-Level Verification to Homotopy Type Theory

The Rocq Prover enables a very wide variety of developments to coexist in the same system, ranging from end-to-end verified software and hardware models to the development of higher-dimensional mathematics. Flagship projects using Rocq include the Mathematical Components library and its derived proofs of the Four-Color and Feith-Thompson theorems; the verified CompCert C compiler and the associated Verified Software Toolchain for proofs of C-like programs, or the development of Homotopy Type Theory and Univalent Foundations of mathematics. Rocq is also a great vehicle for teaching logic and computer science as exemplified by the thousands of students that have gone through the Software Foundations series of books. Rocq's development is entirely open-source and a large and diverse community of users participate in its continued evolution.

COMPCERT
👁 Image
Mathematical Components
(* (c) Copyright 2006-2018 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
From fourcolor Require Import real realplane.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]

(******************************************************************************)
(* This files contains the proof of the high-level statement of the Four *)
(* Color Theorem, whose statement uses only the elementary real topology *)
(* defined in libraries real and realplane. The theorem is stated for an *)
(* arbitrary model of the real line, which we show in separate libraries *)
(* (dedekind and realcategorical) is equivalent to assuming the classical *)
(* excluded middle axiom. *)
(* We only import the real and realplane libraries, which do not introduce *)
(* any extra-logical context, in particular no new notation, so that the *)
(* interpretation of the text below is as transparent as possible. *)
(* Accordingly we use qualified names refer to the supporting result in the *)
(* finitize, discretize and combinatorial4ct libraries, and do not rely on *)
(* the ssreflect extensions in the formulation of the final arguments. *)
(******************************************************************************)
Section FourColorTheorem.Variable Rmodel : Real.model.Let R := Real.model_structure Rmodel.Implicit Type m : map R.
Rmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map R
finite_simple_map (R:=R) m ->
colorable_with (R:=R) 4 m
Rmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map R
finite_simple_map (R:=R) m ->
colorable_with (R:=R) 4 m
Rmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map R
fin_m: finite_simple_map (R:=R) m
colorable_with (R:=R) 4 m
Rmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map R
fin_m: finite_simple_map (R:=R) m
G: hypermap.hypermap
planarG: geometry.planar_bridgeless G
colG: coloring.four_colorable G ->
colorable_with (R:=Real.model_structure Rmodel)
 4 m
colorable_with (R:=R) 4 m
exact (colG (combinatorial4ct.four_color_hypermap planarG)).Qed.
Rmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map R
simple_map (R:=R) m -> colorable_with (R:=R) 4 m
Rmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map R
simple_map (R:=R) m -> colorable_with (R:=R) 4 m
revert m; exact (finitize.compactness_extension four_color_finite).Qed.End FourColorTheorem.
Homotopy Type Theory
Set Universe Polymorphism.
(* Equivalences *)

Class IsEquiv {A : Type} {B : Type} (f : A -> B) := BuildIsEquiv {
 e_inv : B -> A ;
 e_sect : forall x, e_inv (f x) = x;
 e_retr : forall y, f (e_inv y) = y;
 e_adj : forall x : A, e_retr (f x) = ap f (e_sect x);
}.

(** A class that includes all the data of an adjoint equivalence. *)
Class Equiv A B := BuildEquiv {
 e_fun : A -> B ;
 e_isequiv :> IsEquiv e_fun
}.
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
isretr (f a) = ap f (issect' f g issect isretr a)
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
isretr (f a) = ap f (issect' f g issect isretr a)
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
isretr (f a) =
ap f
 ((ap g (ap f (issect a)^) @ ap g (isretr (f a))) @
 issect a)
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
eq_refl =
ap f
 ((ap g (ap f (issect a)^) @ ap g (isretr (f a))) @
 issect a) @ (isretr (f a))^
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
eq_refl =
((ap f (ap g (ap f (issect a)^)) @
 ap f (ap g (isretr (f a)))) @ 
 ap f (issect a)) @ (isretr (f a))^
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
(ap f (issect a) @ (isretr (f a))^)
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
(ap f (issect a) @ (isretr (f a))^)
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
eq_refl = ?y
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
?y =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
(ap f (issect a) @ (isretr (f a))^)
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
?y =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
(ap f (issect a) @ (isretr (f a))^)
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
?x =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
ap f (ap g (isretr (f a)))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
?x' = ap f (issect a) @ (isretr (f a))^
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
?x' = ap f (issect a) @ (isretr (f a))^
exact e.
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
((fun b : B => (isretr b)^) (f (g (f a))) @
 ap (fun b : B => f (g b)) (ap f (issect a)))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a)))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a)))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a)))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a))))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0:= concat_A1p (fun b : B => isretr b) (isretr (f a)): ap (fun x : B => f (g x)) (isretr (f a)) @
(fun b : B => isretr b) (f a) =
(fun b : B => isretr b) (f (g (f a))) @
isretr (f a)
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a))))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap (fun x : B => f (g x)) (isretr (f a)) =
(isretr (f (g (f a))) @ isretr (f a)) @
(isretr (f a))^
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a))))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap (fun x : B => f (g x)) (isretr (f a)) =
isretr (f (g (f a))) @
(isretr (f a) @ (isretr (f a))^)
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a))))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap (fun x : B => f (g x)) (isretr (f a)) =
isretr (f (g (f a))) @ eq_refl
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a))))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap (fun x : B => f (g x)) (isretr (f a)) =
isretr (f (g (f a)))
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a))))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a))))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
eq_refl = ?y
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?y =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a))))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?y =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a))))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x = ap (fun x : B => f (g x)) (ap f (issect a)^)
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x' =
ap f (ap g (isretr (f a))) @
((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a)))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x' =
ap f (ap g (isretr (f a))) @
((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a)))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x' =
(ap f (ap g (isretr (f a))) @ (isretr (f (g (f a))))^) @
ap (fun b : B => f (g b)) (ap f (issect a))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x' = ?y
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?y =
(ap f (ap g (isretr (f a))) @ (isretr (f (g (f a))))^) @
ap (fun b : B => f (g b)) (ap f (issect a))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?y =
(ap f (ap g (isretr (f a))) @ (isretr (f (g (f a))))^) @
ap (fun b : B => f (g b)) (ap f (issect a))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x =
ap f (ap g (isretr (f a))) @ (isretr (f (g (f a))))^
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x'0 = ap (fun b : B => f (g b)) (ap f (issect a))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x = ?y
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?y =
ap f (ap g (isretr (f a))) @ (isretr (f (g (f a))))^
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x'0 = ap (fun b : B => f (g b)) (ap f (issect a))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?y =
ap f (ap g (isretr (f a))) @ (isretr (f (g (f a))))^
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x0 = ap f (ap g (isretr (f a)))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x'1 = (isretr (f (g (f a))))^
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
ap f (ap g (isretr (f a))) = ?x0
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x'1 = (isretr (f (g (f a))))^
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x'1 = (isretr (f (g (f a))))^
reflexivity.
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x = isretr (f (g (f a))) @ (isretr (f (g (f a))))^
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x'0 = ap (fun b : B => f (g b)) (ap f (issect a))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
isretr (f (g (f a))) @ (isretr (f (g (f a))))^ = ?x
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x'0 = ap (fun b : B => f (g b)) (ap f (issect a))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x'0 = ap (fun b : B => f (g b)) (ap f (issect a))
reflexivity.
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x' =
eq_refl @ ap (fun b : B => f (g b)) (ap f (issect a))
reflexivity.
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(eq_refl @ ap (fun b : B => f (g b)) (ap f (issect a)))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
eq_refl =
ap (fun x : A => f (g (f x))) (issect a)^ @
(eq_refl @ ap (fun x : A => f (g (f x))) (issect a))
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
eq_refl =
ap (fun x : A => f (g (f x))) (issect a)^ @
ap (fun x : A => f (g (f x))) (issect a)
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
ap (fun x : A => f (g (f x))) (issect a)^ @
ap (fun x : A => f (g (f x))) (issect a) = eq_refl
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
ap (fun x : A => f (g (f x))) (issect a)^ @
ap (fun x : A => f (g (f x))) (issect a) = 
?y
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?y = eq_refl
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
ap (f ∘ g) ∘ f ((issect a)^ @ issect a) = eq_refl
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
 (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
ap (fun x : A => f (g (f x))) eq_refl = eq_refl
reflexivity.Defined.Definition isequiv_adjointify {A B : Type} (f : A -> B) (g : B -> A)
 (issect : g∘ f == id) (isretr : f ∘ g == id) : IsEquiv f
 := BuildIsEquiv A B f g (issect' f g issect isretr) isretr
 (is_adjoint' f g issect isretr).

EXTENSIBILITY AND CUSTOMIZABILITY
Elaboration, Metaprogramming and Embedded Domain-Specific Logics and Languages

Developing formal proofs and verified programs often requires extending the core language with domain-specific notations, proof strategies and application-specific structures. The Rocq Prover provides many mechanisms to tailor the environment to one's requirements and structure developments. Rocq comes with a built-in lightweight scoped notation system, a coercion system and typeclass systems that allow user-defined extension of the elaboration phases. This support is essential for developing embedded domain-specific logics and languages, as exemplified in the Iris project which allows to reason about effectful programs in languages like Rust using sophisticated variants of separation logic.

PERFORMANCE
Fast Proof Checker

The Rocq Prover offers a finely-tuned proof engine and kernel implementation allowing large-scale formalization, with efficient bytecode and native conversion checkers relying on the OCaml runtime. It can also interoperate with code written in other languages thanks to its unique extraction facilities.

Releases

Recent Releases

Rocq Prover 9.2.0 (2026-03-27)

  • Reenable support for native_compute when compiled with OCaml 5. As it relies on some architecture-specific code, only some x86 setups are supported for now
  • Records in Type and Prop, with only fields in SProp, can now have primitive projections but without eta conversion.
  • Implicit elaboration of elimination constraints
  • Parsing of elimination constraints in prenex polymorphic definitions as well as in constraints declaration Constraint s1 -> s2.
  • Induction hypotheses are now generated for nested arguments provided an All predicate, and a theorem to prove it, have been registered with the keys All and AllForall.
  • Add a Scheme All command to generate the All predicate and its theorem for inductive types used for the eliminators of nested inductive types
  • Tactics such as induction find eliminators (like nat_rect) through the Register Scheme table (which is automatically populated by Scheme and automatic scheme declarations) instead of by name (the lookup by name remains for now for backward compatibility)
  • attribute schemes to control automatic scheme declaration.
  • Goal names can be automatically generated for induction, destruct and eapply by using the Generate Goal Names flag
  • congruence tactics now handle primitive ints, floats and strings
  • Ltac2 Custom Entry making it possible to define more complex Ltac2 Notations and many other additions to Ltac2 (see below for details).
  • Printing Fully Qualified to print all names (global references, modules, module types, universes, etc) using fully qualified paths
  • Generalized universe polymorphism flag structure (ML API change)

Rocq Platform 2025.08.3 (2026-03-19)

  • For Rocq 9.0
  • Coq 8.12.2-8.20.1 available

Rocq Platform 2025.08.2 (2026-02-24)

  • For Rocq 9.0
  • Coq 8.12.2-8.20.1 available
See All Releases

Changelog

Releases & Updates

Rocq Prover and Rocq Platform

Release of Rocq 9.2.0

We are happy to announce that Rocq 9.2.0 has been released. The main changes are: - Reenable suppo...

See full changelog
Release of Rocq 9.1.1

We have the pleasure of announcing the first patch release of Rocq 9.1.1. The main changes are: ...

See full changelog
Release of Rocq 9.1

We have the pleasure of announcing the first release of Rocq 9.1. The main changes are: - Fixed ...

See full changelog
See Full Changelog

Users of Rocq

Rocq is used by hundreds of developers, companies, research labs, teachers, and more. Learn how it fits your use case.

For Educators

With its mathematical roots, the Rocq Prover has always had strong ties to academia. It is taught in universities around the world, and has accrued an ever-growing body of research. Learn more about the academic rigor that defines the culture of Rocq.

Learn more

For Industrial Users

Rocq's strong correctness guarantees and high performance empower companies to provide reliable services and products. Learn more about how Rocq is used in the industry.

Learn more

Curated Resources

Get up to speed quickly to enjoy the benefits of the Rocq Prover across your projects.

Rocq Packages

Explore hundreds of open-source Rocq packages with their documentation.

Explore packages