From eee1ccbb4be43a1c4fb233c4c10a2852d3983d6f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 25 Feb 2026 15:11:28 +0100 Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1545 --- finmap.v | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/finmap.v b/finmap.v index 00ec186..208378a 100644 --- a/finmap.v +++ b/finmap.v @@ -136,6 +136,7 @@ From mathcomp Require Import choice finset finfun fintype bigop. (* fsinjectiveb f == boolean predicate of injectivity of f *) (*****************************************************************************) +Unset SsrOldRewriteGoalsOrder. (* remove this line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. @@ -1918,7 +1919,7 @@ Proof. by rewrite -!fsubset0 fsubUset. Qed. Lemma fsubsetD1 A B x : (A `<=` B `\ x) = (A `<=` B) && (x \notin A). Proof. do !rewrite -(@subset_fsubE (x |` A `|` B)) ?fsubDset ?fsetUA // 1?fsetUAC //. -rewrite fsubD1 => [|mem_x]; first by rewrite -fsetUA fset1U1. +rewrite fsubD1 => [mem_x|]; last by rewrite -fsetUA fset1U1. by rewrite subsetD1 // inE. Qed. @@ -1971,9 +1972,9 @@ Qed. Lemma fsetDpS C A B : B `<=` C -> A `<` B -> C `\` B `<` C `\` A. Proof. move=> subBC subAB; rewrite fproperEneq fsetDS 1?fproper_sub// andbT. -apply/negP => /eqP /(congr1 (fsetD C)); rewrite !fsetDK // => [eqAB//|]. - by rewrite eqAB (negPf (fproper_irrefl _)) in subAB. -by apply: fsubset_trans subBC; apply: fproper_sub. +apply/negP => /eqP /(congr1 (fsetD C)); rewrite !fsetDK // => [|eqAB//]. + by apply: fsubset_trans subBC; apply: fproper_sub. +by rewrite eqAB (negPf (fproper_irrefl _)) in subAB. Qed. Lemma fproperD2l C A B : A `<=` C -> B `<=` C -> (C `\` B `<` C `\` A) = (A `<` B). @@ -2027,7 +2028,7 @@ Proof. pose D := A `|` B `|` C. have AD : A `<=` D by rewrite /D -fsetUA fsubsetUl. have BD : B `<=` D by rewrite /D fsetUAC fsubsetUr. -rewrite -(@subset_fsubE D) //; last first. +rewrite -(@subset_fsubE D) //. by rewrite fsubDset (fsubset_trans BD) // fsubsetUr. rewrite fsubD subsetD !subset_fsubE // disjoint_fsub //. by rewrite /D fsetUAC fsubsetUl. @@ -2251,7 +2252,7 @@ Proof. by apply/fsetP=> X; rewrite inE !fpowersetE fsubsetI. Qed. Lemma card_fpowerset (A : {fset K}) : #|` fpowerset A| = 2 ^ #|` A|. Proof. -rewrite !card_imfset; first by rewrite -cardE card_powerset cardsE cardfE. +rewrite !card_imfset; last by rewrite -cardE card_powerset cardsE cardfE. by move=> X Y /fsetP eqXY; apply/setP => x; have := eqXY (val x); rewrite !inE. Qed. @@ -2395,7 +2396,7 @@ Lemma big_fset_incl (A : {fset I}) B F : A `<=` B -> \big[op/idx]_(x <- A) F x = \big[op/idx]_(x <- B) F x. Proof. move=> subAB Fid; rewrite [in RHS](big_fsetID (mem A)) /=. -rewrite [X in op _ X]big1_fset ?Monoid.mulm1; last first. +rewrite [X in op _ X]big1_fset ?Monoid.mulm1. by move=> i; rewrite !inE /= => /andP[iB iNA _]; apply: Fid. by apply: eq_fbigl => i; rewrite !inE /= -(@in_fsetI _ B A) (fsetIidPr _). Qed. @@ -2441,7 +2442,7 @@ Lemma pair_big_dep_cond (A : {fset I}) (B : I -> {fset J}) \big[op/idx]_(p <- [fset ((i, j) : I * J) | i in [fset i in A | P i], j in [fset j in B i | Q i j]]) F p.1 p.2. Proof. -rewrite big_imfset2 //=; last by move=> [??] [??] _ _ /= [-> ->]. +rewrite big_imfset2 //=; first by move=> [??] [??] _ _ /= [-> ->]. by rewrite big_fset /=; apply: eq_bigr => i _; rewrite big_fset. Qed. End BigFsetDep. @@ -2466,8 +2467,8 @@ transitivity (\big[op/idx]_(i <- [fset ij | ij in by rewrite in_imfset. by move=> /andP[/allpairsP[[/= j i] [/imfsetP[/=a aA ->] iA ->/= /eqP<-]]]; exists i. rewrite eq_big_imfset //= big_map undup_id. - by rewrite big_allpairs; apply: eq_bigr => i /= _; rewrite -big_mkcond. -by rewrite allpairs_uniq => //= -[j0 i0] [j1 i1] /=. + by rewrite allpairs_uniq => //= -[j0 i0] [j1 i1] /=. +by rewrite big_allpairs; apply: eq_bigr => i /= _; rewrite -big_mkcond. Qed. End BigComImfset. @@ -2662,7 +2663,7 @@ have {tI} : {in enum_fset P &, forall A B, A != B -> [disjoint A & B]%fset}. by []. elim: (enum_fset P) (fset_uniq P) => [_|h t ih /= /andP[ht ut] tP]. by rewrite !big_nil. -rewrite !big_cons -ih //; last first. +rewrite !big_cons -ih //. by move=> x y xt yt xy; apply tP => //; rewrite !inE ?(xt,yt) orbT. rewrite {1}/fsetU big_imfset //= undup_cat /= big_cat !undup_id //. congr (op _ _). @@ -2691,11 +2692,11 @@ have trivP : trivIfset P. 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 iK /andP[jK notFj0] eqFij] /=. - rewrite big_filter big_mkcond; apply eq_bigr => i _. - by case: ifPn => // /negPn /eqP ->; rewrite big_seq_fset0. -move: iK; rewrite !inE/= => /andP[iK Fi0]. -by apply: contraNeq (disjF _ _ iK jK) _; rewrite -fsetI_eq0 eqFij fsetIid. +rewrite big_trivIfset // /rhs big_imfset => [i j iK /andP[jK notFj0] eqFij|] /=. + move: iK; rewrite !inE/= => /andP[iK Fi0]. + by apply: contraNeq (disjF _ _ iK jK) _; rewrite -fsetI_eq0 eqFij fsetIid. +rewrite big_filter big_mkcond; apply eq_bigr => i _. +by case: ifPn => // /negPn /eqP ->; rewrite big_seq_fset0. Qed. End FsetBigOps.