| CARVIEW |
Select Language
HTTP/1.1 200 OK
Server: nginx
Date: Mon, 29 Dec 2025 23:06:22 GMT
Content-Type: text/html; charset=utf-8
Content-Length: 41015
Connection: keep-alive
Content-Encoding: gzip
Strict-Transport-Security: max-age=63072000; includeSubDomains
Content-Security-Policy: frame-ancestors 'self' https://rocq-prover.org *.rocq-prover.org *.inria.fr
X-Frame-Options: SAMEORIGIN
X-Content-Type-Options: nosniff
Referrer-Policy: same-origin
Permissions-Policy: geolocation=(),midi=(),sync-xhr=(),microphone=(),camera=(),magnetometer=(),gyroscope=(),fullscreen=(self),payment=()
Welcome to a World of Rocq
See All Releases
See Full Changelog
Explore packages
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.
Fixpoint fac n := match n with | 0 => 1 | S n' => n * fac n' end.[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]= 120 : natn: natfac (S n) = S n * fac nreflexivity. Qed.n: natfac (S n) = S n * fac nn: natfac n > 0n: natfac n > 0fac 0 > 0n: nat
IHn: fac n > 0fac (S n) > 0fac 0 > 0lia.1 > 0n: nat
IHn: fac n > 0fac (S n) > 0lia. Qed.n: nat
IHn: fac n > 0S n * fac n > 0Extraction Language OCaml.[Loading ML file extraction_plugin.cmxs (using legacy method) ... done](** 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
Mathematical Components
(* (c) Copyright 2006-2018 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From fourcolor Require Import real realplane.(******************************************************************************) (* 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.[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]Rmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map Rfinite_simple_map (R:=R) m -> colorable_with (R:=R) 4 mRmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map Rfinite_simple_map (R:=R) m -> colorable_with (R:=R) 4 mRmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map R
fin_m: finite_simple_map (R:=R) mcolorable_with (R:=R) 4 mexact (colG (combinatorial4ct.four_color_hypermap planarG)). Qed.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 mcolorable_with (R:=R) 4 mRmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map Rsimple_map (R:=R) m -> colorable_with (R:=R) 4 mrevert m; exact (finitize.compactness_extension four_color_finite). Qed. End FourColorTheorem.Rmodel: Real.model
R:= Real.model_structure Rmodel: Real.structure
m: map Rsimple_map (R:=R) m -> colorable_with (R:=R) 4 m
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: Aisretr (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: Aisretr (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: Aisretr (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: Aeq_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: Aeq_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: Aeq_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 = ?yA, 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))^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)?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)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: Aeq_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_refleq_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 = ?yA, 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' = ?yA, 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 = ?yA, 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))) = ?x0A, 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'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 = 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))))^ = ?xA, 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'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))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_reflA, 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) = ?yA, 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_reflA, 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_reflreflexivity. 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).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
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
Coq Platform 2025.01.0 (2025-02-06)
- For Coq 8.20.1
- Coq 8.12.2-8.19.0 available
Coq Platform 2024.10.1 (2024-12-02)
- For Coq 8.19.2
- Coq 8.12.2-8.18.0 available
- Compatibility with opam 2.3.0
Rocq Prover 9.1.0 (2025-09-15)
- Fixed incorrect guard checking leading to inconsistencies
- Sort polymorphic universe instances should now be written as
@{s ; u}instead of@{s | u} - Fixed handling of notation variables for ltac2 in notations (i.e.
Notation "'foo' x" := ltac2:(...)) - Support for
refineattribute inDefinition - Rocq can be compile-time configured to be relocatable
- Extraction handles sort polymorphic definitions
Changelog
Releases & Updates
Rocq Prover and Rocq Platform
We have the pleasure of announcing the first release of Rocq 9. The main changes are: - "The Roc...
See full changelogWe have the pleasure of announcing the release of Coq 8.20.1. The full list of changes is availabl...
See full changelogUsers 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 moreFor 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 moreCurated Resources
Get up to speed quickly to enjoy the benefits of the Rocq Prover across your projects.
Getting Started
Install the Rocq Prover, set up your favorite text editor and start your first project.
Reference Manual
The authoritative reference for the Rocq Prover (not learning oriented).
Books
Discover books on Rocq for both computer science and mathematics - from complete beginner level to advanced topics.
Standard Library
The documentation of the standard library.
Exercises
Learn Rocq by solving problems on a variety of topics, from easy to challenging.
Papers
Explore papers that have influenced or used the Rocq Prover.
Rocq Packages
Explore hundreds of open-source Rocq packages with their documentation.