Adapt to Rocq 9.4 and MathComp dev

.github/workflows/coq-action.yml

@@ -15,13 +15,13 @@ jobs:
     strategy:
       matrix:
         image:
-          - mathcomp/mathcomp:2.3.0-coq-8.20
+          - mathcomp/mathcomp:2.6.0-rocq-prover-9.2
       fail-fast: false
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1
       with:
-        opam_file: 'coq-mathcomp-dioid.opam'
+        opam_file: 'rocq-mathcomp-dioid.opam'
         custom_image: ${{ matrix.image }}
         custom_script: |
           startGroup Print opam config
@@ -31,18 +31,18 @@ jobs:
           startGroup Update opam cache
             opam update -y
           endGroup
-          startGroup Build coq-mathcomp-dioid dependencies
-            opam pin add -n -y -k path coq-mathcomp-dioid .
-            opam remove coq-mathcomp-character coq-mathcomp-field coq-mathcomp-solvable # coq-mathcomp-algebra is enough
-            opam install -y -j ${NJOBS} coq-mathcomp-dioid --deps-only
+          startGroup Build rocq-mathcomp-dioid dependencies
+            opam pin add -n -y -k path rocq-mathcomp-dioid .
+            opam remove -y rocq-mathcomp-character rocq-mathcomp-field rocq-mathcomp-solvable # rocq-mathcomp-algebra is enough
+            opam install -y -j ${NJOBS} rocq-mathcomp-dioid --deps-only
             opam list
           endGroup
-          startGroup Build coq-mathcomp-dioid
-            opam install -y -v -j ${NJOBS} coq-mathcomp-dioid
+          startGroup Build rocq-mathcomp-dioid
+            opam install -y -v -j ${NJOBS} rocq-mathcomp-dioid
             opam list
           endGroup
           startGroup Uninstallation test
-            opam remove -y coq-mathcomp-dioid
+            opam remove -y rocq-mathcomp-dioid
           endGroup
 
 # See also:

.gitignore

@@ -1,7 +1,7 @@
 *~
-Makefile.coq
-Makefile.coq.conf
-.Makefile.coq.d
+Makefile.rocq
+Makefile.rocq.conf
+.Makefile.rocq.d
 .*.aux
 *.glob
 *.vo

Makefile

@@ -1,33 +1,33 @@
 # Makefile for dioid
 
 COQ_PROJ := _CoqProject
-COQ_MAKEFILE := Makefile.coq
-COQ_MAKE := +$(MAKE) -f $(COQ_MAKEFILE)
+ROCQ_MAKEFILE := Makefile.rocq
+ROCQ_MAKE := +$(MAKE) -f $(ROCQ_MAKEFILE)
 
-ifneq "$(COQBIN)" ""
-	COQBIN := $(COQBIN)/
+ifneq "$(ROCQBIN)" ""
+	ROCQBIN := $(ROCQBIN)/
 else
-	COQBIN := $(dir $(shell which coqc))
+	ROCQBIN := $(dir $(shell which coqc))
 endif
-export COQBIN
+export ROCQBIN
 
-all install html gallinahtml: $(COQ_MAKEFILE) Makefile
-	$(COQ_MAKE) $@
+all install html gallinahtml: $(ROCQ_MAKEFILE) Makefile
+	$(ROCQ_MAKE) $@
 
 %.vo: %.v
-	$(COQ_MAKE) $@
+	$(ROCQ_MAKE) $@
 
-$(COQ_MAKEFILE): $(COQ_PROJ)
-	$(COQBIN)coq_makefile -f $< -o $@
+$(ROCQ_MAKEFILE): $(COQ_PROJ)
+	$(ROCQBIN)rocq makefile -f $< -o $@
 
 clean:
-	-$(COQ_MAKE) clean
+	-$(ROCQ_MAKE) clean
 
 distclean: clean
-	$(RM) $(COQ_MAKEFILE) $(COQ_MAKEFILE).conf
+	$(RM) $(ROCQ_MAKEFILE) $(ROCQ_MAKEFILE).conf
 	$(RM) *~ .*.aux .lia.cache
 
 
