Merge branch 'mathcomp-2.0.0'

.circleci/config.yml

@@ -18,10 +18,10 @@ commands:
     parameters:
       mathcomp-version:
         type: string
-        default: 1.13.0
+        default: 2.0.0
       deriving-version:
         type: string
-        default: 0.1.0
+        default: 0.2.0
     steps:
     - run:
         name: Install dependencies
@@ -42,72 +42,27 @@ commands:
           opam install --with-test .
 
 jobs:
-  coq-8-11:
-    <<: *defaults
-    steps:
-    - startup
-    - prepare
-    - build
-    docker:
-    - image: coqorg/coq:8.11
-
-  coq-8-12:
-    <<: *defaults
-    steps:
-    - startup
-    - prepare
-    - build
-    docker:
-    - image: coqorg/coq:8.12
-
-  coq-8-13:
-    <<: *defaults
-    steps:
-    - startup
-    - prepare
-    - build
-    docker:
-    - image: coqorg/coq:8.13
-
-  coq-8-14:
-    <<: *defaults
-    steps:
-    - startup
-    - prepare
-    - build
-    docker:
-    - image: coqorg/coq:8.14
-
-  coq-8-15:
-    <<: *defaults
-    steps:
-    - startup
-    - prepare:
-        mathcomp-version: 1.15.0
-    - build
-    docker:
-    - image: coqorg/coq:8.15
-
-  coq-8-16:
+  coq-8-17:
     <<: *defaults
     steps:
     - startup
     - prepare:
-        mathcomp-version: 1.16.0
+        mathcomp-version: 2.0.0
+        deriving-version: 0.2.0
     - build
     docker:
-    - image: coqorg/coq:8.16
+    - image: coqorg/coq:8.17
 
-  coq-8-17:
+  coq-8-18:
     <<: *defaults
     steps:
     - startup
     - prepare:
-        mathcomp-version: 1.16.0
-        deriving-version: 0.1.1
+        mathcomp-version: 2.0.0
+        deriving-version: 0.2.0
     - build
     docker:
-    - image: coqorg/coq:8.17
+    - image: coqorg/coq:8.18
 
   coq-dev:
     <<: *defaults
@@ -124,11 +79,6 @@ jobs:
 workflows:
   build:
     jobs:
-    - coq-8-11
-    - coq-8-12
-    - coq-8-13
-    - coq-8-14
-    - coq-8-15
-    - coq-8-16
     - coq-8-17
+    - coq-8-18
     - coq-dev

CHANGELOG.md

@@ -2,15 +2,40 @@
 
 ## Added
 
+## Changed
+
+## Deprecated
+
+## Fixed
+
+## Removed
+
+# 0.4.0 (2023/09/25)
+
+## Added
+
 - Infix notations for `fsubset` (`:<=:`) and `fdisjoint` (`:#:`).
 
 ## Changed
 
+- Use Hierarchy Builder to define the ordType interface.
+
+- `ordMixin` has been replaced with `hasOrd`
+
 - Use maximally implicit arguments for the type arguments of `getm`, `setm`,
   `repm`, `updm`, `mapim`, `mapm`, `filterm`, `remm`, `mkfmap`, `mkfmapf`,
   `mkfmapfp` and `domm`.
 
-## Removed
+## Deprecated
+
+- `InjOrdMixin`, `PcanOrdMixin` and `CanOrdMixin` have been deprecated in favor
+  of `InjHasOrd`, `PcanHasOrd` and `CanHasOrd`.
+
+- The `[ordMixin of T by <:]` notation has been deprecated in favor of `[Ord of
+  T by <:]`.
+
+- The `[derive [<flag>] ordMixin for T]` notations have been deprecated in favor
+  of `[derive [<flag>] hasOrd for T]`.
 
 ## Fixed
 

README.md

@@ -75,9 +75,9 @@ After installing OPAM and adding the Coq archive, run:
 Alternatively, you can compile the package by hand.  You'll need the following
 dependencies:
 
