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. We can then use "link" to transfer (copy) structure instances 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.