From 41c7fa558122fd44ee31b1b9e923691b8e0e7b70 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 2 Dec 2024 12:17:44 +0900 Subject: [PATCH] nitpick --- CHANGELOG_UNRELEASED.md | 1 - finmap.v | 16 ++++++++-------- multiset.v | 2 +- 3 files changed, 9 insertions(+), 10 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6e9d7a0..0dae9da 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -5,7 +5,6 @@ ### Added - in `finmap.v`: - + lemmas `bigfcup_imfset1`, `fbig_pred1_inj` + lemmas `fset_seq1`, `imfset0`, `imfset_fset1`, `imfset_fset2`, `imfsetU`, `imfsetU1`, `imfsetI`, `bigfcup_imfset` diff --git a/finmap.v b/finmap.v index 2fa2d7c..3911b52 100644 --- a/finmap.v +++ b/finmap.v @@ -5,7 +5,7 @@ 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". -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, *) @@ -2189,12 +2189,12 @@ Proof. by rewrite imfsetU imfset_fset1. Qed. Lemma imfsetI f A B : {in A & B, injective f} -> f @` (A `&` B) = f @` A `&` f @` B. Proof. - move=> injf; apply/fsetP => v. - apply/imfsetP/fsetIP => /=. - by move=> [k /fsetIP [kinA kinB] ->]; split; apply/imfsetP; exists k. - move=> [/imfsetP /= [ka kainA eqka] /imfsetP /= [kb kbinB eqkb]]. - have eqk : ka = kb by apply: injf => //; rewrite -eqka -eqkb. - by exists ka => //; apply/fsetIP; split=> //; rewrite eqk. +move=> injf; apply/fsetP => v. +apply/imfsetP/fsetIP => /=. + by move=> [k /fsetIP [kinA kinB] ->]; split; apply/imfsetP; exists k. +move=> [/imfsetP /= [ka kainA eqka] /imfsetP /= [kb kbinB eqkb]]. +have eqk : ka = kb by apply: injf => //; rewrite -eqka -eqkb. +by exists ka => //; apply/fsetIP; split=> //; rewrite eqk. Qed. End ImfsetTh. @@ -2523,7 +2523,7 @@ Implicit Types (f : I -> T). Lemma bigfcup_imfset1 (P : {fset I}) f : \bigcup_(i <- P) [fset f i] = f @` P. Proof. apply/eqP; rewrite eqEfsubset; apply/andP; split; apply/fsubsetP => x. -- by case/bigfcupP=> i /andP [] iP _; rewrite inE => /eqP ->; apply/imfsetP; exists i. +- by case/bigfcupP=> i /andP [] iP _ /[!inE] /eqP ->; apply/imfsetP; exists i. - case/imfsetP => i /= iP ->; apply/bigfcupP; exists i; rewrite ?andbT //. by apply/imfsetP; exists (f i); rewrite ?inE. Qed. diff --git a/multiset.v b/multiset.v index a665284..4107eb0 100644 --- a/multiset.v +++ b/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. (*****************************************************************************)