Generic sets mathcomp2

.github/workflows/docker-action.yml

@@ -17,20 +17,10 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp-dev:coq-8.13'
-          - 'mathcomp/mathcomp-dev:coq-8.14'
-          - 'mathcomp/mathcomp-dev:coq-8.15'
+          - '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:

.gitignore

@@ -1,4 +1,6 @@
 *.vo
+*.vos
+*.vok
 *.glob
 *.v.d
 *.aux

_CoqProject

@@ -1,6 +1,5 @@
 finmap.v
 multiset.v
-set.v
 
 -R . mathcomp.finmap
 -arg -w -arg -projection-no-head-constant

coq-mathcomp-finmap.opam

@@ -21,8 +21,8 @@ which will be used to subsume notations for finite sets, eventually."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev") }
+  "coq" { (>= "8.16" & < "8.18~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.0.0" & < "2.1~") | (= "dev") }
 ]
 
 tags: [

finmap.v

@@ -1,6 +1,7 @@
 (* (c) Copyright 2006-2019 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 
+From HB Require Import structures.
 Set Warnings "-notation-incompatible-format".
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
 Set Warnings "notation-incompatible-format".
@@ -505,11 +506,8 @@ Section FinSetCanonicals.
 
 Variable (K : choiceType).
 
-Canonical fsetType := Eval hnf in [subType for (@enum_fset K)].
-Definition fset_eqMixin := Eval hnf in [eqMixin of {fset K} by <:].
-Canonical fset_eqType := Eval hnf in EqType {fset K} fset_eqMixin.
-Definition fset_choiceMixin := Eval hnf in [choiceMixin of {fset K} by <:].
-Canonical fset_choiceType := Eval hnf in ChoiceType {fset K} fset_choiceMixin.
+HB.instance Definition _ := [isSub for (@enum_fset K)].
+HB.instance Definition _ := [Choice of {fset K} by <:].
 
 End FinSetCanonicals.
 
@@ -526,14 +524,9 @@ Proof. by rewrite canonical_uniq // keys_canonical. Qed.
 Record fset_sub_type : predArgType :=
   FSetSub {fsval : K; fsvalP : in_mem fsval (@mem K _ A)}.
 
-Canonical fset_sub_subType := Eval hnf in [subType for fsval].
-Definition fset_sub_eqMixin := Eval hnf in [eqMixin of fset_sub_type by <:].
-Canonical fset_sub_eqType := Eval hnf in EqType fset_sub_type fset_sub_eqMixin.
-Definition fset_sub_choiceMixin := Eval hnf in [choiceMixin of fset_sub_type by <:].
-Canonical fset_sub_choiceType := Eval hnf in ChoiceType fset_sub_type fset_sub_choiceMixin.
-Definition fset_countMixin (T : countType) := Eval hnf in [countMixin of {fset T} by <:].
-Canonical fset_countType (T : countType) := Eval hnf in CountType {fset T} (fset_countMixin T).
-
+HB.instance Definition _ := [isSub for fsval].
+HB.instance Definition _ := [Choice of fset_sub_type by <:].
+HB.instance Definition _ (T : countType) := [Countable of {fset T} by <:].
 
 Definition fset_sub_enum : seq fset_sub_type :=
   undup (pmap insub (enum_fset A)).
@@ -556,13 +549,10 @@ rewrite /fset_sub_unpickle => x.
 by rewrite (nth_map x) ?nth_index ?index_mem ?mem_fset_sub_enum.
 Qed.
 
-Definition fset_sub_countMixin := CountMixin fset_sub_pickleK.
-Canonical fset_sub_countType := Eval hnf in CountType fset_sub_type fset_sub_countMixin.
-
-Definition fset_sub_finMixin :=
-  Eval hnf in UniqFinMixin (undup_uniq _) mem_fset_sub_enum.
-Canonical fset_sub_finType := Eval hnf in FinType fset_sub_type fset_sub_finMixin.
-Canonical fset_sub_subfinType := [subFinType of fset_sub_type].
+HB.instance Definition _ :=
+  Countable.copy fset_sub_type (pcan_type fset_sub_pickleK).
+HB.instance Definition _ := isFinite.Build fset_sub_type
+  (Finite.uniq_enumP (undup_uniq _) mem_fset_sub_enum).
 
 Lemma enum_fsetE : enum_fset A = [seq val i | i <- enum fset_sub_type].
 Proof. by rewrite enumT unlock val_fset_sub_enum. Qed.
@@ -618,11 +608,8 @@ End SeqFset.
 
 #[global] Hint Resolve keys_canonical sort_keys_uniq : core.
 
-Canonical  finSetSubType K := [subType for (@enum_fset K)].
-Definition finSetEqMixin (K : choiceType) := [eqMixin of {fset K} by <:].
-Canonical  finSetEqType  (K : choiceType) := EqType {fset K} (finSetEqMixin K).
-Definition finSetChoiceMixin (K : choiceType) := [choiceMixin of {fset K} by <:].
-Canonical  finSetChoiceType  (K : choiceType) := ChoiceType {fset K} (finSetChoiceMixin K).
+HB.instance Definition _ K := [isSub for (@enum_fset K)].
+HB.instance Definition _ (K : choiceType) := [Choice of {fset K} by <:].
 
 Section FinPredStruct.
 
@@ -1057,7 +1044,7 @@ Lemma imfset_rec (T : choiceType) (f : T -> K) (p : finmempred T)
 Proof.
 move=> PP v; have /imfsetP [k pk vv_eq] := valP v.
 pose vP := in_imfset f pk; suff -> : P v = P [` vP] by apply: PP.
-by congr P; apply/val_inj => /=; rewrite vv_eq.
+by congr P; apply/val_inj => /=; rewrite -vv_eq (*FIXME: was rewrite vv_eq*).
 Qed.
 
 Lemma mem_imfset (T : choiceType) (f : T -> K) (p : finmempred T) :
@@ -1138,7 +1125,7 @@ Lemma val_in_fset A (p : finmempred _) (k : A) :
    (val k \in imfset key val p) = (in_mem k p).
 Proof. by rewrite mem_imfset ?in_finmempred //; exact: val_inj. Qed.
 
-Lemma in_fset_val A (p : finmempred [eqType of A]) (k : K) :
+Lemma in_fset_val A (p : finmempred A) (k : K) :
   (k \in imfset key val p) = if insub k is Some a then in_mem a p else false.
 Proof.
 have [a _ <- /=|kNA] := insubP; first by rewrite val_in_fset.
@@ -1156,7 +1143,7 @@ apply: (iffP (imfsetP _ _ _ _)) => [|[kA xkA]]; last by exists [`kA].
 by move=> /sig2_eqW[/= x Xx ->]; exists (valP x); rewrite fsetsubE.
 Qed.
 
-Lemma in_fset_valF A (p : finmempred [eqType of A]) (k : K) : k \notin A ->
+Lemma in_fset_valF A (p : finmempred A) (k : K) : k \notin A ->
   (k \in imfset key val p) = false.
 Proof. by apply: contraNF => /imfsetP[/= a Xa->]. Qed.
 
@@ -1370,7 +1357,7 @@ apply: (iffP fset_eqP) => AsubB a; first by rewrite -AsubB inE => /andP[].
 by rewrite inE; have [/AsubB|] := boolP (a \in A).
 Qed.
 
-Lemma fset_sub_val A (p : finmempred [eqType of A]) :
+Lemma fset_sub_val A (p : finmempred A) :
   (imfset key val p) `<=` A.
 Proof. by apply/fsubsetP => k /in_fset_valP []. Qed.
 
@@ -2128,11 +2115,11 @@ End FSetInE.
 Section Enum.
 
 Lemma enum_fset0 (T : choiceType) :
-  enum [finType of fset0] = [::] :> seq (@fset0 T).
+  enum (fset0 : finType) = [::] :> seq (@fset0 T).
 Proof. by rewrite enumT unlock. Qed.
 
 Lemma enum_fset1 (T : choiceType) (x : T) :
-  enum [finType of [fset x]] = [:: [`fset11 x]].
+  enum ([fset x] : finType) = [:: [`fset11 x]].
 Proof.
 apply/perm_small_eq=> //; apply/uniq_perm => //.
   by apply/enum_uniq.
@@ -2231,8 +2218,7 @@ Proof. by move=> s; apply/fsetP=> x; rewrite !inE. Qed.
 Lemma unpickleK : cancel unpickle pickle.
 Proof. by move=> s; apply/setP=> x; rewrite !inE. Qed.
 
-Definition fset_finMixin := CanFinMixin pickleK.
-Canonical fset_finType := Eval hnf in FinType {fset T} fset_finMixin.
+HB.instance Definition _ : fintype.isFinite {fset T} := CanIsFinite pickleK.
 
 Lemma card_fsets : #|{:{fset T}}| = 2^#|T|.
 Proof.
@@ -2449,8 +2435,8 @@ Section FSetMonoids.
 Import Monoid.
 Variable (T : choiceType).
 
-Canonical fsetU_monoid := Law (@fsetUA T) (@fset0U T) (@fsetU0 T).
-Canonical fsetU_comoid := ComLaw (@fsetUC T).
+HB.instance Definition _ := isComLaw.Build {fset T} fset0 fsetU
+  (@fsetUA T) (@fsetUC T) (@fset0U T).
 
 End FSetMonoids.
 Section BigFOpsSeq.
@@ -2971,24 +2957,24 @@ End FinMapEncode.
 Section FinMapEqType.
 Variable (K : choiceType) (V : eqType).
 
-Definition finMap_eqMixin := CanEqMixin (@finMap_codeK K V).
-Canonical finMap_eqType := EqType {fmap K -> V} finMap_eqMixin.
+HB.instance Definition _ := Equality.copy {fmap K -> V}
+  (can_type (@finMap_codeK K V)).
 
 End FinMapEqType.
 
 Section FinMapChoiceType.
 Variable (K V : choiceType).
 
-Definition finMap_choiceMixin := CanChoiceMixin (@finMap_codeK K V).
-Canonical finMap_choiceType := ChoiceType {fmap K -> V} finMap_choiceMixin.
+HB.instance Definition _ := Choice.copy {fmap K -> V}
+  (can_type (@finMap_codeK K V)).
 
 End FinMapChoiceType.
 
 Section FinMapCountType.
 Variable (K V : countType).
 
-Definition finMap_countMixin := CanCountMixin (@finMap_codeK K V).
-Canonical finMap_countType := CountType {fmap K -> V} finMap_countMixin.
+HB.instance Definition _ := Countable.copy {fmap K -> V}
+  (can_type (@finMap_codeK K V)).
 
 End FinMapCountType.
 
@@ -3617,9 +3603,8 @@ Record fsfun := Fsfun {
        fmap_of_fsfun k != default (val k)]
 }.
 
-Canonical fsfun_subType := Eval hnf in [subType for fmap_of_fsfun].
-Definition fsfun_eqMixin := [eqMixin of fsfun by <:].
-Canonical  fsfun_eqType := EqType fsfun fsfun_eqMixin.
+HB.instance Definition _ := [isSub for fmap_of_fsfun].
+HB.instance Definition _ := [Equality of fsfun by <:].
 
 Fact fsfun_subproof (f : fsfun) :
   forall (k : K) (kf : k \in fmap_of_fsfun f),
@@ -3773,15 +3758,11 @@ Definition fsfun_of_ffun key (K : choiceType) (V : eqType)
   (S : {fset K}) (h : S -> V) (default : K -> V) :=
   (Fsfun.of_ffun default h key).
 
-Definition fsfun_choiceMixin (K V : choiceType) (d : K -> V) :=
-  [choiceMixin of fsfun d by <:].
-Canonical  fsfun_choiceType (K V : choiceType) (d : K -> V) :=
-  ChoiceType (fsfun d) (fsfun_choiceMixin d).
+HB.instance Definition _ (K V : choiceType) (d : K -> V) :=
+  [Choice of fsfun d by <:].
 
-Definition fsfun_countMixin (K V : countType) (d : K -> V) :=
-  [countMixin of fsfun d by <:].
-Canonical  fsfun_countType (K V : countType) (d : K -> V) :=
-  CountType (fsfun d) (fsfun_countMixin d).
+HB.instance Definition _ (K V : countType) (d : K -> V) :=
+  [Countable of fsfun d by <:].
 
 Declare Scope fsfun_scope.
 Delimit Scope fsfun_scope with fsfun.

set.v

@@ -1,3 +1,4 @@
+From HB Require Import structures.
 Set Warnings "-notation-incompatible-format".
 From mathcomp Require Import ssreflect ssrbool eqtype ssrfun ssrnat choice seq.
 Set Warnings "notation-incompatible-format".
@@ -106,7 +107,7 @@ Notation set0 := (@Order.bottom (display_set _) _).
 Notation setT := (@Order.top (display_set _) _).
 Notation setU := (@Order.join (display_set _) _).
 Notation setI := (@Order.meet (display_set _) _).
-Notation setD := (@Order.sub (display_set _) _).
+Notation setD := (@Order.diff (display_set _) _).
 Notation setC := (@Order.compl (display_set _) _).
 
 Notation "x :&: y" := (setI x y).
@@ -118,6 +119,48 @@ Notation "x \subset y" := (\sub%set x y) : bool_scope.
 Notation "x \proper y" := (\proper%set x y) : bool_scope.
 End SetSyntax.
 
+(*Coercion eqType_of_elementType : elementType >-> eqType.*)
+(*Implicit Types (X Y : elementType).*)
+HB.mixin Record isSemiset (elementType : Type (* Universe type *))
+    (eqType_of_elementType : elementType -> eqType)
+    d (set : elementType -> cbDistrLatticeType (display_set d)) := {
+  memset : forall X, set X -> eqType_of_elementType X -> bool;
+  set1 : forall X, eqType_of_elementType X -> set X;
+  notin_set0 : forall X (x : eqType_of_elementType X), ~~ memset _ set0 x; (* set0 is empty instead *)
+  in_set1 : forall X (x y : eqType_of_elementType X), memset _ (set1 _ y) x = (x == y);
+  sub1set : forall X (x : eqType_of_elementType X) A, (set1 _ x \subset A) = (memset _ A x);
+  set_gt0_ex : forall X (A : set X), (set0 \proper A) -> {x | memset _ A x} ; (* exists or sig ?? *)
+  subsetP_subproof : forall X (A B : set X), {subset memset _ A <= memset _ B} -> A \subset B;
+  in_setU : forall X (x : eqType_of_elementType X) A B, (memset _ (A :|: B) x) =
+                    (memset _ A x) || (memset _ B x);
+  (* there is no closure in a set *)
+  funsort : elementType -> elementType -> Type;
+  fun_of_funsort : forall X Y : elementType, funsort X Y -> eqType_of_elementType X -> eqType_of_elementType Y;
+  imset : forall X Y, funsort X Y -> set X -> set Y;
+  FIXME(*couldn't find the name*) : forall X Y (f : funsort X Y) (A : set X) (y : eqType_of_elementType Y),
+    reflect (exists2 x : eqType_of_elementType X, memset _ A x & y = fun_of_funsort _ _ f x)
+            (memset _ (imset _ _ f A) y)
+}.
+
+HB.structure Definition Semiset
+    (elementType : Type)
+    (eqType_of_elementType : elementType -> eqType)
+    d :=
+  {T of @isSemiset elementType eqType_of_elementType d T }.
+
+(* FIXME: how to integrate the constraint Order.CBDistrLattice d T ?
+forall x, Order.hasSub d (T x) ? *)
+
+(* STOP
+
+Record class_of (set : elementType -> Type) := Class {
+  base  : forall X, @Order.CBDistrLattice.class_of (set X);
+  mixin_disp : unit;
+  mixin : mixin_of (fun X => Order.CBDistrLattice.Pack (display_set mixin_disp) (base X))
+}.
+
+
+
 Module Semiset.
 Section ClassDef.
 Variable elementType : Type. (* Universe type *)
@@ -1043,4 +1086,6 @@ Export setTheory.
 
 End Theory.
 
+*)
+
 End SET.