-- Coq v8.11 -- v8.15
-- [Ssreflect][2] v1.12 -- v1.15 (`coq-mathcomp-ssreflect` on OPAM).
-- `deriving` v0.1 (https://github.com/arthuraa/deriving)
+- Coq v8.17 -- v8.18
+- [Ssreflect][2] v2.0 (`coq-mathcomp-ssreflect` on OPAM).
+- `deriving` v0.2 (https://github.com/arthuraa/deriving)
 
 To compile the package, simply run
 

extructures.opam

@@ -19,9 +19,9 @@ install: [
 ]
 depends: [
   "ocaml"
-  "coq" {(>= "8.11" & < "8.18~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.12")}
-  "coq-deriving" {(>= "0.1")}
+  "coq" {(>= "8.17" & < "8.19~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "2.0.0") | (= "dev")}
+  "coq-deriving" {(>= "0.2.0") | (= "dev")}
 ]
 tags: [
   "keyword:finite maps"

flake.nix

@@ -0,0 +1,41 @@
+{
+  description = ''
+    Finite sets, maps, and other data structures with extensional reasoning
+  '';
+
+  inputs.flake-utils.url = "github:numtide/flake-utils";
+
+  inputs.deriving.url = "github:arthuraa/deriving/v0.2.0";
+  inputs.deriving.inputs.nixpkgs.follows = "nixpkgs";
+  inputs.deriving.inputs.flake-utils.follows = "flake-utils";
+
+  outputs = { self, nixpkgs, flake-utils, deriving }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let pkgs = nixpkgs.legacyPackages.${system};
+          derivingSrc = deriving;
+          lib = pkgs.lib; in rec {
+            packages = rec {
+              coq = pkgs.coq_8_17;
+              coqPackages = pkgs.coqPackages_8_17.overrideScope' (self: super:
+                { mathcomp = super.mathcomp.override {
+                    version = "2.0.0";
+                  };
+                  deriving = super.deriving.overrideAttrs (s: {
+                    version = "0.2.0";
+                    src = derivingSrc;
+                  });
+                });
+              ocaml = pkgs.ocaml;
+            };
+
+            devShell = pkgs.mkShell {
+              packages = with packages; [
+                coq
+                coqPackages.mathcomp.ssreflect
+                coqPackages.deriving
+                ocaml
+              ];
+            };
+      }
+    );
+}

tests/tutorial.v

@@ -8,6 +8,7 @@ as sets rather than lists. First, we import the main libraries.
 *)
 
 Require Import Coq.Strings.String. (* For atomic formulas *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect.
 From deriving Require Import deriving.
 From extructures Require Import ord fset fmap.
@@ -49,18 +50,20 @@ Notation "A → B" := (Impl A B)
 (**
 
 To store formulas in sets, they need to have an order relation. We use the
-deriving library to define instances of OrdType for the formula type.
+deriving library to define instances of Ord for the formula type.
 
 *)
 
 Definition formula_indDef := [indDef for formula_rect].
 Canonical formula_indType := IndType formula formula_indDef.
-Definition formula_eqMixin := [derive eqMixin for formula].
-Canonical formula_eqType := EqType formula formula_eqMixin.
-Definition formula_choiceMixin := [derive choiceMixin for formula].
-Canonical formula_choiceType := ChoiceType formula formula_choiceMixin.
-Definition formula_ordMixin := [derive ordMixin for formula].
-Canonical formula_ordType := OrdType formula formula_ordMixin.
+Definition formula_hasDecEq := [derive hasDecEq for formula].
+HB.instance Definition _ := formula_hasDecEq.
+Definition formula_hasChoice := [derive hasChoice for formula].
+#[hnf] HB.instance Definition _ := formula_hasChoice.
+Definition formula_hasOrd := [derive hasOrd for formula].
+(* FIXME: This is taking way too long. *)
+#[hnf] HB.instance Definition _ := formula_hasOrd.
+
 
 Notation context := {fset formula}.
 
@@ -202,8 +205,8 @@ Lemma in_eq_formula_den A ρ1 ρ2 :
   {in atoms A, ρ1 =1 ρ2} -> `F⟦A⟧^ρ1 = `F⟦A⟧^ρ2.
 Proof.
 move: {-1}(atoms A) (fsubsetxx (atoms A)) => Xs.
-by elim: A => /= [X|A IHA B IHB|A IHA B IHB|A IHA B IHB] sub ρ12;
-do ?[move: sub; rewrite fsubUset; case/andP => ??];
+by elim: A => /= [X|A IHA B IHB|A IHA B IHB|A IHA B IHB] AXs ρ12;
+do ?[move: AXs; rewrite fsubUset; case/andP => ??];
 rewrite ?ρ12 // ?IHA ?IHB // -fsub1set.
 Qed.
 

theories/ffun.v

@@ -1,3 +1,4 @@
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice seq.
 
 From extructures Require Import ord fset fmap.
@@ -40,7 +41,7 @@ Record ffun := FFun {
 }.
 Arguments FFun _ _ : clear implicits.
 
-Canonical ffun_subType := [subType for ffval].
+HB.instance Definition _ := [isSub of ffun for ffval].
 
 Implicit Types (f g : ffun) (x : T) (y : S).
 
@@ -202,15 +203,9 @@ Qed.
 
 End Mapping.
 
-Definition ffun_eqMixin T (S : eqType) def :=
-  [eqMixin of @ffun T S def by <:].
-Canonical ffun_eqType T S def :=
-  EqType _ (@ffun_eqMixin T S def).
-Definition ffun_choiceMixin T (S : choiceType) def :=
-  [choiceMixin of @ffun T S def by <:].
-Canonical ffun_choiceType T S def :=
-  Eval hnf in ChoiceType _ (@ffun_choiceMixin T S def).
-Definition ffun_ordMixin T (S : ordType) def :=
-  [ordMixin of @ffun T S def by <:].
-Canonical ffun_ordType T S def :=
-  Eval hnf in OrdType _ (@ffun_ordMixin T S def).
+HB.instance Definition _ T (S : eqType) def :=
+  [Equality of @ffun T S def by <:].
+#[hnf] HB.instance Definition _ T (S : choiceType) def :=
+  [Choice of @ffun T S def by <:].
+#[hnf] HB.instance Definition _ T (S : ordType) def :=
+  [Ord of @ffun T S def by <:].