The MathComp library provides various theories. A theory is abstractly developed using parameters, which are used as the axioms of the theory. Any type T, which can implement the axioms of a theory, can benefit from all the lemmas and notations from the theory. This tutorial is about how to connect your theories with the ones in MathComp using the hierarchy builder (HB).

Installation:

• Coq version 8.18.0 or later.
• MathComp version 2.2.0 or later.

We first propose a working example, then we show the different ways to declare it an eqType. We cover the declaration by transferring and by using factories.

As a working example, we define the prime numbers as natural numbers satisfying a primality test. Next, we show the different options for declaring it an eqType.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

(* nat is already an instance of eqType, we can use eqType's notations and lemmas *)
Variables n m : nat.
Check n == m.
(* n == m : bool *)

Variable is_prime : nat -> bool.
Record prime := mkPrime { p : nat ; p_prime : is_prime p }.
 
(* primes don't have access to eqType's lemmas nor notations, because prime has not been declared an eqType yet. *)
Variable prime1 prime2 : prime.
Fail Check prime1 == prime2.
(* The command has indeed failed with message:
   ...
   The term "prime1" has type "prime" while it is expected to have type
   "Equality.sort ?s". *)

There are two paths for declaring a type to be an eqType: by transferring, that is, connecting the type with another eqType; or by using a factory, and defining and proving the axioms of the theory of eqTypes for your particular type.

The recommended path for declaring an instance is by transferring, but we start using factories since:

1. It is not always possible to transfer.
2. Factories are more pedestrian.

We now describe the general process to declare a MathComp instance using a factory. The overview follows these three steps:

1. Discover the available factories for the theory you are interested in.
2. Check the arguments for the factories.
3. Choose one of the factories, implement the arguments, and call HB using the factory and the arguments.

The command HB.howto T enumerates the available factories for T.

HB.howto eqType.
(* HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): *)
(*     - hasDecEq *)

The output says we have one factory to declare instances of eqType: hasDecEq.

We can discover the arguments of the factory using the command HB.about F.Build, where F is the name of the factory.

HB.about hasDecEq.Build.
(* HB: hasDecEq.Build is a factory constructor (from "./eqtype.v", line 135) *)
(* HB: hasDecEq.Build requires its subject to be already equipped with: *)
(* HB: hasDecEq.Build provides the following mixins: *)
(*     - hasDecEq *)
(* HB: arguments: hasDecEq.Build T [eq_op] eqP *)
(*     - T : Type *)
(*     - eq_op : rel T *)
(*     - eqP : Equality.axiom (T:=T) eq_op *)

The output says that to build an eqType using hasDecEq, we have to provide a type T, an equality operator eq_op: T -> T -> bool, and a proof of Equality axiom (T:=T) eq_op.

It suffices to implement the arguments from the factory and then use them to declare the instance of eqType.

For testing whether two primes are equal, we check that the underlying natural numbers are equal.

Definition eqb_prime (p1 p2 : prime) :=
  match (p1, p2) with
  | (mkPrime p1 _, mkPrime p2 _) => p1 == p2
  end.

Now we have to prove the equality axiom holds for eqb_prime. We need to prove that eqb_prime is correct, i.e. forall x y : prime, eqb_prime x y -> x = y, and that it is complete, i.e. forall x y : prime, x = y -> eqb_prime. Proving completeness is straightforward. For proving correctness, the key ingredient lies in eq_irrelevance : forall [T : eqType] [x y : T] (e1 e2 : x = y), e1 = e2. The lemma says that equality proofs are equal for terms that are eqTypes. Since bool is an eqType, we use eq_irrelevance to prove that p1P and p2P are equal.

Lemma prime_eqDec : Equality.axiom eqb_prime.
Proof.
  move=> [p1 p1P] [p2 p2P]; apply (iffP idP).
  + by move=> /eqP eqp; subst; congr mkPrime; apply eq_irrelevance.
  + by rewrite /eqb_prime=> [[->]]; apply /eqP.
Qed.

Finally, we can declare prime an eqType.

HB.instance Definition _ := hasDecEq.Build prime prime_eqDec.

In this setting, there are three options to transfer the eqType declaration:

1. By injection, if you can provide an injective encoding from prime to an eqType.
2. By subtyping, if the type you want to declare is subtype of an eqType.
3. By providing an encoding and decoding functions, and prove they cancel or partially cancel each other, i.e. provide code : prime -> T, decode : T -> prime, or pdecode : T -> option prime, and prove cancel code decode or pcancel code pdecode.

In this working example, nat is a good candidate for the eqType transfer, but any eqType for which you can provide an injective function to it will work. We have to provide an injective function from prime to nat. We already have one. The function p : prime -> nat, which projects the underlying natural number from a prime, is injective.

Lemma p_inj : injective p.
Proof.
move=> [p1 p1P] [p2 p2P] /= eqp.
by subst; congr mkPrime; apply eq_irrelevance.
Qed.

(* Now we can declare prime an eqType. *)
HB.instance Definition _ := Equality.copy prime (inj_type p_inj).

For boolean sigma types, like prime, the lemma required for injection is already proved given the projection. This lemma can be accessed by declaring the type as a subtype. Since every prime is a nat satisfying more properties and nat is already an eqType, we can declare prime as subtype of nat using isSub.

(* Declare that prime is subtype of nat by showing the fuction p *)
HB.instance Definition _ := [isSub for p].

(* Transfers the eqType from nat to prime by subtyping *)
HB.instance Definition _ := [Equality of prime by <:].

We show below which are the explicit declarations happening under the hood.

Lemma prime_rect : (forall K : prime -> Type,
     (forall (x : nat) (Px : is_prime x), K {| p := x; p_prime := Px |}) ->
     forall u : prime, K u).
Proof. by move=> K kprime [] p pP; apply kprime. Qed.

Lemma mkPrimeK : forall (x : nat) (Px : is_prime x), p {| p := x; p_prime := Px |} = x.
Proof. by []. Qed.

(* We declare primes to be a subtype of natural numbers using isSub factory *)
HB.instance Definition _ := isSub.Build nat is_prime prime prime_rect mkPrimeK.

(* Now we can declare prime an eqType. *)
HB.instance Definition _ := Equality.copy prime (pcan_type valK).

When the type in question is not a boolean sigma type, isSub cannot be used. However, we can declare the instance by providing a more generic encoding system. This system requires the definition of encoding and decoding functions to an eqType. We will again use the natural numbers as the target type. For the encoding, we use p. For the decoding, we define a function which checks whether the input satisfies the primality test. Then, we prove they partially cancel each other.

Definition code_prime : prime -> nat := p.

Definition pdecode_prime (n : nat) : option prime :=
  if insub n : {? x | is_prime x} is Some ss then
    Some (mkPrime _ (valP ss))
  else None.

Lemma code_decodeK : pcancel code_prime pdecode_prime.
Proof.
move=> [n nP] /=.
rewrite /pdecode_prime.
case: (insubP _ _) => [p pP ps |]; last by rewrite nP.
by congr Some; subst; congr mkPrime; apply: eq_irrelevance.
Qed.

Now we can declare prime an eqType.

HB.instance Definition _ := Equality.copy prime (pcan_type code_decodeK).