Classes should be decomposable into factories with views.

[CohenCyril]

Sometimes, it might be necessary to do a case analysis on a structure, then a class (for example to show subtyping properties as in measurable functions in mathcomp analysis), but this is forbidden because it breaks HB invariant that structures can be remplemented in completely different ways.

In order to do so safely (aside from generating subtyping interfaces in HB), we may provide custom elimination lemmas.

E.g.

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

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module State1.

HB.mixin Record M T := { m1 : bool; m2 : bool}.
HB.structure Definition S := { T of M T }.

(* Should generate automatically *)
Definition Spack x c := @S.Pack x c.
Definition SpackP P :
    (forall x (c : S x), P (@Spack x c)) ->
    forall x : S.type, P x :=
  fun p x => match x with @S.Pack _ c => p _ c end.

(* and *)
Definition S_of_M x (m : M x) : S x := @S.Class x m.
Definition S_of_M_P x (P : S x -> Type) :
    (forall m, P (@S_of_M x m)) -> forall (c : S x), P c :=
  fun p c => p c.

(* relies on coercion *)
Check fun T => id : S T -> M T.

(* so that we can do *)
Lemma test P (x : S.type) : P x.
Proof.
elim/SpackP: x => x; elim/S_of_M_P => m.
Abort.

End State1.

Module State2.

HB.mixin Record M1 T := { m1 : unit }.
HB.mixin Record M2 T := { m2 : unit }.
HB.factory Record M T := { m1 : unit; m2 : unit }.
HB.builders Context T of M T.
  HB.instance Definition _ := M1.Build T m1.
  HB.instance Definition _ := M2.Build T m2.
HB.end.
HB.structure Definition S := { T of M T }.

(* The coercion from the class S to factory M disapeared *)
Fail Check fun T => id : S T -> M T.

(*
We should provide e.g.

HB.cobuilders Context T of S T.
  HB.instance Definition _ := M.Build T.
HB.end

That syntetises the following coercions:
*)

Definition type_subst_subdef {B} (proj : B -> Type) T' T (e : T = proj T') :
  forall P, P (proj T') -> P T :=  match e with erefl => fun p => id end.
Notation type_subst T' := (@type_subst_subdef _ id T' _ erefl).

Coercion S_to_M x (s : S x) : M x.
Proof.
pose x' : S.type := HB.pack x s; elim/(type_subst x'): (x); move: x' => {s}x.
constructor.
  exact (@m1 x).
  exact (@m2 x).
Defined.
Check fun T => id : S T -> M T.
 

(* Should generate automatically *)
Definition Spack x c := @S.Pack x c.
Definition SpackP P :
    (forall x (c : S x), P (@Spack x c)) ->
    forall x : S.type, P x :=
  fun p x => match x with @S.Pack _ c => p _ c end.

(* and *)
Definition S_of_M x (m : M x) : S x.
Proof.
pose x' : S.type := HB.pack x m; elim/(type_subst x'): (x); move: x' => {m}x.
exact: S.class.
Defined.
(* and *)
Definition S_to_MK x (c : S x) : S_of_M c = c.
Proof.
by case: c; do ![let x := fresh "x_" in case=> [^ x]].
Defined.
(* Which relies on the coercion *)
Check fun T => id : S T -> M T.
(* and *)
Definition S_of_M_P x (P : S x -> Type) :
    (forall m, P (@S_of_M x m)) -> forall (c : S x), P c.
Proof. by move=> p c; rewrite -[c]S_to_MK; exact/p. Qed.

(* so that we can do again *)
Lemma test P (x : S.type) : P x.
Proof.
elim/SpackP: x => x; elim/S_of_M_P => m.
Abort.

End State2.