--include $(COQ_MAKEFILE).conf
+-include $(ROCQ_MAKEFILE).conf
 
 .PHONY: all install html gallinahtml clean distclean

README.md

@@ -17,16 +17,15 @@ Installation
 Dependencies
 ------------
 
-* Coq (>= 8.20)
-* The Mathcomp library (>= 2.3.0)
-* Hierarchy Builder (= 1.8.0)
-* Mathcomp classical (= 1.8.0)
+* Rocq (>= 9.2)
+* The Mathcomp library (>= 2.6.0)
+* Mathcomp classical (>= 1.17.0)
 
 Dependencies can be installed with OPAM (>= 2.0) by typing:
 
 ```
 % opam repo add coq-released https://coq.inria.fr/opam/released
-% opam install coq.8.20.1 coq-mathcomp-algebra.2.3.0 coq-mathcomp-classical.1.8.0
+% opam install coq-core.9.0.1 rocq-mathcomp-algebra.2.6.0 rocq-mathcomp-classical
 ```
 
 Compilation

complete_dioid.v

@@ -58,8 +58,8 @@
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Reserved Notation "x ^+" (at level 2, format "x ^+").
-Reserved Notation "x ^*" (at level 2, format "x ^*").
+Reserved Notation "x ^*" (at level 1, left associativity, format "x ^*").
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -68,7 +68,7 @@
 
 Import Order.Theory GRing.Theory.
 
