Merge pull request #104 from thery/codomf_cat

add the theorem codomf_cat

.github/workflows/docker-action.yml

@@ -17,8 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
@@ -36,12 +34,13 @@ jobs:
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - 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

README.md

@@ -26,7 +26,7 @@ which will be used to subsume notations for finite sets, eventually.
 - License: [CeCILL-B](CECILL-B)
 - Compatible Coq versions: Coq 8.13 to 8.16
 - Additional dependencies:
-  - [MathComp ssreflect 1.12 to 1.15](https://math-comp.github.io)
+  - [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io)
 - Coq namespace: `mathcomp.finmap`
 - Related publication(s): none
 

coq-mathcomp-finmap.opam

@@ -22,7 +22,7 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.16~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev") }
 ]
 
 tags: [

finmap.v

@@ -3587,6 +3587,18 @@ move: fk'_eq; rewrite fnd_set.
 by have [->|//] := altP eqP; rewrite fnd_rem inE eqxx.
 Qed.
 
+Lemma codomf_cat (f g : {fmap K -> V}) :
+  codomf (f + g) = codomf g `|` codomf f.[\domf g].
+Proof.
+apply/fsetP => v'; rewrite !inE.
+apply/codomfP/(orPP (codomfP _ _) (codomfP _ _)); last first.
+  move=> [] [x xI]; exists x; rewrite fnd_cat; first by case: fndP xI.
+  by move: xI; rewrite fnd_rem; case: ifP.
+move=> []x; rewrite fnd_cat; case: fndP => // [xg gx|xNg fx].
+  by left; exists x; rewrite in_fnd.
+by right; exists x; rewrite fnd_rem ifN.
+Qed.
+
 End FinMapKeyType.
 
 Module Import FinmapInE.

meta.yml

@@ -35,10 +35,6 @@ supported_coq_versions:
   opam: '{ (>= "8.13" & < "8.17~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '1.12.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'
@@ -73,9 +69,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.12.0" & < "1.16~") | (= "dev") }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
   description: |-
-    [MathComp ssreflect 1.12 to 1.15](https://math-comp.github.io)
+    [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io)
 
 namespace: mathcomp.finmap