fixes #113

CHANGELOG.md

@@ -1,6 +1,15 @@
 # Changelog
 
-Last release: [[1.5.2] - 2022-07-06](#152---2022-07-06)
+Last release: [[2.1.0] - 2024-01-17](#210---2024-01-17)
+
+## [2.1.0] - 2024-01-17
+
+no documentation
+
+## [2.0.0] - 2023-05-23
+
+- in `finmap.v`:
+  + lemmas `bigfcup_imfset1`, `fbig_pred1_inj`
 
 ## [1.5.2] - 2022-07-06
 

CHANGELOG_UNRELEASED.md

@@ -4,11 +4,11 @@
 
 ### Added
 
-- in `finmap.v`:
-  + lemmas `bigfcup_imfset`, `fbig_pred1_inj`
-
 ### Changed
 
+- in `finmap.v`
+  + lemma `partition_disjoint_bigfcup` generalized
+
 ### Renamed
 
 ### Removed

finmap.v

@@ -5,7 +5,7 @@
 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.
+From mathcomp Require Import choice finset finfun fintype bigop.
 
 (*****************************************************************************)
 (* This file provides representations for finite sets over a choiceType K,   *)
@@ -146,10 +146,10 @@
 Reserved Notation "A `=P` B" (at level 70, no associativity).
 
 Reserved Notation "f @`[ key ] A" (at level 24, key at level 0).
 Reserved Notation "f @2`[ key ] ( A , B )"
   (at level 24, format "f  @2`[ key ]  ( A ,  B )").
 Reserved Notation "f @` A" (at level 24).
 Reserved Notation "f @2` ( A , B )" (at level 24, format "f  @2`  ( A ,  B )").
 
 (* unary *)
 Reserved Notation "[ 'fset' E | x : T 'in' A ]" (at level 0, E, x at level 99).
@@ -167,9 +167,9 @@
 Reserved Notation "[ 'fset' x 'in' A | P & Q ]" (at level 0, x at level 99).
 
 (* binary *)
 Reserved Notation "[ 'fset' E | x : T 'in' A , y : T' 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset' E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 
 (* keyed parse only *)
@@ -182,11 +182,11 @@
   (at level 0, E, x at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A & P ]"
   (at level 0, E, x at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : T 'in' A , y : T' 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A , y : B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A , y 'in' B ]"
   (at level 0, E, x, y at level 99).
@@ -232,7 +232,7 @@
 Reserved Notation "[ 'f' 'set' x 'in' A | P & Q ]"
   (at level 0, x at level 99, format "[ 'f' 'set'  x  'in'  A  |  P  &  Q ]").
 (* binary printing only *)
 Reserved Notation "[ 'f' 'set' E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99,
    format "[ '[hv' 'f' 'set'  E '/ '  |  x  'in'  A , '/' y  'in'  B ] ']'").
 
@@ -354,9 +354,9 @@
            format "'[' \bigcup_ ( i  'in'  A ) '/  '  F ']'").
 
 Reserved Notation "{fmap T }" (at level 0, format "{fmap  T }").
 Reserved Notation "x .[ k <- v ]"
   (at level 2, left associativity, format "x .[ k  <-  v ]").
 Reserved Notation "x .[~ k ]" (at level 2, k at level 200, format "x .[~  k ]").
 Reserved Notation "x .[& k ]" (at level 2, k at level 200, format "x .[&  k ]").
 Reserved Notation "x .[\ k ]" (at level 2, k at level 200, format "x .[\  k ]").
 Reserved Notation "x .[? k ]" (at level 2, k at level 200, format "x .[?  k ]").
@@ -2607,21 +2607,24 @@
 
 Lemma partition_disjoint_bigfcup (f : T -> R) (F : I -> {fset T})
   (K : {fset I}) :
-  (forall i j, i != j -> [disjoint F i & F j])%fset ->
+  (forall i j, i \in K -> j \in K -> i != j -> [disjoint F i & F j])%fset ->
   \big[op/idx]_(i <- \big[fsetU/fset0]_(x <- K) (F x)) f i =
   \big[op/idx]_(k <- K) (\big[op/idx]_(i <- F k) f i).
 Proof.
 move=> disjF; pose P := [fset F i | i in K & F i != fset0]%fset.
 have trivP : trivIfset P.
-  apply/trivIfsetP => _ _ /imfsetP[i _ ->] /imfsetP[j _ ->] neqFij.
-  by apply: disjF; apply: contraNneq neqFij => ->.
+  apply/trivIfsetP => _ _ /imfsetP[i iK ->] /imfsetP[j jK ->] neqFij.
+  move: iK; rewrite !inE/= => /andP[iK Fi0].
+  move: jK; rewrite !inE/= => /andP[jK Fj0].
+  by apply: (disjF _ _ iK jK); apply: contraNneq neqFij => ->.
 have -> : (\bigcup_(i <- K) F i)%fset = fcover P.
   apply/esym; rewrite /P fcover_imfset big_mkcond /=; apply eq_bigr => i _.
   by case: ifPn => // /negPn/eqP.
-rewrite big_trivIfset // /rhs big_imfset => [|i j _ /andP[jK notFj0] eqFij] /=.
+rewrite big_trivIfset // /rhs big_imfset => [|i j iK /andP[jK notFj0] eqFij] /=.
   rewrite big_filter big_mkcond; apply eq_bigr => i _.
   by case: ifPn => // /negPn /eqP ->;  rewrite big_seq_fset0.
-by apply: contraNeq (disjF _ _) _; rewrite -fsetI_eq0 eqFij fsetIid.
+move: iK; rewrite !inE/= => /andP[iK Fi0].
+by apply: contraNeq (disjF _ _ iK jK) _; rewrite -fsetI_eq0 eqFij fsetIid.
 Qed.
 
 End FsetBigOps.

multiset.v

@@ -7,7 +7,7 @@
 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.
+From mathcomp Require Import choice finset finfun fintype bigop tuple.
 Require Import finmap.
 
 (*****************************************************************************)