Starting port to HB

.nix/config.nix

@@ -31,14 +31,21 @@
 
   ## select an entry to build in the following `bundles` set
   ## defaults to "default"
-  default-bundle = "8.16";
+  default-bundle = "8.15";
 
   ## write one `bundles.name` attribute set per
   ## alternative configuration
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
   bundles."8.14".coqPackages.coq.override.version = "8.14";
-  bundles."8.15".coqPackages.coq.override.version = "8.15";
+  bundles."8.15".coqPackages = {
+    coq.override.version = "8.15";
+    hierarchy-builder.override.version = "fun_instances";
+    mathcomp.override.version = "CohenCyril:hb-ssrnum";
+    mathcomp-bigenough.override.version = "1.0.1";
+    mathcomp-finmap.override.version = "proux01:hierarchy-builder";
+    mathcomp-real-closed.override.version = "CohenCyril:hierarchy-builder";
+  };
 
   bundles."8.16".coqPackages = {
     coq.override.version = "8.16";
@@ -47,7 +54,7 @@
     mathcomp-bigenough.override.version = "1.0.1";
     mathcomp-finmap.override.version = "1.5.2";
     mathcomp-real-closed.override.version = "1.1.3";
-    mathcomp.override.version = "mathcomp-1.15.0";
+    mathcomp.override.version = "CohenCyril:hb-ssrnum";
   };
 
   bundles."master".coqPackages = {
@@ -65,17 +72,17 @@
   cachix.coq = {};
   cachix.math-comp.authToken = "CACHIX_AUTH_TOKEN";
   cachix.coq-community = {};
-  
+
   ## If you have write access to one of these caches you can
   ## provide the auth token or signing key through a secret
   ## variable on GitHub. Then, you should give the variable
   ## name here. For instance, coq-community projects can use
   ## the following line instead of the one above:
   # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN";
-  
+
   ## Or if you have a signing key for a given Cachix cache:
   # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY"
-  
+
   ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY
   ## are the names of secret variables. They are set in
   ## GitHub's web interface.

theories/boolp.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2015--2018 - Inria                                   *)
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
-
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect.
 
 (******************************************************************************)
@@ -164,7 +164,7 @@ Proof. by move: x (x) y => /propT-> [] []. Qed.
 (* -------------------------------------------------------------------- *)
 Record mclassic := {
   _ : forall (P : Prop), {P} + {~P};
-  _ : forall T, Choice.mixin_of T
+  _ : forall T, HasChoice T
 }.
 
 Lemma choice X Y (P : X -> Y -> Prop) :
@@ -211,7 +211,7 @@ exists (fun (P : pred T) (n : nat) =>
 by exists 0; case: pselect => // -[]; exists x.
 Qed.
 
-Lemma gen_choiceMixin {T : Type} : Choice.mixin_of T.
+Lemma gen_choiceMixin (T : Type) : HasChoice T.
 Proof. by case: classic. Qed.
 
 Lemma pdegen (P : Prop): P = True \/ P = False.
@@ -322,37 +322,31 @@ Proof. by move=> [] []; rewrite ?(trueE, falseE) ?propeqE; tauto. Qed.
 Definition gen_eq (T : Type) (u v : T) := `[<u = v>].
 Lemma gen_eqP (T : Type) : Equality.axiom (@gen_eq T).
 Proof. by move=> x y; apply: (iffP (asboolP _)). Qed.
-Definition gen_eqMixin {T : Type} := EqMixin (@gen_eqP T).
-
-Canonical arrow_eqType (T : Type) (T' : eqType) :=
-  EqType (T -> T') gen_eqMixin.
-Canonical arrow_choiceType (T : Type) (T' : choiceType) :=
-  ChoiceType (T -> T') gen_choiceMixin.
+Definition gen_eqMixin (T : Type) : HasDecEq T :=
+  HasDecEq.Build T (@gen_eqP T).
 
-Definition dep_arrow_eqType (T : Type) (T' : T -> eqType) :=
-  EqType (forall x : T, T' x) gen_eqMixin.
-Definition dep_arrow_choiceClass (T : Type) (T' : T -> choiceType) :=
-  Choice.Class (Equality.class (dep_arrow_eqType T')) gen_choiceMixin.
-Definition dep_arrow_choiceType (T : Type) (T' : T -> choiceType) :=
-  Choice.Pack (dep_arrow_choiceClass T').
+HB.instance Definition _ (T : Type) (T' : T -> eqType) :=
+  gen_eqMixin (forall x : T, T' x).
+HB.instance Definition _ (T : Type) (T' : T -> choiceType) :=
+  gen_choiceMixin (forall x : T, T' x).
 
-Canonical Prop_eqType := EqType Prop gen_eqMixin.
-Canonical Prop_choiceType := ChoiceType Prop gen_choiceMixin.
+HB.instance Definition _ := gen_eqMixin Prop.
+HB.instance Definition _ := gen_choiceMixin Prop.
 
 Section classicType.
 Variable T : Type.
 Definition classicType := T.
-Canonical classicType_eqType := EqType classicType gen_eqMixin.
-Canonical classicType_choiceType := ChoiceType classicType gen_choiceMixin.
+HB.instance Definition _ := gen_eqMixin classicType.
+HB.instance Definition _ := gen_choiceMixin classicType.
 End classicType.
 Notation "'{classic' T }" := (classicType T)
  (format "'{classic'  T }") : type_scope.
 
 Section eclassicType.
 Variable T : eqType.
 Definition eclassicType : Type := T.
-Canonical eclassicType_eqType := EqType eclassicType (Equality.class T).
-Canonical eclassicType_choiceType := ChoiceType eclassicType gen_choiceMixin.
+HB.instance Definition _ := Equality.copy eclassicType T.
+HB.instance Definition _ := gen_choiceMixin eclassicType.
 End eclassicType.
 Notation "'{eclassic' T }" := (eclassicType T)
  (format "'{eclassic'  T }") : type_scope.
@@ -371,7 +365,10 @@ Proof. by apply: canon => T; exists  [eqType of {classic T}]. Qed.
 Lemma Pchoice : canonical Type choiceType.
 Proof. by apply: canon => T; exists [choiceType of {classic T}]. Qed.
 Lemma eqPchoice : canonical eqType choiceType.
-Proof. by apply: canon=> T; exists [choiceType of {eclassic T}]; case: T. Qed.
+Proof. 
+apply: canon => T; exists [choiceType of {eclassic T}].
+by case: T => //= T [?]//.
+Qed.
 
 Lemma not_True : (~ True) = False. Proof. exact/propext. Qed.
 Lemma not_False : (~ False) = True. Proof. by apply/propext; split=> _. Qed.
@@ -715,6 +712,7 @@ move=> g f h /asboolP fg /asboolP gh; apply/asboolP => x.
 by rewrite (le_trans (fg x)).
 Qed.
 
+HB.instance Definition := 
 Definition porderMixin :=
   @LePOrderMixin _ lef ltf ltf_def lef_refl lef_anti lef_trans.
 

theories/mathcomp_extra.v

@@ -3,7 +3,6 @@ From mathcomp Require choice.
 (* Missing coercion (done before Import to avoid redeclaration error,
    thanks to KS for the trick) *)
 (* MathComp 1.15 addition *)
-Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From mathcomp Require Import finset interval.