FeatherFactory

HB comes with a concept of factory, a virtual interface that is compiled down to the real ones.

When the contents of a factory are just one lemma, the following trick may come handy.

We define a type link which is convertible to a new type T but carries, as a dummy argument, a proof that T is linked to some known type xT which is supposedly equipped with some structure. We can then use link to transfer (copy) structure instances for xT on T across the link.

From HB Require Import structures.
Require Import ssreflect ssrfun ssrbool.

Module Feather.

(* We need a hierarchy with a few structure, here we Equality -> Singleton *)
HB.mixin Record HasEqDec T := {
    eqtest : T -> T -> bool;
    eqOK : forall x y, reflect (x = y) (eqtest x y);
}.
HB.structure Definition Equality := { T of HasEqDec T }.

HB.mixin Record IsContractible T of HasEqDec T := {
    def : T;
    all_def : forall x, eqtest x def = true;
}.
HB.structure Definition Singleton := { T of IsContractible T }.

(*
   This is the type which is used as a feather factory.

   - xT plays the role of a rich type,
   - T is a new type linked to xT by some lemma. In this case a very strong
     cancellation lemma canfg
*)
Definition link {xT T : Type} {f : xT -> T} {g : T -> xT}
                (canfg : forall x, f (g x) = x)
              :=
                 T. (* (link canfg) is convertible to T *)

(* We explain HB how to transfer Equality over link *)
Section TransferEQ.

Context {eT : Equality.type} {T : Type} {f : eT -> T} {g : T -> eT}.
Context (canfg : forall x, f (g x) = x).

Definition link_eqtest (x y : T) : bool := eqtest (g x) (g y).

Lemma link_eqOK (x y : T) : reflect (x = y) (link_eqtest x y).
Proof.
rewrite /link_eqtest; case: (eqOK (g x) (g y)) => [E|abs].
  by constructor; rewrite -[x]canfg -[y]canfg E canfg.
by constructor=> /(f_equal g)/abs.
Qed.

(* (link canfg) is now an Equality instance *)
HB.instance Definition link_HasEqDec :=
  HasEqDec.Build (link canfg) link_eqtest link_eqOK.

End TransferEQ.

(* We explain HB how to transfer Singleton over link *)
Section TransferSingleton.

Context {eT : Singleton.type} {T : Type} {f : eT -> T} {g : T -> eT}.
Context (canfg : forall x, f (g x) = x).

Definition link_def : link canfg := f def.

Lemma link_all_def x : eqtest x link_def = true.
Proof.
rewrite /link_def; have /eqOK <- := all_def (g x).
by rewrite canfg; case: (eqOK x x).
Qed.

(* (link canfg) is now a Signleton instance *)
HB.instance Definition _ := IsContractible.Build (link canfg) link_def link_all_def.

End TransferSingleton.

(* We assume a known type B which is both an Equality and a Singleton *)
Axioms B : Type.

Axiom testB : B -> B -> bool.
Axiom testOKB : forall x y, reflect (x = y) (testB x y).
HB.instance Definition _ := HasEqDec.Build B testB testOKB.

Axiom defB : B.
Axiom all_defB : forall x, eqtest x defB = true.
HB.instance Definition _ := IsContractible.Build B defB all_defB.

(* Now we copy all instances from B to A via link *)
Axiom A : Type.
Axiom f : B -> A.
Axiom g : A -> B.
Axiom canfg : forall x, f (g x) = x.

(* We take all the instances up to Singleton on (link canfg) and we copy them
   on A. Recall (link canfg) is convertible to A *)
HB.instance Definition _ := Singleton.copy A (link canfg).

HB.about A. (* both Equality and Singleton have been copied *)

End Feather.