Rocq logo

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

Install About The Rocq Prover Why Rocq?
Latest Rocq Prover release: 8.20.0
Latest Rocq Platform release: 2024.10.1

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. 
Definition square x := x * x.

= 9
: nat

Fixpoint fac n :=
  match n with
  | 0 | 1 => 1
  | S n' => n * fac n'
  end.

= 120
: nat


forall n : nat, n > 0 -> square n > 0


forall n : nat, n > 0 -> square n > 0

   
0 > 0 -> square 0 > 0
n: nat
IHn: n > 0 -> square n > 0
S n > 0 -> square (S n) > 0

   
0 > 0 -> square 0 > 0
 trivial.
   
n: nat
IHn: n > 0 -> square n > 0
S n > 0 -> square (S n) > 0
 now unfold square; lia.
Qed.
Try the Playground

Trusted in Academia and Industry

These organisations and companies rely on Rocq every day — along with hundreds of other researchers and engineers.
Inria
Université de Paris
Collège de France
University of Pennsylvania
MIT Massachusetts Institute of Technology
Max Planck Institute for Software Systems
Arhus University
AbsInt
BlueRock
Formal Vindication
Google

The Rocq Prover has been recognised by the ACM for their prestigious SIGPLAN Programming Languages Software and Software System Awards.

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.
Read more

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.

trustworthy

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.

[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).
Iris Proof Script
Iris Proof Goal

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 effectul 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 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

Coq 8.20.0 (2024-09-04)

  • User-defined rewrite rules
  • Primitive strings
  • A lot of work went into reducing the size of the bytecode segment, which in turn means that .vo files might now be considerably smaller.
  • A new version of the docker-keeper compiler to build and maintain Docker images of Coq.
See All Releases

Changelog

Releases & Updates

Rocq Prover and Rocq Platform

Preview of rocq-prover.org, open for contributions

Release of Coq 8.20.0

We have the pleasure of announcing the release of Coq 8.20.0. The full list of changes is availabl...

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.

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 Rocq books from expert programmers and researchers - from 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.

Explore packages