-HB.mixin Record isCompleteDioid d D of Dioid d D & CompleteLattice d D := {
+HB.mixin Record isCompleteDioid d D & Dioid d D & CompleteLattice d D := {
   set_mulDl : forall (a : D) (B : set D),
       a * set_join B = set_join [set a * x | x in B];
   set_mulDr : forall (a : D) (B : set D),
@@ -90,7 +90,7 @@
 Implicit Types a b c : D.
 Implicit Types B : set D.
 
 Notation set_add := set_join.
 
 Lemma bottom_zero : \bot = 0%R :> D.
 Proof. by apply/le_anti; rewrite le0x le0d. Qed.
@@ -253,7 +253,7 @@
 elim=> [ | i IHi]; [by rewrite set_add1 !exp0|].
 rewrite expS mulrDl mul1r IHi set_mulDl.
 set B' := [set a ^ j | j in [set j | (1 <= j <= i)%N]].
-rewrite [X in set_join X](_ : _ = a ^ i.+1 |` B'); last first.
+rewrite [X in set_join X](_ : _ = a ^ i.+1 |` B').
 { rewrite predeqP => x; split.
   - move=> -[y [[j Hj] _ <-] <-].
     rewrite expS /= -!expS.
@@ -263,7 +263,7 @@
     move=> -[[//|j] /andP [Hj Hji] <-]; rewrite expS; exists (a ^ j) => //.
     by move: Hji => /ltnW; rewrite -ltnS => Hji; exists (Ordinal Hji). }
 rewrite -[set_join]/set_add set_addDl.
-rewrite (_ : image _ _ = (1%R |` B')); last first.
+rewrite (_ : image _ _ = (1%R |` B')).
 { rewrite predeqP => x; split.
   { move=> -[[[|j] Hj] _ <-]; [by left; rewrite exp0|].
     by right; exists (Ordinal Hj). }
@@ -286,7 +286,7 @@
 Proof.
 rewrite {1}/op_kleene set_mulDr.
 set B' := (a ^* |` (range (fun i => a ^ i.+1 * a ^*))).
-rewrite (_ : image _ _ = B'); last first.
+rewrite (_ : image _ _ = B').
 { rewrite predeqP => x; split.
   - by move=> -[_ [[|i] _ <-] <-]; [left; rewrite exp0 mul1r|right; exists i].
   - move=> [-> | [i _ <-]]; [by exists 1%R; [exists O|rewrite mul1r]|].
@@ -310,7 +310,7 @@
 Lemma kleene_kleene a : (a ^*) ^* = a ^*.
 Proof.
 rewrite kleeneSr /op_plus.
-rewrite (_ : image _ _ = a ^* |` set0).
+rewrite (_ : image _ _ = a ^* |` set0); last first.
   by rewrite setU0 set_join1 kleeneSr addrA adddd.
 rewrite predeqP => x; split.
 - move=> [i _ <-]; left; exact: kleene_exp.
@@ -324,7 +324,7 @@
 Proof.
 move=> x Hx.
 rewrite set_mulDr.
-rewrite [X in set_join X](_ : _ = [set (a ^ i) * b | i in setT]); last first.
+rewrite [X in set_join X](_ : _ = [set (a ^ i) * b | i in setT]).
   rewrite predeqP => y; split.
   - by move=> [_ [i _ <-] <-]; exists i.
   - by move=> [i _ <-]; exists (a ^ i); [exists i|].
@@ -435,15 +435,15 @@
 
 #[short(type="comCompleteDioidType")]
 HB.structure Definition ComCompleteDioid d :=
-  { D of GRing.ComSemiRing D & CompleteDioid d D }.
+  { D of GRing.ComNzSemiRing D & CompleteDioid d D }.
 
 HB.factory Record isComCompleteDioid d D
-    of ComDioid d D & CompleteLattice d D := {
+    & ComDioid d D & CompleteLattice d D := {
   set_mulDl : forall (a : D) (B : set D),
     a * set_join B = set_join [set a * x | x in B];
 }.
 
-HB.builders Context d D of isComCompleteDioid d D.
+HB.builders Context d D & isComCompleteDioid d D.
 Lemma set_mulDr a (B : set D) :
   set_join B * a = set_join [set x * a | x in B].
 Proof.
@@ -454,7 +454,7 @@
 HB.end.
 
 HB.factory Record CompleteLattice_isComCompleteDioid d D
-    of CompleteLattice d D := {
+    & CompleteLattice d D := {
   zero : D;
   add : D -> D -> D;
   one : D;
@@ -474,7 +474,7 @@
     mul a (set_join B) = set_join [set mul a x | x in B];
 }.
 
-HB.builders Context d D of CompleteLattice_isComCompleteDioid d D.
+HB.builders Context d D & CompleteLattice_isComCompleteDioid d D.
 HB.instance Definition _ := POrder_isComDioid.Build d D
   addA addC add0d adddd mulA mulC mul1d mulDl mul0d oner_neq0 le_def.
 HB.instance Definition _ := isComCompleteDioid.Build d D set_mulDl.
@@ -552,10 +552,10 @@
 
 HB.factory Record SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid
     d (D : completeDioidType d) S d' U
-    of @SubDioid d D S d' U & @JoinSubCompleteLattice d D S d' U := {}.
+    & @SubDioid d D S d' U & @JoinSubCompleteLattice d D S d' U := {}.
 
 HB.builders Context d D S d' U
-  of SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid d D S d' U.
+  & SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid d D S d' U.
 Lemma set_mulDl (a : U) (B : set U) :
   a * set_join B = set_join [set a * x | x in B].
 Proof.
@@ -573,50 +573,50 @@
 
 HB.factory Record SubDioid_SubPOrder_isJoinSubCompleteDioid d
     (D : completeDioidType d) S d' U
-    of @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := {
+    & @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := {
   opredSJ_subproof : set_join_closed S;
 }.
 
 HB.builders Context d D S d' U
-  of SubDioid_SubPOrder_isJoinSubCompleteDioid d D S d' U.
+  & SubDioid_SubPOrder_isJoinSubCompleteDioid d D S d' U.
 HB.instance Definition _ := SubPOrder_isJoinSubCompleteLattice.Build d D S d' U
   opredSJ_subproof.
 HB.instance Definition _ :=
   SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid.Build d D S d' U.
 HB.end.
 
 HB.factory Record SubChoice_isJoinSubCompleteDioid d (D : completeDioidType d)
-    S (d' : Order.disp_t) U of SubChoice D S U := {
+    S (d' : Order.disp_t) U & SubChoice D S U := {
   semiring_closed_subproof : semiring_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
-HB.builders Context d D S d' U of SubChoice_isJoinSubCompleteDioid d D S d' U.
+HB.builders Context d D S d' U & SubChoice_isJoinSubCompleteDioid d D S d' U.
 HB.instance Definition _ := SubChoice_isSubDioid.Build d D S d' U
   semiring_closed_subproof.
 HB.instance Definition _ :=
   SubDioid_SubPOrder_isJoinSubCompleteDioid.Build d D S d' U opredSJ_subproof.
 HB.end.
 
 HB.factory Record SubChoice_isJoinSubComCompleteDioid d
-    (D : comCompleteDioidType d) S (d' : Order.disp_t) U of SubChoice D S U := {
+    (D : comCompleteDioidType d) S (d' : Order.disp_t) U & SubChoice D S U := {
   semiring_closed_subproof : semiring_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
 HB.builders Context d D S d' U
-  of SubChoice_isJoinSubComCompleteDioid d D S d' U.
+  & SubChoice_isJoinSubComCompleteDioid d D S d' U.
 HB.instance Definition _ := SubChoice_isJoinSubCompleteDioid.Build d D S d' U
   semiring_closed_subproof opredSJ_subproof.
 HB.instance Definition _ := GRing.SubSemiRing_isSubComSemiRing.Build D S U.
 HB.end.
 
 HB.factory Record SubDioid_SubCompleteLattice_isSubCompleteDioid
     d (D : completeDioidType d) S d' U
-    of @SubDioid d D S d' U & @SubCompleteLattice d D S d' U := {}.
+    & @SubDioid d D S d' U & @SubCompleteLattice d D S d' U := {}.
 
 HB.builders Context d D S d' U
-  of SubDioid_SubCompleteLattice_isSubCompleteDioid d D S d' U.
+  & SubDioid_SubCompleteLattice_isSubCompleteDioid d D S d' U.
 Lemma set_mulDl (a : U) (B : set U) :
   a * set_join B = set_join [set a * x | x in B].
 Proof.
@@ -634,27 +634,27 @@
 
 HB.factory Record SubDioid_SubPOrder_isSubCompleteDioid d
     (D : completeDioidType d) S d' U
-    of @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := {
+    & @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := {
   opredSM_subproof : set_meet_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
 HB.builders Context d D S d' U
-  of SubDioid_SubPOrder_isSubCompleteDioid d D S d' U.
+  & SubDioid_SubPOrder_isSubCompleteDioid d D S d' U.
 HB.instance Definition _ := SubPOrder_isSubCompleteLattice.Build d D S d' U
   opredSM_subproof opredSJ_subproof.
 HB.instance Definition _ :=
   SubDioid_SubCompleteLattice_isSubCompleteDioid.Build d D S d' U.
 HB.end.
 
 HB.factory Record SubChoice_isSubCompleteDioid d (D : completeDioidType d) S
-    (d' : Order.disp_t) U of SubChoice D S U := {
+    (d' : Order.disp_t) U & SubChoice D S U := {
   semiring_closed_subproof : semiring_closed S;
   opredSM_subproof : set_meet_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
-HB.builders Context d D S d' U of SubChoice_isSubCompleteDioid d D S d' U.
+HB.builders Context d D S d' U & SubChoice_isSubCompleteDioid d D S d' U.
 HB.instance Definition _ := SubChoice_isSubDioid.Build d D S d' U
   semiring_closed_subproof.
 HB.instance Definition _ :=
@@ -663,14 +663,14 @@
 HB.end.
 
 HB.factory Record SubChoice_isSubComCompleteDioid d
-    (D : comCompleteDioidType d) S (d' : Order.disp_t) U of SubChoice D S U := {
+    (D : comCompleteDioidType d) S (d' : Order.disp_t) U & SubChoice D S U := {
   semiring_closed_subproof : semiring_closed S;
   opredSM_subproof : set_meet_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
 HB.builders Context d D S d' U
-  of SubChoice_isSubComCompleteDioid d D S d' U.
+  & SubChoice_isSubComCompleteDioid d D S d' U.
 HB.instance Definition _ := SubChoice_isSubCompleteDioid.Build d D S d' U
   semiring_closed_subproof opredSM_subproof opredSJ_subproof.
 HB.instance Definition _ := GRing.SubSemiRing_isSubComSemiRing.Build D S U.