Merge pull request #42 from proux01/hierarchy-builder

Port to Hierarchy Builder

Author: CohenCyril

.github/workflows/ci.yml

@@ -8,24 +8,11 @@ jobs:
     strategy:
       matrix:
         image:
-          - coqorg/coq:8.13-native-ocaml-4.07 # with the coq-native opam pkg
-          - coqorg/coq:8.17-native-ocaml-4.13-flambda # with the coq-native opam pkg
-          - mathcomp/mathcomp:1.13.0-coq-8.13 # (without coq-native for now)
-          - mathcomp/mathcomp:1.13.0-coq-8.14 # (without coq-native for now)
-          - mathcomp/mathcomp:1.13.0-coq-8.15 # (without coq-native for now)
-          - mathcomp/mathcomp:1.15.0-coq-8.13
-          - mathcomp/mathcomp:1.15.0-coq-8.16
-          - mathcomp/mathcomp:1.16.0-coq-8.13
-          - mathcomp/mathcomp:1.16.0-coq-8.14
-          - mathcomp/mathcomp:1.16.0-coq-8.15
-          - mathcomp/mathcomp:1.16.0-coq-8.16
-          - mathcomp/mathcomp:1.16.0-coq-8.17
-          - mathcomp/mathcomp:1.17.0-coq-8.17
-          - mathcomp/mathcomp-dev:coq-8.15 # (without coq-native for now)
-          - mathcomp/mathcomp-dev:coq-8.16 # (without coq-native for now)
-          - mathcomp/mathcomp-dev:coq-8.17 # (without coq-native for now)
-          - mathcomp/mathcomp-dev:coq-dev # (without coq-native for now)
-          # the previous comments refer to https://github.com/coq/ceps/pull/48
+          - mathcomp/mathcomp:2.0.0-coq-8.16
+          - mathcomp/mathcomp:2.0.0-coq-8.17
+          - mathcomp/mathcomp-dev:coq-8.16
+          - mathcomp/mathcomp-dev:coq-8.17
+          - mathcomp/mathcomp-dev:coq-dev
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

Makefile

@@ -12,5 +12,8 @@ default: build
 build:
 	$(DUNE) build
 
+install:
+	$(DUNE) install
+
 clean:
 	$(DUNE) clean

coq-mathcomp-multinomials.opam

