diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml new file mode 100644 index 0000000..43c321c --- /dev/null +++ b/.github/workflows/coq-action.yml @@ -0,0 +1,38 @@ +name: CI + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + +jobs: + build: + # the OS must be GNU/Linux to be able to use the docker-coq-action + runs-on: ubuntu-latest + strategy: + matrix: + image: + - 'mathcomp/mathcomp:1.11.0-coq-8.10' + - 'mathcomp/mathcomp:1.11.0-coq-8.11' + - 'mathcomp/mathcomp:1.11.0-coq-8.12' + - 'mathcomp/mathcomp:1.12.0-coq-8.10' + - 'mathcomp/mathcomp:1.12.0-coq-8.11' + - 'mathcomp/mathcomp:1.12.0-coq-8.12' + - 'mathcomp/mathcomp-dev:coq-8.10' + - 'mathcomp/mathcomp-dev:coq-8.11' + - 'mathcomp/mathcomp-dev:coq-8.12' + - 'mathcomp/mathcomp-dev:coq-dev' + fail-fast: false + steps: + - uses: actions/checkout@v2 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'coq-mathcomp-finmap.opam' + custom_image: ${{ matrix.image }} + +# See also: +# https://github.com/coq-community/docker-coq-action#readme +# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index a1f770b..0000000 --- a/.travis.yml +++ /dev/null @@ -1,62 +0,0 @@ -dist: trusty -sudo: required -language: generic - -branches: - only: - - master - -services: - - docker - -env: - global: - - NJOBS="2" - - CONTRIB_NAME="finmap" - matrix: - - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.7" - - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.8" - - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.9" - - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.10" - - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.11" - - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.12" - - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.7" - - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.8" - - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.9" - - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.10" - - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.11" - - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.12" - -install: | - # Prepare the COQ container - docker pull "${DOCKERIMAGE}" - docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB_NAME} -w /home/coq/${CONTRIB_NAME} "${DOCKERIMAGE}" - docker exec COQ /bin/bash --login -c " - # This bash script is double-quoted to interpolate Travis CI env vars: - echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\" - export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' - set -ex # -e = exit on failure; -x = trace for debug - # Using flambda makes sense here as we usually get ~10% faster - # builds in math-comp. - opam switch \$COMPILER_EDGE - eval \$(opam env) - opam update -y - opam config list - opam repo list - opam list - sudo chown -R coq:coq /home/coq/${CONTRIB_NAME} - opam pin add -y -n -k path coq-mathcomp-finmap.dev . - # install deps only - opam install -y -vvv --deps-only coq-mathcomp-finmap - " -script: -- echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r' -- | - docker exec COQ /bin/bash --login -c " - export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' - set -ex - eval \$(opam env) - opam install -y -vvv coq-mathcomp-finmap - " -- docker stop COQ # optional -- echo -en 'travis_fold:end:script\\r' diff --git a/CeCILL-B b/CECILL-B similarity index 97% rename from CeCILL-B rename to CECILL-B index fe29f5c..e441d5a 100644 --- a/CeCILL-B +++ b/CECILL-B @@ -16,7 +16,7 @@ the two main principles guiding its drafting: both authors and holders of the economic rights over software. The authors of the CeCILL-B (for Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre]) -license are: +license are: Commissariat à l'Energie Atomique - CEA, a public scientific, technical and industrial research establishment, having its principal place of @@ -402,8 +402,8 @@ rights set forth in Article 5). 9.3 The Licensee acknowledges that the Software is supplied "as is" by the Licensor without any other express or tacit warranty, other than -that provided for in Article 9.2 and, in particular, without any warranty -as to its commercial value, its secured, safe, innovative or relevant +that provided for in Article 9.2 and, in particular, without any warranty +as to its commercial value, its secured, safe, innovative or relevant nature. Specifically, the Licensor does not warrant that the Software is free diff --git a/README.md b/README.md index 8c0409d..aca1ed6 100644 --- a/README.md +++ b/README.md @@ -1,33 +1,73 @@ -[![Build Status](https://travis-ci.org/math-comp/finmap.svg?branch=master)](https://travis-ci.org/math-comp/finmap) +# Finite maps -# A finset and finmap library +[![CI][action-shield]][action-link] -## AUTHORS +[action-shield]: https://github.com/math-comp/finmap/workflows/CI/badge.svg?branch=master +[action-link]: https://github.com/math-comp/finmap/actions?query=workflow%3ACI -Cyril Cohen, -Kazuhiko Sakaguchi (for the order library now moved to the main math-comp repository) -and contributions from various people https://github.com/math-comp/finmap/graphs/contributors -# RELATED WORK -This library was developed independently but inspired from Pierre-Yves -Strub's library (https://github.com/strub/ssrmisc/blob/master/fset.v), -from Christian Doczkal's library -(https://www.ps.uni-saarland.de/formalizations/fset/html/libs.fset.html) -and from Beta Ziliani's work (no reference provided so far). -This library should ultimately be integrated to the mathematical -components library, when it is finished. +This library is an extension of mathematical component in order to +support finite sets and finite maps on choicetypes (rather that finite +types). This includes support for functions with finite support and +multisets. The library also contains a generic order and set libary, +which will be used to subsume notations for finite sets, eventually. + +## Meta + +- Author(s): + - Cyril Cohen (initial) + - Kazuhiko Sakaguchi +- License: [CeCILL-B](CECILL-B) +- Compatible Coq versions: Coq 8.10 to 8.12 +- Additional dependencies: + - [MathComp ssreflect 1.10 to 1.12](https://math-comp.github.io) + - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough) +- Coq namespace: `mathcomp.finmap` +- Related publication(s): none + +## Building and installation instructions + +The easiest way to install the latest released version of Finite maps +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 +``` + +To instead build and install manually, do: -## DOCUMENTATION +``` shell +git clone https://github.com/math-comp/finmap.git +cd finmap +make # or make -j +make install +``` + + +## Documentation The documentation is available in the header of the file. -## LICENSING +This library will be integrated to the mathematical components +library in the near future. + +## Related work + +This library was developed independently but inspired from +[Pierre-Yves Strub's +library](https://github.com/strub/ssrmisc/blob/master/fset.v), from +[Christian Doczkal's +library](https://www.ps.uni-saarland.de/formalizations/fset/html/libs.fset.html) +and from Beta Ziliani's work (no reference provided so far). + +Another alternative is [Arthur Azevedo de Amorim extensional +structures library](https://github.com/arthuraa/extructures). -This program is free software; you can redistribute it and/or modify -it under the terms of the CeCILL B FREE SOFTWARE LICENSE. +## Acknowledgments -You should have received a copy of the CeCILL B License with this -Kit, in the file named "CeCILL-B". -If not, visit http://www.cecill.info +Many thanks to Kazuhiko Sakaguchi (for the order library now moved to +the main math-comp repository) and to [various +contributors](https://github.com/math-comp/finmap/graphs/contributors) diff --git a/_CoqProject b/_CoqProject index 4da5775..a775ba4 100644 --- a/_CoqProject +++ b/_CoqProject @@ -3,3 +3,11 @@ multiset.v set.v -R . mathcomp.finmap +-arg -w -arg -projection-no-head-constant +-arg -w -arg -redundant-canonical-projection +-arg -w -arg -notation-overridden +-arg -w -arg +duplicate-clear +-arg -w -arg +non-primitive-record +-arg -w -arg +undeclared-scope +-arg -w -arg -ambiguous-paths +-arg -w -arg -uniform-inheritance \ No newline at end of file diff --git a/config.nix b/config.nix new file mode 100644 index 0000000..adbbdfe --- /dev/null +++ b/config.nix @@ -0,0 +1,4 @@ +{ + coq = "8.10"; + mathcomp = "1.11.0"; +} diff --git a/opam b/coq-mathcomp-finmap.opam similarity index 58% rename from opam rename to coq-mathcomp-finmap.opam index e3128be..cc8a618 100644 --- a/opam +++ b/coq-mathcomp-finmap.opam @@ -1,28 +1,35 @@ opam-version: "2.0" -name: "coq-mathcomp-finmap" -version: "dev" maintainer: "Cyril Cohen " +version: "dev" homepage: "https://github.com/math-comp/finmap" -bug-reports: "https://github.com/math-comp/finmap/issues" dev-repo: "git+https://github.com/math-comp/finmap.git" -license: "CeCILL-B" - -build: [ make "-j" "%{jobs}%" ] -install: [ make "install" ] +bug-reports: "https://github.com/math-comp/finmap/issues" +license: "CECILL-B" -depends: [ - "coq" { (>= "8.7" & < "8.13~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") | (= "dev") } - "coq-mathcomp-bigenough" { (>= "1.0.0" & < "1.1~") | (= "dev") } -] -tags: [ "keyword:finmap" "keyword:finset" "keyword:multiset" "keyword:order"] -authors: [ "Cyril Cohen " "Kazuhiko Sakaguchi " ] -synopsis: "Finite sets, finite maps, finitely supported functions, orders" +synopsis: "Finite sets, finite maps, finitely supported functions" description: """ This library is an extension of mathematical component in order to support finite sets and finite maps on choicetypes (rather that finite types). This includes support for functions with finite support and multisets. The library also contains a generic order and set libary, -which will be used to subsume notations for finite sets, eventually. -""" +which will be used to subsume notations for finite sets, eventually.""" + +build: [make "-j%{jobs}%" ] +install: [make "install"] +depends: [ + "coq" { (>= "8.10" & < "8.13~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.13~") | (= "dev") } + "coq-mathcomp-bigenough" {>= "1.0.0"} +] + +tags: [ + "keyword:finmap" + "keyword:finset" + "keyword:multiset" + "logpath:mathcomp.finmap" +] +authors: [ + "Cyril Cohen" + "Kazuhiko Sakaguchi" +] diff --git a/default.nix b/default.nix new file mode 100644 index 0000000..9c4336c --- /dev/null +++ b/default.nix @@ -0,0 +1,144 @@ +{ + nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix + else fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/502845c3e31ef3de0e424f3fcb09217df2ce6df6.tar.gz), + config ? (if builtins.pathExists ./config.nix then import ./config.nix else {}), + withEmacs ? false, + print-env ? false, + do-nothing ? false, + package ? (if builtins.pathExists ./package.nix then import ./package.nix else "mathcomp-fast"), + src ? (if builtins.pathExists ./package.nix then ./. else false) +}: +with builtins; +let + cfg-fun = if isFunction config then config else (pkgs: config); + pkg-src = if src == false then {} + else { ${if package == "mathcomp.single" then "mathcomp" else package} = src; }; + pkgs = if isAttrs nixpkgs then nixpkgs else import nixpkgs { + overlays = [ (pkgs: super-pkgs: with pkgs.lib; + let coqPackages = with pkgs; { + "8.7" = coqPackages_8_7; + "8.8" = coqPackages_8_8; + "8.9" = coqPackages_8_9; + "8.10" = coqPackages_8_10; + "8.11" = coqPackages_8_11; + "8.12" = coqPackages_8_12; + "default" = coqPackages_8_10; + }.${(cfg-fun pkgs).coq or "default"}.overrideScope' + (coqPackages: super-coqPackages: + let + all-pkgs = pkgs // { inherit coqPackages; }; + cfg = pkg-src // { + mathcomp-fast = { + src = ./.; + propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-fast); + }; + mathcomp-full = { + src = ./.; + propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-all); + }; + } // (cfg-fun all-pkgs); + in { + mathcomp-extra-config = + let mec = super-coqPackages.mathcomp-extra-config; in + lib.recursiveUpdate mec { + initial = { + # fixing mathcomp analysis to depend on real-closed + mathcomp-analysis = {version, coqPackages} @ args: + let mca = mec.initial.mathcomp-analysis args; in + mca // { + propagatedBuildInputs = mca.propagatedBuildInputs ++ + (if builtins.elem coq.version ["8.10" "8.11" "8.12"] then (with coqPackages; [ coq-elpi hierarchy-builder ]) else []); + }; + }; + for-coq-and-mc.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} = + (super-coqPackages.mathcomp-extra-config.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} or {}) // + (removeAttrs cfg [ "mathcomp" "coq" "mathcomp-fast" "mathcomp-full" ]); + }; + mathcomp = if cfg?mathcomp then coqPackages.mathcomp_ cfg.mathcomp else super-coqPackages.mathcomp; + } // mapAttrs + (package: version: coqPackages.mathcomp-extra package version) + (removeAttrs cfg ["mathcomp" "coq"]) + ); in { + coqPackages = coqPackages.filterPackages coqPackages.coq coqPackages; + coq = coqPackages.coq; + mc-clean = src: { + version = baseNameOf src; + src = cleanSourceWith { + src = cleanSource src; + filter = path: type: let baseName = baseNameOf (toString path); in ! ( + hasSuffix ".aux" baseName || + hasSuffix ".d" baseName || + hasSuffix ".vo" baseName || + hasSuffix ".glob" baseName || + elem baseName ["Makefile.coq" "Makefile.coq.conf" ".mailmap" ".git"] + ); + }; + }; + })]; + }; + + mathcompnix = ./.; + + shellHook = '' + nixEnv () { + echo "Here is your work environement" + echo "buildInputs:" + for x in $buildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done + echo "propagatedBuildInputs:" + for x in $propagatedBuildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done + echo "you can pass option --arg config '{coq = \"x.y\"; math-comp = \"x.y.z\";}' to nix-shell to change coq and/or math-comp versions" + } + + printEnv () { + for x in $buildInputs; do echo $x; done + for x in $propagatedBuildInputs; do echo $x; done + } + + cachixEnv () { + echo "Pushing environement to cachix" + printEnv | cachix push math-comp + } + + nixDefault () { + cat $mathcompnix/default.nix + } > default.nix + + updateNixPkgs (){ + HASH=$(git ls-remote https://github.com/NixOS/nixpkgs-channels refs/heads/nixpkgs-unstable | cut -f1); + URL=https://github.com/NixOS/nixpkgs-channels/archive/$HASH.tar.gz + SHA256=$(nix-prefetch-url --unpack $URL) + echo "fetchTarball { + url = $URL; + sha256 = \"$SHA256\"; + }" > nixpkgs.nix + } + updateNixPkgsMaster (){ + HASH=$(git ls-remote https://github.com/NixOS/nixpkgs refs/heads/master | cut -f1); + URL=https://github.com/NixOS/nixpkgs/archive/$HASH.tar.gz + SHA256=$(nix-prefetch-url --unpack $URL) + echo "fetchTarball { + url = $URL; + sha256 = \"$SHA256\"; + }" > nixpkgs.nix + } + '' + + pkgs.lib.optionalString print-env "nixEnv"; + + emacs = with pkgs; emacsWithPackages + (epkgs: with epkgs.melpaStablePackages; [proof-general]); + + pkg = with pkgs; + if package == "mathcomp.single" then coqPackages.mathcomp.single + else coqPackages.${package} or (coqPackages.current-mathcomp-extra package); +in +if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: { + inherit shellHook mathcompnix; + + buildInputs = if do-nothing then [] + else (old.buildInputs ++ + (if pkgs.lib.trivial.inNixShell then pkgs.lib.optional withEmacs pkgs.emacs + else [])); + + propagatedBuildInputs = if do-nothing then [] else old.propagatedBuildInputs; + +}) else pkg diff --git a/dune b/dune new file mode 100644 index 0000000..25f129b --- /dev/null +++ b/dune @@ -0,0 +1,4 @@ +(coq.theory + (name mathcomp.finmap) + (package coq-mathcomp-finmap) + (synopsis "Finite sets, finite maps, finitely supported functions")) diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..e977151 --- /dev/null +++ b/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.5) +(using coq 0.2) +(name finmap) diff --git a/finmap.v b/finmap.v index a382523..d06e8e5 100644 --- a/finmap.v +++ b/finmap.v @@ -1,6 +1,9 @@ (* (c) Copyright 2006-2019 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) + +Set Warnings "-notation-incompatible-format". From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq. +Set Warnings "notation-incompatible-format". From mathcomp Require Import choice path finset finfun fintype bigop. (*****************************************************************************) @@ -426,9 +429,7 @@ Qed. End SortKeys. End SortKeys. -Hint Resolve SortKeys.perm. -Hint Resolve SortKeys.uniq. -Hint Resolve SortKeys.E. +#[global] Hint Resolve SortKeys.perm SortKeys.uniq SortKeys.E : core. Notation sort_keys := SortKeys.f. Notation sort_keys_perm := SortKeys.perm. @@ -573,8 +574,9 @@ End FinTypeSet. Identity Coercion finSet_sub_type : finset_of >-> finSet. Coercion fset_sub_type : finSet >-> predArgType. -Hint Resolve fsvalP fset_uniq mem_fset_sub_enum. +#[global] Hint Resolve fsvalP fset_uniq mem_fset_sub_enum : core. +Declare Scope fset_scope. Delimit Scope fset_scope with fset. Local Open Scope fset_scope. @@ -614,8 +616,7 @@ Proof. by rewrite [seq_fset]unlock //= sort_keys_perm. Qed. End SeqFset. -Hint Resolve keys_canonical. -Hint Resolve sort_keys_uniq. +#[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 <:]. @@ -1384,7 +1385,7 @@ by rewrite !inE andbC; apply/negP => /andP [/sAB ->]. Qed. Lemma fsubset_refl A : A `<=` A. Proof. exact/fsubsetP. Qed. -Hint Resolve fsubset_refl. +Hint Resolve fsubset_refl : core. Definition fincl A B (AsubB : A `<=` B) (a : A) : B := [` (fsubsetP AsubB) _ (valP a)]. @@ -1445,22 +1446,22 @@ Proof. by rewrite fsetUC; apply/fsetUidPr. Qed. Lemma fsubsetUl A B : A `<=` A `|` B. Proof. by apply/fsubsetP => a; rewrite inE => ->. Qed. -Hint Resolve fsubsetUl. +Hint Resolve fsubsetUl : core. Lemma fsubsetUr A B : B `<=` A `|` B. Proof. by rewrite fsetUC. Qed. -Hint Resolve fsubsetUr. +Hint Resolve fsubsetUr : core. Lemma fsubsetU1 x A : A `<=` x |` A. Proof. by rewrite fsubsetUr. Qed. -Hint Resolve fsubsetU1. +Hint Resolve fsubsetU1 : core. Lemma fsubsetU A B C : (A `<=` B) || (A `<=` C) -> A `<=` B `|` C. Proof. by move=> /orP [] /fsubset_trans ->. Qed. Lemma fincl_inj A B (AsubB : A `<=` B) : injective (fincl AsubB). Proof. by move=> a b [eq_ab]; apply: val_inj. Qed. -Hint Resolve fincl_inj. +Hint Resolve fincl_inj : core. Lemma fsub_inj B : {in [pred A | A `<=` B] &, injective (fsub B)}. Proof. @@ -1469,7 +1470,7 @@ apply/idP/idP => mem_a. by have := eqAA' (fincl sAB [` mem_a]); rewrite !inE // => <-. by have := eqAA' (fincl sA'B [` mem_a]); rewrite !inE // => ->. Qed. -Hint Resolve fsub_inj. +Hint Resolve fsub_inj : core. Lemma eqEfsubset A B : (A == B) = (A `<=` B) && (B `<=` A). Proof. @@ -1522,7 +1523,7 @@ Qed. Lemma fsub0set A : fset0 `<=` A. Proof. by apply/fsubsetP=> x; rewrite inE. Qed. -Hint Resolve fsub0set. +Hint Resolve fsub0set : core. Lemma fsubset0 A : (A `<=` fset0) = (A == fset0). Proof. by rewrite eqEfsubset fsub0set andbT. Qed. @@ -1791,7 +1792,7 @@ move=> sAC sBC; apply/idP/idP; last exact: fsetDS. by move=> /(@fsetDS C); rewrite !fsetDK //; apply; apply: fsubsetDl. Qed. -Hint Resolve fsubsetIl fsubsetIr fsubsetDl fsubD1set. +Hint Resolve fsubsetIl fsubsetIr fsubsetDl fsubD1set : core. (* cardinal lemmas for fsets *) @@ -2066,12 +2067,17 @@ Lemma fdisjointP_sym {A B} : reflect (forall a, a \in A -> a \notin B) [disjoint B & A]%fset. Proof. by rewrite fdisjoint_sym; apply: fdisjointP. Qed. -Lemma fdisjoint_trans A B C : - A `<=` B -> [disjoint B & C] -> [disjoint A & C]. +Lemma fdisjointWl A B C : + A `<=` B -> [disjoint B & C] -> [disjoint A & C]. Proof. move=> AsubB; rewrite -!(@disjoint_fsub (B `|` C)) ?fsetSU //. by apply: disjoint_trans; rewrite subset_fsub. Qed. +Notation fdisjoint_trans := fdisjointWl. + +Lemma fdisjointWr A B C : + A `<=` B -> [disjoint C & B] -> [disjoint C & A]. +Proof. by rewrite ![[disjoint C & _]]fdisjoint_sym; apply: fdisjointWl. Qed. Lemma fdisjoint0X A : [disjoint fset0 & A]. Proof. by rewrite -fsetI_eq0 fset0I. Qed. @@ -2112,10 +2118,8 @@ Lemma FSetK A (X : {set A}) : fsub A [fsetval k in X] = X. Proof. by apply/setP => x; rewrite !inE. Qed. End Theory. -Hint Resolve fsubset_refl. -Hint Resolve fsubset_trans. -Hint Resolve fproper_irrefl. -Hint Resolve fsub0set. +#[global] Hint Resolve fsubset_refl fsubset_trans : core. +#[global] Hint Resolve fproper_irrefl fsub0set : core. Module Import FSetInE. Definition inE := (inE, in_fsetE). @@ -2523,7 +2527,7 @@ have {PAe} -> : P = [fset x | x in A :: e]%fset. by apply/fsetP => i; rewrite !inE /= PAe inE. move=> {P} /andP[]; rewrite fset_cons => Ae ue. set E := [fset x | x in e]%fset; have Ee : E =i e by move=> x; rewrite !inE. -rewrite -Ee in Ae; move: (ih _ Ee ue) => {ih}ih. +rewrite -Ee in Ae; move: (ih _ Ee ue) => {}ih. rewrite /trivIfset /fcover !big_fsetU1 // eq_sym. have := leq_card_fcover E; rewrite -(mono_leqif (leq_add2l #|` A|)). move/(leqif_trans (leq_card_fsetU _ _)) => /= ->. @@ -2631,7 +2635,7 @@ Lemma fset_bounded_coind (T : choiceType) (P : {fset T} -> Type) (U : {fset T}): Proof. move=> Psuper X XsubU; rewrite -[X](fsetDK XsubU)//. have {XsubU}: (U `\` X) `<=` U by rewrite fsubsetDl. -elim: (_ `\` X) => {X} X IHX XsubU. +elim: (_ `\` X) => {}X IHX XsubU. apply: Psuper => Y /fsetDK<-; rewrite fproperD2l ?fsubsetDl //. by move=> /IHX; apply; rewrite fsubsetDl. Qed. @@ -2668,7 +2672,7 @@ suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|. elim: k => [|k IHk] k_lt //=; apply: (leq_ltn_trans (IHk (ltnW k_lt))). by rewrite proper_card// properEneq// set_iterF_sub neq_iter. Qed. -Hint Resolve fixsetK. +Hint Resolve fixsetK : core. Lemma minset_fix : minset [pred X | F X == X] fixset. Proof. @@ -2751,7 +2755,7 @@ Definition funsetC X := ~: (F (~: X)). Notation G := funsetC. Lemma funsetC_mono : {homo G : X Y / X \subset Y}. Proof. by move=> *; rewrite subCset setCK F_mono// subCset setCK. Qed. -Hint Resolve funsetC_mono. +Hint Resolve funsetC_mono : core. Definition cofixset := ~: fixset G. @@ -2793,7 +2797,7 @@ Proof. move=> X Y subXY; apply: subset_fsub; last by apply/F_bound/fset_sub_val. by apply/F_mono/subset_imfset/subsetP. Qed. -Hint Resolve Fsub_mono. +Hint Resolve Fsub_mono : core. Definition fixfset := [fsetval x in fixset Fsub]. @@ -2810,7 +2814,7 @@ Lemma fixfsetK : F fixfset = fixfset. Proof. by rewrite /fixfset -[in RHS]fixsetK// fset_fsub// F_bound//= fset_sub_val. Qed. -Hint Resolve fixfsetK. +Hint Resolve fixfsetK : core. Lemma fixfsetKn k : iter k F fixfset = fixfset. Proof. by rewrite iter_fix. Qed. @@ -2897,6 +2901,7 @@ Definition pred_of_finmap (K : choiceType) (V : Type) Canonical finMapPredType (K : choiceType) (V : Type) := PredType (@pred_of_finmap K V). +Declare Scope fmap_scope. Delimit Scope fmap_scope with fmap. Local Open Scope fmap_scope. Notation "f .[ kf ]" := (f [` kf]) : fmap_scope. @@ -3749,6 +3754,7 @@ Definition fsfun_choiceMixin (K V : choiceType) (d : K -> V) := Canonical fsfun_choiceType (K V : choiceType) (d : K -> V) := ChoiceType (fsfun d) (fsfun_choiceMixin d). +Declare Scope fsfun_scope. Delimit Scope fsfun_scope with fsfun. Notation "[ 'fsfun[' key ] x : aT => F | default ]" := diff --git a/index.md b/index.md new file mode 100644 index 0000000..f70bdbf --- /dev/null +++ b/index.md @@ -0,0 +1,47 @@ +--- +title: Finite maps +lang: en +header-includes: + - | + + + + + +--- + +
+View the project on GitHub +
+ +## About + +Welcome to the Finite maps project website! + +This library is an extension of mathematical component in order to +support finite sets and finite maps on choicetypes (rather that finite +types). This includes support for functions with finite support and +multisets. The library also contains a generic order and set libary, +which will be used to subsume notations for finite sets, eventually. + +This is an open source project, licensed under the CeCILL-B. + +## Get the code + +The current stable release of Finite maps can be [downloaded from GitHub](https://github.com/math-comp/finmap/releases). + +## Documentation + + +Related publications, if any, are listed below. + + +## Help and contact + +- Report issues on [GitHub](https://github.com/math-comp/finmap/issues) + +## Authors and contributors + +- Cyril Cohen +- Kazuhiko Sakaguchi + diff --git a/meta.yml b/meta.yml new file mode 100644 index 0000000..8897b6a --- /dev/null +++ b/meta.yml @@ -0,0 +1,101 @@ +fullname: Finite maps +shortname: finmap +organization: math-comp +opam_name: coq-mathcomp-finmap +community: false +action: true +coqdoc: false + +synopsis: >- + Finite sets, finite maps, finitely supported functions +description: |- + This library is an extension of mathematical component in order to + support finite sets and finite maps on choicetypes (rather that finite + types). This includes support for functions with finite support and + multisets. The library also contains a generic order and set libary, + which will be used to subsume notations for finite sets, eventually. + +authors: +- name: Cyril Cohen + initial: true +- name: Kazuhiko Sakaguchi + initial: false + +opam-file-maintainer: Cyril Cohen + +opam-file-version: dev + +license: + fullname: CeCILL-B + identifier: CECILL-B + file: CECILL-B + +supported_coq_versions: + text: Coq 8.10 to 8.12 + opam: '{ (>= "8.10" & < "8.13~") | (= "dev") }' + +tested_coq_opam_versions: +- version: '1.11.0-coq-8.10' + repo: 'mathcomp/mathcomp' +- version: '1.11.0-coq-8.11' + repo: 'mathcomp/mathcomp' +- version: '1.11.0-coq-8.12' + repo: 'mathcomp/mathcomp' +- version: '1.12.0-coq-8.10' + repo: 'mathcomp/mathcomp' +- version: '1.12.0-coq-8.11' + repo: 'mathcomp/mathcomp' +- version: '1.12.0-coq-8.12' + repo: 'mathcomp/mathcomp' +- version: 'coq-8.10' + repo: 'mathcomp/mathcomp-dev' +- version: 'coq-8.11' + repo: 'mathcomp/mathcomp-dev' +- version: 'coq-8.12' + repo: 'mathcomp/mathcomp-dev' +- version: 'coq-dev' + repo: 'mathcomp/mathcomp-dev' + +dependencies: +- opam: + name: coq-mathcomp-ssreflect + version: '{ (>= "1.11.0" & < "1.13~") | (= "dev") }' + description: |- + [MathComp ssreflect 1.10 to 1.12](https://math-comp.github.io) +- opam: + name: coq-mathcomp-bigenough + version: '{>= "1.0.0"}' + description: |- + [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough) +namespace: mathcomp.finmap + +keywords: +- name: finmap +- name: finset +- name: multiset + +documentation: |- + ## Documentation + + The documentation is available in the header of the file. + + This library will be integrated to the mathematical components + library in the near future. + + ## Related work + + This library was developed independently but inspired from + [Pierre-Yves Strub's + library](https://github.com/strub/ssrmisc/blob/master/fset.v), from + [Christian Doczkal's + library](https://www.ps.uni-saarland.de/formalizations/fset/html/libs.fset.html) + and from Beta Ziliani's work (no reference provided so far). + + Another alternative is [Arthur Azevedo de Amorim extensional + structures library](https://github.com/arthuraa/extructures). + + ## Acknowledgments + + Many thanks to Kazuhiko Sakaguchi (for the order library now moved to + the main math-comp repository) and to [various + contributors](https://github.com/math-comp/finmap/graphs/contributors) diff --git a/multiset.v b/multiset.v index af99c72..a47b940 100644 --- a/multiset.v +++ b/multiset.v @@ -4,8 +4,9 @@ (* DRAFT - PLEASE USE WITH CAUTION *) (* License CeCILL-B *) (*************************************************************************) - +Set Warnings "-notation-incompatible-format". From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq. +Set Warnings "notation-incompatible-format". From mathcomp Require Import choice path finset finfun fintype bigop tuple. Require Import finmap. @@ -46,7 +47,7 @@ Lemma sumn_map_filter I s (f : I -> nat) P : sumn [seq f i | i <- s & P i] = \sum_(i <- s | P i) f i. Proof. by rewrite sumn_map big_filter. Qed. - +Declare Scope mset_scope. Delimit Scope mset_scope with mset. Local Open Scope fset_scope. Local Open Scope fmap_scope. @@ -645,7 +646,7 @@ by have := AB a; rewrite !msetE -subn_eq0 => /eqP. Qed. Lemma msubset_refl A : A `<=` A. Proof. exact/msubsetP. Qed. -Hint Resolve msubset_refl. +Hint Resolve msubset_refl : core. Lemma msubset_trans : transitive (@msubset K). Proof. @@ -707,15 +708,15 @@ Proof. by rewrite msetUC; apply/msetUidPr. Qed. Lemma msubsetUl A B : A `<=` A `|` B. Proof. by apply/msubsetP=> a; rewrite !msetE leq_maxl. Qed. -Hint Resolve msubsetUl. +Hint Resolve msubsetUl : core. Lemma msubsetUr A B : B `<=` (A `|` B). Proof. by rewrite msetUC. Qed. -Hint Resolve msubsetUr. +Hint Resolve msubsetUr : core. Lemma msubsetU1 x A : A `<=` (x |` A). Proof. by rewrite msubsetUr. Qed. -Hint Resolve msubsetU1. +Hint Resolve msubsetU1 : core. Lemma msubsetU A B C : (A `<=` B) || (A `<=` C) -> A `<=` (B `|` C). Proof. by move=> /orP [] /msubset_trans ->. Qed. @@ -746,7 +747,7 @@ Proof. by rewrite negb_and negbK andb_orr andbN eqEmsubset. Qed. Lemma msub0set A : msubset mset0 A. Proof. by apply/msubsetP=> x; rewrite msetE. Qed. -Hint Resolve msub0set. +Hint Resolve msub0set : core. Lemma msubset0 A : (A `<=` mset0) = (A == mset0). Proof. by rewrite eqEmsubset msub0set andbT. Qed. @@ -877,7 +878,7 @@ Proof. by apply/msubsetP=> x; rewrite msetE leq_subLR leq_addl. Qed. Lemma msubD1set A x : A `\ x `<=` A. Proof. by rewrite msubsetDl. Qed. -Hint Resolve msubsetIl msubsetIr msubsetDl msubD1set. +Hint Resolve msubsetIl msubsetIr msubsetDl msubD1set : core. (* cardinal lemmas for msets *) diff --git a/package.nix b/package.nix new file mode 100644 index 0000000..e82c813 --- /dev/null +++ b/package.nix @@ -0,0 +1 @@ +"mathcomp-finmap" diff --git a/set.v b/set.v index ae67399..6d58613 100644 --- a/set.v +++ b/set.v @@ -1,7 +1,7 @@ -From mathcomp -Require Import ssreflect ssrbool eqtype ssrfun ssrnat choice seq. -From mathcomp -Require Import fintype tuple bigop path. +Set Warnings "-notation-incompatible-format". +From mathcomp Require Import ssreflect ssrbool eqtype ssrfun ssrnat choice seq. +Set Warnings "notation-incompatible-format". +From mathcomp Require Import fintype tuple bigop path. (***********************************************************************) (* Experimental library of generic sets *) @@ -14,18 +14,20 @@ Require Import fintype tuple bigop path. From mathcomp Require Import order. +Declare Scope abstract_set_scope. + Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Reserved Notation "x \subset y" (at level 70, y at next level). -Reserved Notation "x \contains y" (at level 70, y at next level, only parsing). +Reserved Notation "x \superset y" (at level 70, y at next level). Reserved Notation "x \proper y" (at level 70, y at next level). -Reserved Notation "x \containsproper y" (at level 70, y at next level, only parsing). +Reserved Notation "x \superproper y" (at level 70, y at next level). Reserved Notation "x \subset y :> T" (at level 70, y at next level). -Reserved Notation "x \contains y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x \superset y :> T" (at level 70, y at next level). Reserved Notation "x \proper y :> T" (at level 70, y at next level). -Reserved Notation "x \containsproper y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x \superproper y :> T" (at level 70, y at next level). Reserved Notation "\subsets y" (at level 35). Reserved Notation "\supersets y" (at level 35). Reserved Notation "\propersets y" (at level 35). @@ -83,9 +85,13 @@ Notation "\superpropersets y :> T" := (\superpropersets (y : T)) : abstract_set_ Notation "x \subset y" := (\sub%set x y) : abstract_set_scope. Notation "x \subset y :> T" := ((x : T) \subset (y : T)) : abstract_set_scope. +Notation "x \superset y" := (\sub%set y x) (only parsing) : abstract_set_scope. +Notation "x \superset y :> T" := ((y : T) \subset (x : T)) (only parsing) : abstract_set_scope. Notation "x \proper y" := (\proper%set x y) : abstract_set_scope. Notation "x \proper y :> T" := ((x : T) \proper (y : T)) : abstract_set_scope. +Notation "x \superproper y" := (\proper%set y x) (only parsing) : abstract_set_scope. +Notation "x \superproper y :> T" := ((y : T) \proper (x : T)) (only parsing) : abstract_set_scope. Notation "x \subset y \subset z" := ((x \subset y)%set && (y \subset z)%set) : abstract_set_scope. Notation "x \proper y \subset z" := ((x \proper y)%set && (y \subset z)%set) : abstract_set_scope. @@ -392,7 +398,7 @@ Proof. by rewrite (negPf (set1_neq0 _)). Qed. Lemma set11 x : x \in ([set x] : set X). Proof. by rewrite -sub1set. Qed. -Hint Resolve set11. +Hint Resolve set11 : core. Lemma set1_inj : injective (@set1 _ _ _ set X). Proof. diff --git a/shell.nix b/shell.nix deleted file mode 100644 index edb0dce..0000000 --- a/shell.nix +++ /dev/null @@ -1,52 +0,0 @@ -{withEmacs ? false, - nixpkgs ? (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/05f0934825c2a0750d4888c4735f9420c906b388.tar.gz"; - sha256 = "1g8c2w0661qn89ajp44znmwfmghbbiygvdzq0rzlvlpdiz28v6gy"; -}), -coq-version ? "8.11", -mc ? "1.10.0", -print-env ? false -}: -let - config.packageOverrides = pkgs: - with pkgs; rec { - coqPackages = - let coqPackages = (with pkgs; { - "8.7" = coqPackages_8_7; - "8.8" = coqPackages_8_8; - "8.9" = coqPackages_8_9; - "8.10" = coqPackages_8_10; - "8.11" = coqPackages_8_11; - }."${coq-version}"); - in - coqPackages.overrideScope' (self: super: { - mathcompPkgs = if builtins.isString mc then (super.mathcompGen mc) - else super.mathcomp.mathcompGen (o: { - version = "dev"; - name = "coq${self.coq.coq-version}-mathcomp-custom"; - src = mc; - }); - mathcomp = self.mathcompPkgs.all; - mathcomp-ssreflect = self.mathcompPkgs.ssreflect; - }); - coq = coqPackages.coq; - }; -in -with import nixpkgs {inherit config;}; -let - pgEmacs = emacsWithPackages (epkgs: - with epkgs.melpaStablePackages; [proof-general]); -in -stdenv.mkDerivation rec { - name = "env"; - env = buildEnv { name = name; paths = buildInputs; }; - buildInputs = [ coq ] ++ (with coqPackages; [mathcomp-ssreflect]) - ++ lib.optional withEmacs pgEmacs; - shellHook = '' - nixEnv (){ - echo "Here is your work environement:" - for x in $buildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done - echo "you can pass option '--argstr coq-version \"x.y\"' to nix-shell to change coq versions" - } - '' + lib.optionalString print-env "nixEnv"; -}