diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index c091e98..217c627 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -18,8 +18,10 @@ jobs: matrix: image: - 'mathcomp/mathcomp:2.3.0-coq-8.20' - - 'mathcomp/mathcomp:2.3.0-coq-8.20' - - 'mathcomp/mathcomp-dev:coq-8.20' + - 'mathcomp/mathcomp:2.4.0-coq-8.20' + - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0' + - 'mathcomp/mathcomp:2.4.0-rocq-prover-dev' + - 'mathcomp/mathcomp-dev:rocq-prover-9.0' - 'mathcomp/mathcomp-dev:rocq-prover-dev' fail-fast: false steps: diff --git a/README.md b/README.md index 577c7c1..516ead6 100644 --- a/README.md +++ b/README.md @@ -24,10 +24,10 @@ which will be used to subsume notations for finite sets, eventually. - Cyril Cohen (initial) - Kazuhiko Sakaguchi - License: [CeCILL-B](CECILL-B) -- Compatible Coq versions: Coq 8.20 to 9.0 +- Compatible Rocq/Coq versions: 8.20 or later - Additional dependencies: - - [MathComp ssreflect 2.0 to 2.3](https://math-comp.github.io) -- Coq namespace: `mathcomp.finmap` + - [MathComp](https://math-comp.github.io) ssreflect 2.0.0 or later +- Rocq/Coq namespace: `mathcomp.finmap` - Related publication(s): none ## Building and installation instructions @@ -37,7 +37,7 @@ is via [OPAM](https://opam.ocaml.org/doc/Install.html): ```shell opam repo add coq-released https://coq.inria.fr/opam/released -opam install coq-mathcomp-finmap +opam install rocq-mathcomp-finmap ``` To instead build and install manually, do: diff --git a/finmap.v b/finmap.v index ad60625..9ad2520 100644 --- a/finmap.v +++ b/finmap.v @@ -338,7 +338,10 @@ Reserved Notation "[ 'f' 'setval' x : A | P ]" Reserved Notation "[ 'f' 'setval' x : A | P & Q ]" (at level 0, x at level 99, format "[ 'f' 'setval' x : A | P & Q ]"). -Reserved Notation "{fmap T }" (at level 0, format "{fmap T }"). +Reserved Notation "{ 'fmap' K -> T }" + (at level 0, K at level 98, T at level 99, format "{ 'fmap' K -> T }"). +Reserved Notation "[ 'fmap' 'of' K -> T ]" + (at level 0, K at level 98, T at level 99, format "[ 'fmap' 'of' K -> T ]"). Reserved Notation "x .[ k <- v ]" (left associativity, format "x .[ k <- v ]"). Reserved Notation "x .[~ k ]" (format "x .[~ k ]"). @@ -476,25 +479,24 @@ Structure finSet : Type := mkFinSet { _ : canonical_keys enum_fset }. +#[deprecated(since="finmap 2.3.0", note="Use finSet instead")] Definition finset_of (_ : phant K) := finSet. End Def. +Arguments finSet K%type_scope. + +#[warning="-deprecated-reference"] Identity Coercion type_of_finset : finset_of >-> finSet. -Notation "{fset T }" := (@finset_of _ (Phant T)) : type_scope. +Notation "{fset T }" := (finSet T) : type_scope. Definition pred_of_finset (K : choiceType) (f : finSet K) : pred K := fun k => k \in (enum_fset f). Canonical finSetPredType (K : choiceType) := PredType (@pred_of_finset K). -Section FinSetCanonicals. - -Variable (K : choiceType). - -HB.instance Definition _ := [isSub for (@enum_fset K)]. -HB.instance Definition _ := [Choice of {fset K} by <:]. - -End FinSetCanonicals. +HB.instance Definition _ (K : choiceType) := [isSub for @enum_fset K]. +HB.instance Definition _ (K : choiceType) := [Choice of {fset K} by <:]. +HB.instance Definition _ (T : countType) := [Countable of {fset T} by <:]. Section FinTypeSet. @@ -511,7 +513,6 @@ Record fset_sub_type : predArgType := 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)). @@ -547,6 +548,7 @@ Proof. by rewrite cardE enum_fsetE size_map. Qed. End FinTypeSet. +#[warning="-deprecated-reference"] Identity Coercion finSet_sub_type : finset_of >-> finSet. Coercion fset_sub_type : finSet >-> predArgType. #[global] Hint Resolve fsvalP fset_uniq mem_fset_sub_enum : core. @@ -569,33 +571,32 @@ Definition set_of_fset (K : choiceType) (A : {fset K}) : {set A} := Arguments pred_of_finset : simpl never. +HB.lock Definition seq_fset + (finset_key : unit) (K : choiceType) (s : seq K) : {fset K} := + mkFinSet (@canonical_sort_keys K s). + Section SeqFset. -Variable finset_key : unit. -Definition seq_fset : forall K : choiceType, seq K -> {fset K} := - locked_with finset_key (fun K s => mkFinSet (@canonical_sort_keys K s)). +Variable (finset_key : unit) (K : choiceType) (s : seq K). -Variable (K : choiceType) (s : seq K). +Notation seq_fset := (seq_fset finset_key). Lemma seq_fsetE : seq_fset s =i s. -Proof. by move=> a; rewrite [seq_fset]unlock sort_keysE. Qed. +Proof. by move=> a; rewrite unlock sort_keysE. Qed. Lemma size_seq_fset : size (seq_fset s) = size (undup s). -Proof. by rewrite [seq_fset]unlock /= size_sort_keys. Qed. +Proof. by rewrite unlock /= size_sort_keys. Qed. Lemma seq_fset_uniq : uniq (seq_fset s). -Proof. by rewrite [seq_fset]unlock /= sort_keys_uniq. Qed. +Proof. by rewrite unlock /= sort_keys_uniq. Qed. Lemma seq_fset_perm : perm_eq (seq_fset s) (undup s). -Proof. by rewrite [seq_fset]unlock //= sort_keys_perm. Qed. +Proof. by rewrite unlock //= sort_keys_perm. Qed. End SeqFset. #[global] Hint Resolve keys_canonical sort_keys_uniq : core. -HB.instance Definition _ K := [isSub for (@enum_fset K)]. -HB.instance Definition _ (K : choiceType) := [Choice of {fset K} by <:]. - Section FinPredStruct. Structure finpredType (T : eqType) := FinPredType { @@ -635,6 +636,7 @@ Definition mkFinPredType_of (T : eqType) (U : Type) := @FinPredType T U a (exist _ fpred_seq (fpred_seq_uniq, (mkFinPredType_of_subproof fpred_seqE))). +#[deprecated(since="finmap 2.3.0", note="Use the reverse coercion instead.")] Definition clone_finpredType (T : eqType) (U : Type) := fun (pT : finpredType T) & finpred_sort pT -> U => fun a pP (pT' := @FinPredType T U a pP) & phant_id pT' pT => pT'. @@ -672,6 +674,7 @@ Canonical fin_finpred (T : eqType) (pT : finpredType T) (p : pT) := @FinPred _ _ p (@IsFinite _ _ (enum_finpred p) (enum_finpred_uniq p) (enum_finpredE p)). +#[deprecated(since="finmap 2.3.0", note="Use the reverse coercion instead.")] Definition finpred_of (T : eqType) (pT : predType T) (p : pT) (fp : finpred pT) & phantom pT fp : finpred pT := fp. @@ -691,6 +694,7 @@ Lemma enum_finmemE (T : eqType) (p : finmempred T) : enum_finmem p =i p. Proof. by case: p => ?[]. Qed. +#[deprecated(since="finmap 2.3.0", note="Use the reverse coercion instead.")] Definition finmempred_of (T : eqType) (P : pred T) (mP : finmempred T) & phantom (mem_pred T) mP : finmempred T := mP. @@ -700,6 +704,8 @@ Canonical mem_fin (T : eqType) (pT : predType T) (p : finpred pT) := End FinPredStruct. +#[deprecated(since="finmap 2.3.0", note="Use the reverse coercion instead."), + warning="-deprecated"] Notation "[ 'finpredType' 'of' T ]" := (@clone_finpredType _ T _ id _ _ id) (at level 0, format "[ 'finpredType' 'of' T ]") : form_scope. @@ -733,42 +739,15 @@ Canonical seq_finpredType (T : eqType) := End CanonicalFinPred. -Local Notation imfset_def key := - (fun (T K : choiceType) (f : T -> K) (p : finmempred T) - of phantom (mem_pred T) p => seq_fset key [seq f x | x <- enum_finmem p]). -Local Notation imfset2_def key := - (fun (K T1 : choiceType) (T2 : T1 -> choiceType) - (f : forall x : T1, T2 x -> K) - (p1 : finmempred T1) (p2 : forall x : T1, finmempred (T2 x)) - of phantom (mem_pred T1) p1 & phantom (forall x, mem_pred (T2 x)) p2 => - seq_fset key [seq f x y | x <- enum_finmem p1, y <- enum_finmem (p2 x)]). - -Module Type ImfsetSig. -Parameter imfset : forall (key : unit) (T K : choiceType) - (f : T -> K) (p : finmempred T), - phantom (mem_pred T) p -> {fset K}. -Parameter imfset2 : forall (key : unit) (K T1 : choiceType) - (T2 : T1 -> choiceType)(f : forall x : T1, T2 x -> K) - (p1 : finmempred T1) (p2 : forall x : T1, finmempred (T2 x)), - phantom (mem_pred T1) p1 -> phantom (forall x, mem_pred (T2 x)) p2 -> {fset K}. -Axiom imfsetE : forall key, imfset key = imfset_def key. -Axiom imfset2E : forall key, imfset2 key = imfset2_def key. -End ImfsetSig. - -Module Imfset : ImfsetSig. -Definition imfset key := imfset_def key. -Definition imfset2 key := imfset2_def key. -Lemma imfsetE key : imfset key = imfset_def key. Proof. by []. Qed. -Lemma imfset2E key : imfset2 key = imfset2_def key. Proof. by []. Qed. -End Imfset. - -Notation imfset key f p := - (Imfset.imfset key f (Phantom _ (pred_of_finmempred p))). -Notation imfset2 key f p q := - (Imfset.imfset2 key f (Phantom _ (pred_of_finmempred p)) - (Phantom _ (fun x => (pred_of_finmempred (q x))))). -Canonical imfset_unlock k := Unlockable (Imfset.imfsetE k). -Canonical imfset2_unlock k := Unlockable (Imfset.imfset2E k). +HB.lock Definition imfset + (key : unit) (T K : choiceType) (f : T -> K) (p : finmempred T) : {fset K} := + seq_fset key [seq f x | x <- enum_finmem p]. + +HB.lock Definition imfset2 + (key : unit) (K T1 : choiceType) (T2 : T1 -> choiceType) + (f : forall x : T1, T2 x -> K) + (p1 : finmempred T1) (p2 : forall x : T1, finmempred (T2 x)) : {fset K} := + seq_fset key [seq f x y | x <- enum_finmem p1, y <- enum_finmem (p2 x)]. Notation "A `=` B" := (A = B :> {fset _}) (only parsing) : fset_scope. Notation "A `<>` B" := (A <> B :> {fset _}) (only parsing) : fset_scope. @@ -776,11 +755,9 @@ Notation "A `==` B" := (A == B :> {fset _}) (only parsing) : fset_scope. Notation "A `!=` B" := (A != B :> {fset _}) (only parsing) : fset_scope. Notation "A `=P` B" := (A =P B :> {fset _}) (only parsing) : fset_scope. -Notation "f @`[ key ] A" := - (Imfset.imfset key f (Phantom _ (mem A))) : fset_scope. +Notation "f @`[ key ] A" := (imfset key f (mem A)) : fset_scope. Notation "f @2`[ key ] ( A , B )" := - (Imfset.imfset2 key f (Phantom _ (mem A)) (Phantom _ (fun x => (mem (B x))))) - : fset_scope. + (imfset2 key f (mem A) (fun x => (mem (B x)))) : fset_scope. Fact imfset_key : unit. Proof. exact: tt. Qed. @@ -2984,6 +2961,7 @@ Record finMap : Type := FinMap { ffun_of_fmap :> {ffun domf -> V} }. +#[deprecated(since="finmap 2.3.0", note="Use finMap instead.")] Definition finmap_of (_ : phant (K -> V)) := finMap. Let T_ (domf : {fset K}) := {ffun domf -> V}. @@ -2991,7 +2969,9 @@ Local Notation finMap' := {domf : _ & T_ domf}. End DefMap. -Notation "{fmap T }" := (@finmap_of _ _ (Phant T)) : type_scope. +Arguments finMap K%type_scope V%type_scope. + +Notation "{ 'fmap' K -> T }" := (finMap K T) : type_scope. Definition pred_of_finmap (K : choiceType) (V : Type) (f : {fmap K -> V}) : pred K := mem (domf f). @@ -3045,7 +3025,8 @@ Arguments fmap0 {K V}. Arguments setf : simpl never. Arguments fnd : simpl never. -Notation "[ 'fmap' 'of' T ]" := (fmap0 : {fmap T}) (only parsing) : fmap_scope. +Notation "[ 'fmap' 'of' K -> T ]" := + (fmap0 : {fmap K -> T}) (only parsing) : fmap_scope. Notation "[fmap]" := fmap0 : fmap_scope. Notation "x .[ k <- v ]" := (setf x k v) : fmap_scope. Notation "f .[? k ]" := (fnd f k) : fmap_scope. @@ -3555,14 +3536,14 @@ Proof. by move=> dfg; rewrite catfC remf_id. Qed. Lemma catfAC f g h : f + g + h = f + h + g.[\ domf h]. Proof. by rewrite -!catfA [X in _ + X]catfC. Qed. -Lemma disjoint_catfAC f g h : [disjoint domf g & domf h]%fmap -> +Lemma disjoint_catfAC f g h : [disjoint domf g & domf h] -> f + g + h = f + h + g. Proof. by move=> dgh; rewrite catfAC remf_id. Qed. Lemma catfCA f g h : f + (g + h) = g + (f.[\ domf g] + h). Proof. by rewrite !catfA [X in X + _]catfC. Qed. -Lemma disjoint_catfCA f g h : [disjoint domf f & domf g]%fmap -> +Lemma disjoint_catfCA f g h : [disjoint domf f & domf g] -> f + (g + h) = g + (f + h). Proof. by move=> dfg; rewrite catfCA remf_id. Qed. @@ -3747,31 +3728,19 @@ Record fsfun := Fsfun { 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), - (fmap_of_fsfun f).[kf]%fmap != default k. -Proof. -case:f => f f_stable k kf /=. -exact: (forallP f_stable [` kf]). -Qed. +Fact fsfun_subproof (f : fsfun) (k : K) (kf : k \in fmap_of_fsfun f) : + (fmap_of_fsfun f).[kf] != default k. +Proof. case:f kf => f f_stable kf; exact: (forallP f_stable [` kf]). Qed. Definition fun_of_fsfun (f : fsfun) (k : K) := - odflt (default k) (fmap_of_fsfun f).[? k]%fmap. + odflt (default k) (fmap_of_fsfun f).[? k]. End FsfunDef. Coercion fun_of_fsfun : fsfun >-> Funclass. -Module Type FinSuppSig. -Axiom fs : forall (K : choiceType) (V : eqType) (default : K -> V), - fsfun default -> {fset K}. -Axiom E : fs = (fun K V d f => domf (@fmap_of_fsfun K V d f)). -End FinSuppSig. -Module FinSupp : FinSuppSig. -Definition fs := (fun K V d f => domf (@fmap_of_fsfun K V d f)). -Definition E := erefl fs. -End FinSupp. -Notation finsupp := FinSupp.fs. -Canonical unlockable_finsupp := Unlockable FinSupp.E. +HB.lock Definition finsupp + (K : choiceType) (V : eqType) (d : K -> V) (f : fsfun d) : {fset K} := + domf (@fmap_of_fsfun K V d f). Section FSfunBasics. @@ -3848,38 +3817,34 @@ Notation "{ 'fsfun' 'of' x => dflt }" := {fsfun of x : _ => dflt} Notation "{ 'fsfun' 'with' dflt }" := {fsfun of _ => dflt} (at level 0, only parsing) : type_scope. -Module Type FsfunSig. -Section FsfunSig. -Variables (K : choiceType) (V : eqType) (default : K -> V). - -Parameter of_ffun : forall (S : {fset K}), (S -> V) -> unit -> fsfun default. -Variables (S : {fset K}) (h : S -> V). -Axiom of_ffunE :forall key x, of_ffun h key x = odflt (default x) (omap h (insub x)). - -End FsfunSig. -End FsfunSig. - -Module Fsfun : FsfunSig. Section FsfunOfFinfun. -Variables (K : choiceType) (V : eqType) (default : K -> V) - (S : {fset K}) (h : S -> V). +Variables (K : choiceType) (V : eqType). +Variables (S : {fset K}) (h : S -> V) (default : K -> V). -Let fmap := +Let fmap : {fmap K -> V} := [fmap a : [fsetval a in {: S} | h a != default (val a)] => h (fincl (fset_sub_val _ _) a)]. -Fact fmapP a : fmap a != default (val a). +Fact fsfun_of_ffun_subproof (a : domf fmap) : fmap a != default (val a). Proof. rewrite ffunE; have /in_fset_valP [a_in_S] := valP a. by have -> : [` a_in_S] = fincl (fset_sub_val _ _) a by exact/val_inj. Qed. -Definition of_ffun (k : unit) := fsfun_of_can_ffun fmapP. +End FsfunOfFinfun. -Lemma of_ffunE key x : of_ffun key x = odflt (default x) (omap h (insub x)). +HB.lock Definition fsfun_of_ffun + (k : unit) (K : choiceType) (V : eqType) + (S : {fset K}) (h : S -> V) (default : K -> V) := + fsfun_of_can_ffun (@fsfun_of_ffun_subproof K V S h default). + +Lemma fsfun_ffun + (k : unit) (K : choiceType) (V : eqType) + (default : K -> V) (S : {fset K}) (h : S -> V) (x : K) : + fsfun_of_ffun k h default x = odflt (default x) (omap h (insub x)). Proof. -rewrite /fun_of_fsfun /=. +rewrite unlock /fun_of_fsfun /=. case: insubP => /= [u _ <-|xNS]; last first. case: fndP => //= kf; rewrite !ffunE /=. by set y := (X in h X); rewrite (valP y) in xNS. @@ -3888,17 +3853,8 @@ case: fndP => /= [kf|]. by rewrite inE /= -topredE /= negbK => /eqP ->. Qed. -End FsfunOfFinfun. -End Fsfun. -Canonical fsfun_of_funE K V default S h key x := - Unlockable (@Fsfun.of_ffunE K V default S h key x). - Fact fsfun_key : unit. Proof. exact: tt. Qed. -Definition fsfun_of_ffun key (K : choiceType) (V : eqType) - (S : {fset K}) (h : S -> V) (default : K -> V) := - (Fsfun.of_ffun default h key). - HB.instance Definition _ (K V : choiceType) (d : K -> V) := [Choice of fsfun d by <:]. @@ -4012,18 +3968,13 @@ Notation "[ 'fsfun' ]" := [fsfun for _] Section FsfunTheory. Variables (key : unit) (K : choiceType) (V : eqType) (default : K -> V). -Lemma fsfun_ffun (S : {fset K}) (h : S -> V) (x : K) : - [fsfun[key] a : S => h a | default a] x = - odflt (default x) (omap h (insub x)). -Proof. by rewrite unlock. Qed. - Lemma fsfun_fun (S : {fset K}) (h : K -> V) (x : K) : [fsfun[key] a in S => h a | default a] x = if x \in S then h x else (default x). Proof. by rewrite fsfun_ffun; case: insubP => //= [u -> ->|/negPf ->]. Qed. Lemma fsfun0E : [fsfun for default] =1 default. -Proof. by move=> x; rewrite unlock insubF ?inE. Qed. +Proof. by move=> x; rewrite fsfun_ffun insubF ?inE. Qed. Definition fsfunE := (fsfun_fun, fsfun0E). @@ -4038,7 +3989,7 @@ Qed. Lemma finsupp_sub (S : {fset K}) (h : S -> V) : finsupp [fsfun[key] a : S => h a | default a] `<=` S. Proof. -apply/fsubsetP => a; rewrite mem_finsupp unlock /=. +apply/fsubsetP => a; rewrite mem_finsupp fsfun_ffun. by case: insubP => //=; rewrite eqxx. Qed. diff --git a/meta.yml b/meta.yml index bcbb624..c8693b0 100644 --- a/meta.yml +++ b/meta.yml @@ -31,25 +31,29 @@ license: file: CECILL-B supported_coq_versions: - text: Coq 8.20 to 9.0 - opam: '{ (>= "8.20" & < "8.21~") | (= "dev") }' + text: 8.20 or later + opam: '{>= "8.20"}' tested_coq_opam_versions: - version: '2.3.0-coq-8.20' repo: 'mathcomp/mathcomp' -- version: '2.3.0-coq-8.20' +- version: '2.4.0-coq-8.20' + repo: 'mathcomp/mathcomp' +- version: '2.4.0-rocq-prover-9.0' + repo: 'mathcomp/mathcomp' +- version: '2.4.0-rocq-prover-dev' repo: 'mathcomp/mathcomp' -- version: 'coq-8.20' +- version: 'rocq-prover-9.0' repo: 'mathcomp/mathcomp-dev' -- version: 'coq-dev' +- version: 'rocq-prover-dev' repo: 'mathcomp/mathcomp-dev' dependencies: - opam: name: rocq-mathcomp-ssreflect - version: '{ (>= "2.0" & < "2.5~") | (= "dev") }' + version: '{>= "2.0.0"}' description: |- - [MathComp ssreflect 2.0 to 2.3](https://math-comp.github.io) + [MathComp](https://math-comp.github.io) ssreflect 2.0.0 or later namespace: mathcomp.finmap diff --git a/rocq-mathcomp-finmap.opam b/rocq-mathcomp-finmap.opam index be1f14b..ae0b849 100644 --- a/rocq-mathcomp-finmap.opam +++ b/rocq-mathcomp-finmap.opam @@ -22,9 +22,9 @@ build: [make "-j%{jobs}%"] install: [make "install"] depends: [ ("coq" {>= "8.20" & < "8.21~"} - | "rocq-core" {>= "9.0" | = "dev"}) + | "rocq-core" {>= "9.0"}) ("coq-mathcomp-ssreflect" { >= "2.0" & < "2.4~" } - |"rocq-mathcomp-ssreflect" { (>= "2.4" & < "2.5~") | = "dev" }) + |"rocq-mathcomp-ssreflect" { >= "2.4" }) ] tags: [