@@ -10,12 +10,12 @@ build: [
   [ "dune" "build" "-p" name "-j" jobs ]
 ]
 depends: [
-  "coq"                    {(>= "8.13" & < "8.18~") | = "dev"}
+  "coq"                    {(>= "8.16" & < "8.18~") | = "dev"}
   "dune"                   {>= "2.8"}
-  "coq-mathcomp-ssreflect" {(>= "1.13" & < "1.18~") | = "dev"}
+  "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.1~") | = "dev"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-bigenough" {(>= "1.0" & < "1.1~") | = "dev"}
-  "coq-mathcomp-finmap"    {(>= "1.5" & < "1.6~") | = "dev"}
+  "coq-mathcomp-finmap"    {(>= "2.0" & < "2.1~") | = "dev"}
 ]
 tags: [
   "keyword:multinomials"

src/freeg.v

@@ -23,6 +23,7 @@
 (***********************************************************************)
 
 (* -------------------------------------------------------------------- *)
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import fintype bigop order generic_quotient.
 From mathcomp Require Import ssralg ssrnum ssrint.
@@ -70,13 +71,8 @@ Module FreegDefs.
     Lemma prefreeg_uniq (D : prefreeg) : uniq [seq zx.2 | zx <- D].
     Proof. exact/reduced_uniq/prefreeg_reduced. Qed.
 
-    Canonical prefreeg_subType := [subType for seq_of_prefreeg].
-
-    Definition prefreeg_eqMixin := Eval hnf in [eqMixin of prefreeg by <:].
-    Canonical  prefreeg_eqType  := Eval hnf in EqType _ prefreeg_eqMixin.
-
-    Definition prefreeg_choiceMixin := Eval hnf in [choiceMixin of prefreeg by <:].
-    Canonical  prefreeg_choiceType  := Eval hnf in ChoiceType prefreeg prefreeg_choiceMixin.
+    #[export] HB.instance Definition _ := [isSub for seq_of_prefreeg].
+    #[export] HB.instance Definition _ := [Choice of prefreeg by <:].
   End Defs.
 
   Arguments mkPrefreeg [G K].
@@ -100,15 +96,15 @@ Module FreegDefs.
 
     Notation "{ 'freeg' K / G }" := (type_of (Phant G) (Phant K)).
 
-    Canonical freeg_quotType   := [quotType of type].
-    Canonical freeg_eqType     := [eqType of type].
-    Canonical freeg_choiceType := [choiceType of type].
-    Canonical freeg_eqQuotType := [eqQuotType equiv of type].
+    #[export] HB.instance Definition _ := Quotient.on type.
+    #[export] HB.instance Definition _ := Choice.on type.
+    #[export] HB.instance Definition _ : EqQuotient _ equiv type :=
+      EqQuotient.on type.
 
-    Canonical freeg_of_quotType   := [quotType of {freeg K / G}].
-    Canonical freeg_of_eqType     := [eqType of {freeg K / G}].
-    Canonical freeg_of_choiceType := [choiceType of {freeg K / G}].
-    Canonical freeg_of_eqQuotType := [eqQuotType equiv of {freeg K / G}].
+    #[export] HB.instance Definition _ := Quotient.on {freeg K / G}.
+    #[export] HB.instance Definition _ := Choice.on {freeg K / G}.
+    #[export] HB.instance Definition _ : EqQuotient _ equiv {freeg K / G} :=
+      EqQuotient.on {freeg K / G}.
   End Quotient.
 
   Module Exports.
@@ -117,18 +113,7 @@ Module FreegDefs.
     Canonical prefreeg_equiv.
     Canonical prefreeg_equiv_direct.
 
-    Canonical prefreeg_subType.
-    Canonical prefreeg_eqType.
-    Canonical prefreeg_choiceType.
-    Canonical prefreeg_equiv.
-    Canonical freeg_quotType.
-    Canonical freeg_eqType.
-    Canonical freeg_choiceType.
-    Canonical freeg_eqQuotType.
-    Canonical freeg_of_quotType.
-    Canonical freeg_of_eqType.
-    Canonical freeg_of_choiceType.
-    Canonical freeg_of_eqQuotType.
+    HB.reexport.
 
     Notation prefreeg   := prefreeg.
     Notation fgequiv    := equiv.
@@ -559,14 +544,14 @@ Module FreegZmodType.
       by rewrite !rw /= addrC subrr.
     Qed.
 
-    Definition freeg_zmodMixin := ZmodMixin addmA addmC addm0 addmN.
-    Canonical  freeg_zmodType  := ZmodType {freeg K / R} freeg_zmodMixin.
+    #[export] HB.instance Definition _ := GRing.isZmodule.Build {freeg K / R}
+      addmA addmC addm0 addmN.
   End Defs.
 
   Module Exports.
     Canonical pi_fgadd_morph.
     Canonical pi_fgopp_morph.
-    Canonical freeg_zmodType.
+    HB.reexport.
   End Exports.
 End FreegZmodType.
 
@@ -595,9 +580,11 @@ Section FreegZmodTypeTheory.
 
   (* -------------------------------------------------------------------- *)
   Lemma coeff_is_additive x : additive (coeff x).
-  Proof. exact: lift_is_additive [lalgType R of R^o] _. Qed.
+  Proof. exact: lift_is_additive R^o _. Qed.
 
-  Canonical coeff_additive x := Additive (coeff_is_additive x).
+  #[export] HB.instance Definition _ x :=
+    GRing.isAdditive.Build {freeg K / R} R (coeff x)
+      (coeff_is_additive x).
 
   Lemma coeff0   z   : coeff z 0 = 0               . Proof. exact: raddf0. Qed.
   Lemma coeffN   z   : {morph coeff z: x / - x}    . Proof. exact: raddfN. Qed.
@@ -803,10 +790,8 @@ Section FreeglModType.
     by apply/eqP/freeg_eqP=> x; rewrite !(coeffD, coeff_fgscale) mulrDl.
   Qed.
 
-  Definition freeg_lmodMixin :=
-    LmodMixin fgscaleA fgscale1r fgscaleDr fgscaleDl.
-  Canonical freeg_lmodType :=
-    Eval hnf in LmodType R {freeg K / R} freeg_lmodMixin.
+  HB.instance Definition _ := GRing.Zmodule_isLmodule.Build R {freeg K / R}
+    fgscaleA fgscale1r fgscaleDr fgscaleDl.
 End FreeglModType.
 
 (* -------------------------------------------------------------------- *)
@@ -850,10 +835,12 @@ Section Deg.
 
   Definition predeg (D : seq (int * K)) := \sum_(kx <- D) kx.1.
 
-  Lemma deg_is_additive : additive deg.
-  Proof. exact: lift_is_additive K [lalgType int of int^o] _. Qed.
+  Lemma deg_is_additive: additive deg.
+  Proof. exact: (@lift_is_additive _ K int^o). Qed.
 
-  Canonical deg_additive := Additive deg_is_additive.
+  #[export] HB.instance Definition _ :=
+    GRing.isAdditive.Build {freeg K / int} int deg
+      deg_is_additive.
 
   Lemma deg0     : deg 0 = 0               . Proof. exact: raddf0. Qed.
   Lemma degN     : {morph deg: x / - x}    . Proof. exact: raddfN. Qed.