Skip to content

Adapt to https://github.com/math-comp/math-comp/pull/1545 #152

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
proux01 wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Adapt to https://github.com/math-comp/math-comp/pull/1545 #152

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 17 additions & 16 deletions finmap.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,7 @@
(* 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.
Expand All @@ -147,10 +148,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 )"

Check warning on line 151 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Postfix notations (i.e. starting with a nonterminal symbol and

Check warning on line 151 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Postfix notations (i.e. starting with a nonterminal symbol and

Check warning on line 151 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Postfix notations (i.e. starting with a nonterminal symbol and
(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 )").

Check warning on line 154 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Postfix notations (i.e. starting with a nonterminal symbol and

Check warning on line 154 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Postfix notations (i.e. starting with a nonterminal symbol and

Check warning on line 154 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Postfix notations (i.e. starting with a nonterminal symbol and

(* unary *)
Reserved Notation "[ 'fset' E | x : T 'in' A ]" (at level 0, E, x at level 99).
Expand All @@ -168,9 +169,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 ]"

Check warning on line 172 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 172 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 172 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0
(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 ]"

Check warning on line 174 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 174 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 174 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
(at level 0, E, x at level 99, A at level 200, y at level 99).

(* keyed parse only *)
Expand All @@ -183,11 +184,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 ]"

Check warning on line 187 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 187 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 187 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
(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 ]"

Check warning on line 189 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Check warning on line 189 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Check warning on line 189 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
(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 ]"

Check warning on line 191 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 191 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 191 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
(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).
Expand Down Expand Up @@ -233,7 +234,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 ]"

Check warning on line 237 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 237 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 237 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
(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 ] ']'").

Expand Down Expand Up @@ -484,7 +485,7 @@
Notation "{fset T }" := (@finset_of _ (Phant T)) : type_scope.

Definition pred_of_finset (K : choiceType)
(f : finSet K) : pred K := fun k => k \in (enum_fset f).

Check warning on line 488 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 488 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 488 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Canonical finSetPredType (K : choiceType) := PredType (@pred_of_finset K).

Section FinSetCanonicals.
Expand Down Expand Up @@ -1918,7 +1919,7 @@
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.

Expand Down Expand Up @@ -1971,9 +1972,9 @@
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).
Expand Down Expand Up @@ -2027,7 +2028,7 @@
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.
Expand Down Expand Up @@ -2251,7 +2252,7 @@

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.

Expand Down Expand Up @@ -2395,7 +2396,7 @@
\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.
Expand Down Expand Up @@ -2441,7 +2442,7 @@
\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.
Expand All @@ -2466,8 +2467,8 @@
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.
Expand Down Expand Up @@ -2662,7 +2663,7 @@
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 _ _).
Expand Down Expand Up @@ -2691,11 +2692,11 @@
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.
Expand Down Expand Up @@ -2976,7 +2977,7 @@
(* Finite Maps *)
(***************)

Section DefMap.

Check warning on line 2980 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 2980 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 2980 in finmap.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Variables (K : choiceType) (V : Type).

Record finMap : Type := FinMap {
Expand Down
Loading