Skip to content

Commit 4e2a93e

Browse files
therypi8027
thery
authored and
pi8027
committed
Remove deprecated warnings
1 parent 10b430a commit 4e2a93e

File tree

4 files changed

+171
-127
lines changed

4 files changed

+171
-127
lines changed

‎src/freeg.v‎

Lines changed: 16 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -243,7 +243,7 @@ Section FreegTheory.
243243

244244
(* ------------------------------------------------------------------ *)
245245
Section ZLift.
246-
Context (R : ringType) (M : lmodType R) (K : choiceType) (f : K -> M).
246+
Context (R : pzRingType) (M : lmodType R) (K : choiceType) (f : K -> M).
247247
Implicit Types (rD : prefreeg R K) (D : {freeg K / R}) (s : seq (R * K)).
248248
Implicit Types (z k : R) (x y : K).
249249

@@ -316,7 +316,7 @@ Section FreegTheory.
316316
End ZLift.
317317

318318
(* -------------------------------------------------------------------- *)
319-
Context (R : ringType) (K : choiceType).
319+
Context (R : pzRingType) (K : choiceType).
320320
Implicit Types (rD : prefreeg R K) (D : {freeg K / R}) (s : seq (R * K)).
321321
Implicit Types (z k : R) (x y : K).
322322

@@ -476,7 +476,7 @@ Notation "<< p >>" := [freeg [:: (1, p)]].
476476
(* -------------------------------------------------------------------- *)
477477
Module FreegZmodType.
478478
Section Defs.
479-
Context (R : ringType) (K : choiceType).
479+
Context (R : pzRingType) (K : choiceType).
480480
Implicit Types (rD : prefreeg R K) (D : {freeg K / R}) (s : seq (R * K)).
481481
Implicit Types (z k : R) (x y : K).
482482

@@ -560,7 +560,7 @@ Export FreegZmodType.Exports.
560560

561561
(* -------------------------------------------------------------------- *)
562562
Section FreegZmodTypeTheory.
563-
Context (R : ringType) (K : choiceType).
563+
Context (R : pzRingType) (K : choiceType).
564564
Implicit Types (x y z : K) (k : R) (D: {freeg K / R}).
565565

566566
Local Notation coeff := (@coeff R K).
@@ -615,10 +615,6 @@ Section FreegZmodTypeTheory.
615615
by case: (eqVneq x); rewrite /= ?(mulr0, mulr1, eqxx).
616616
Qed.
617617

618-
(* -------------------------------------------------------------------*)
619-
Lemma domU1 z : dom (<< z >> : {freeg K / R}) = [:: z].
620-
Proof. by rewrite domU ?oner_eq0. Qed.
621-
622618
(* -------------------------------------------------------------------*)
623619
Lemma domN D : dom (-D) =i dom D.
624620
Proof. by move=> z; rewrite !mem_dom coeffN oppr_eq0. Qed.
@@ -746,9 +742,14 @@ Section FreegZmodTypeTheory.
746742
Qed.
747743
End FreegZmodTypeTheory.
748744

745+
(* -------------------------------------------------------------------*)
746+
Lemma domU1 (K : choiceType) (R : nzRingType) z :
747+
dom (<< z >> : {freeg K / R}) = [:: z].
748+
Proof. by rewrite domU ?oner_eq0. Qed.
749+
749750
(* -------------------------------------------------------------------- *)
750751
Section FreeglModType.
751-
Context (R : ringType) (K : choiceType).
752+
Context (R : pzRingType) (K : choiceType).
752753
Implicit Types (x y z : K) (c k : R) (D: {freeg K / R}).
753754

754755
Local Notation coeff := (@coeff R K).
@@ -786,7 +787,7 @@ End FreeglModType.
786787

787788
(* -------------------------------------------------------------------- *)
788789
Section FreeglModTheory.
789-
Context (R : ringType) (K : choiceType).
790+
Context (R : pzRingType) (K : choiceType).
790791
Implicit Types (x y z : K) (c k : R) (D : {freeg K / R}).
791792

792793
Local Notation coeff := (@coeff R K).
@@ -920,7 +921,7 @@ End FreegCmpDom.
920921

921922
(* -------------------------------------------------------------------- *)
922923
Section FreegMap.
923-
Context (G : ringType) (K : choiceType) (P : pred K) (f : G -> G).
924+
Context (G : pzRingType) (K : choiceType) (P : pred K) (f : G -> G).
924925
Implicit Types (D : {freeg K / G}).
925926

926927
Definition fgmap D := \sum_(z <- dom D | P z) << f (coeff z D) *g z >>.
@@ -1091,7 +1092,7 @@ End PosFreegDeg.
10911092

10921093
(* -------------------------------------------------------------------- *)
10931094
Section FreegIndDom.
1094-
Context (R : ringType) (K : choiceType) (F : pred K).
1095+
Context (R : pzRingType) (K : choiceType) (F : pred K).
10951096
Context (P : {freeg K / R} -> Type).
10961097
Implicit Types (D : {freeg K / R}).
10971098

@@ -1149,7 +1150,7 @@ Section FreegIndDom.
11491150
Qed.
11501151
End FreegIndDom.
11511152

1152-
Lemma freeg_ind_dom (R : ringType) (K : choiceType) (F : pred K):
1153+
Lemma freeg_ind_dom (R : pzRingType) (K : choiceType) (F : pred K):
11531154
forall (P : {freeg K / R} -> Prop),
11541155
(forall D : {freeg K / R},
11551156
[predI dom (G:=R) (K:=K) D & [predC F]] =1 pred0 -> P D)
@@ -1161,7 +1162,7 @@ Proof. by move=> P; apply/(@freeg_rect_dom R K F P). Qed.
11611162

11621163
(* -------------------------------------------------------------------- *)
11631164
Section FreegIndDom0.
1164-
Context (R : ringType) (K : choiceType) (P : {freeg K / R} -> Type).
1165+
Context (R : pzRingType) (K : choiceType) (P : {freeg K / R} -> Type).
11651166
Context (H0 : P 0).
11661167
Context (HS : forall k x D, x \notin dom D -> k != 0 ->
11671168
P D -> P (<< k *g x >> + D)).
@@ -1175,7 +1176,7 @@ Section FreegIndDom0.
11751176
Qed.
11761177
End FreegIndDom0.
11771178

1178-
Lemma freeg_ind_dom0 (R : ringType) (K : choiceType):
1179+
Lemma freeg_ind_dom0 (R : pzRingType) (K : choiceType):
11791180
forall (P : {freeg K / R} -> Prop),
11801181
P 0
11811182
-> (forall (k : R) (x : K) (D : {freeg K / R}),

‎src/monalg.v‎

Lines changed: 52 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -117,16 +117,16 @@ Module Exports. HB.reexport. End Exports.
117117
Export Exports.
118118

119119
(* -------------------------------------------------------------------- *)
120-
Definition mmorphism (M : monomType) (S : semiRingType) (f : M -> S) : Prop :=
120+
Definition mmorphism (M : monomType) (S : pzSemiRingType) (f : M -> S) : Prop :=
121121
(f 1%M = 1) * {morph f : x y / (x * y)%M >-> (x * y)%R}.
122122

123123
HB.mixin Record isMultiplicative
124-
(M : monomType) (S : semiRingType) (apply : M -> S) := {
124+
(M : monomType) (S : pzSemiRingType) (apply : M -> S) := {
125125
mmorphism_subproof : mmorphism apply;
126126
}.
127127

128128
#[mathcomp(axiom="multiplicative")]
129-
HB.structure Definition MMorphism (M : monomType) (S : semiRingType) :=
129+
HB.structure Definition MMorphism (M : monomType) (S : pzSemiRingType) :=
130130
{f of isMultiplicative M S f}.
131131

132132
Module MMorphismExports.
@@ -143,7 +143,7 @@ Export MMorphismExports.
143143
(* -------------------------------------------------------------------- *)
144144
Section MMorphismTheory.
145145

146-
Context {M : monomType} {S : semiRingType} (f : {mmorphism M -> S}).
146+
Context {M : monomType} {S : pzSemiRingType} (f : {mmorphism M -> S}).
147147

148148
Lemma mmorph1 : f 1%M = 1.
149149
Proof. exact: mmorphism_subproof.1. Qed.
@@ -191,10 +191,10 @@ Definition msupp (g : {malg G[K]}) : {fset K} := finsupp (malg_val g).
191191

192192
End MalgBaseOp.
193193

194-
Arguments mcoeff {K G} x%monom_scope g%ring_scope.
194+
Arguments mcoeff {K G} x%_monom_scope g%_ring_scope.
195195
Arguments mkmalg {K G} _.
196-
Arguments mkmalgU {K G} k%monom_scope x%ring_scope.
197-
Arguments msupp {K G} g%ring_scope.
196+
Arguments mkmalgU {K G} k%_monom_scope x%_ring_scope.
197+
Arguments msupp {K G} g%_ring_scope.
198198

199199
(* -------------------------------------------------------------------- *)
200200
Notation "g @_ k" := (mcoeff k g).
@@ -420,7 +420,7 @@ End MalgZmodTheory.
420420
(* -------------------------------------------------------------------- *)
421421
Section MalgSemiRingTheory.
422422

423-
Context {K : choiceType} {R : semiRingType}.
423+
Context {K : choiceType} {R : pzSemiRingType}.
424424

425425
Implicit Types (g : {malg R[K]}).
426426

@@ -533,7 +533,7 @@ End MalgMonomTheory.
533533
(* -------------------------------------------------------------------- *)
534534
Section MalgSemiRingTheory.
535535

536-
Context (K : monomType) (R : semiRingType).
536+
Context (K : monomType) (R : pzSemiRingType).
537537

538538
Implicit Types (g : {malg R[K]}) (k l : K).
539539

@@ -656,11 +656,8 @@ rewrite [LHS](big_morph (fgmul _) (fun _ _ => fgmulgDr _ _ _) (fgmulg0 _)).
656656
by rewrite fgmulEr1; apply/eq_bigr=> k3 _; rewrite !fgmulUU mulrA mulmA.
657657
Qed.
658658

659-
Lemma fgoner_eq0 : fgone != 0.
660-
Proof. by apply/eqP/malgP=> /(_ 1%M) /eqP; rewrite !mcoeffsE oner_eq0. Qed.
661-
662-
HB.instance Definition _ := GRing.Nmodule_isSemiRing.Build {malg R[K]}
663-
fgmulA fgmul1g fgmulg1 fgmulgDl fgmulgDr fgmul0g fgmulg0 fgoner_eq0.
659+
HB.instance Definition _ := GRing.Nmodule_isPzSemiRing.Build {malg R[K]}
660+
fgmulA fgmul1g fgmulg1 fgmulgDl fgmulgDr fgmul0g fgmulg0.
664661

665662
Lemma malgM_def g1 g2 : g1 * g2 = fgmul g1 g2.
666663
Proof. by []. Qed.
@@ -674,15 +671,9 @@ Qed.
674671
Lemma fgscaleAl c g1 g2 : c *: (g1 * g2) = (c *: g1) * g2.
675672
Proof. by rewrite -!mul_malgC mulrA. Qed.
676673

677-
HB.instance Definition _ :=
678-
GRing.LSemiModule_isLSemiAlgebra.Build R {malg R[K]} fgscaleAl.
679-
680674
Lemma mcoeffU1 k k' : (<< k >> : {malg R[K]})@_k' = (k == k')%:R.
681675
Proof. by rewrite mcoeffU. Qed.
682676

683-
Lemma msuppU1 k : @msupp _ R << k >> = [fset k].
684-
Proof. by rewrite msuppU oner_eq0. Qed.
685-
686677
Lemma malgME g1 g2 :
687678
g1 * g2 = \sum_(k1 <- msupp g1) \sum_(k2 <- msupp g2)
688679
<< g1@_k1 * g2@_k2 *g k1 * k2 >>.
@@ -794,14 +785,26 @@ HB.instance Definition _ :=
794785

795786
End MalgSemiRingTheory.
796787

797-
(* FIXME: HB.saturate *)
798-
HB.instance Definition _ (K : monomType) (R : ringType) :=
799-
GRing.SemiRing.on {malg R[K]}.
788+
(* -------------------------------------------------------------------- *)
789+
Section MalgNzSemiRingTheory.
790+
791+
Context (K : monomType) (R : nzSemiRingType).
792+
793+
Lemma fgoner_eq0 : 1 != 0 :> {malg R[K]}.
794+
Proof. by apply/eqP/malgP=> /(_ 1%M) /eqP; rewrite !mcoeffsE oner_eq0. Qed.
795+
796+
HB.instance Definition _ :=
797+
GRing.PzSemiRing_isNonZero.Build {malg R[K]} fgoner_eq0.
798+
799+
HB.instance Definition _ :=
800+
GRing.LSemiModule_isLSemiAlgebra.Build R {malg R[K]} (@fgscaleAl K R).
801+
802+
End MalgNzSemiRingTheory.
800803

801804
(* -------------------------------------------------------------------- *)
802805
Section MalgComSemiRingType.
803806

804-
Context {K : conomType} {R : comSemiRingType}.
807+
Context {K : conomType} {R : comPzSemiRingType}.
805808

806809
Lemma fgmulC : @commutative {malg R[K]} _ *%R.
807810
Proof.
@@ -811,25 +814,37 @@ by rewrite mulrC [X in X==k]mulmC.
811814
Qed.
812815

813816
HB.instance Definition _ :=
814-
GRing.SemiRing_hasCommutativeMul.Build {malg R[K]} fgmulC.
817+
GRing.PzSemiRing_hasCommutativeMul.Build {malg R[K]} fgmulC.
818+
819+
End MalgComSemiRingType.
820+
821+
(* -------------------------------------------------------------------- *)
822+
Section MalgNzComSemiRingType.
815823

824+
Context {K : conomType} {R : comNzSemiRingType}.
825+
826+
HB.instance Definition _ := GRing.ComPzSemiRing.on {malg R[K]}.
816827
HB.instance Definition _ :=
817828
GRing.LSemiAlgebra_isComSemiAlgebra.Build R {malg R[K]}.
818829

819-
End MalgComSemiRingType.
830+
End MalgNzComSemiRingType.
820831

821832
(* FIXME: HB.saturate *)
822-
HB.instance Definition _ (K : monomType) (R : ringType) :=
823-
GRing.Lmodule.on {malg R[K]}.
824-
HB.instance Definition _ (K : conomType) (R : comRingType) :=
825-
GRing.Lmodule.on {malg R[K]}.
833+
HB.instance Definition _ (K : monomType) (R : pzRingType) :=
834+
GRing.PzSemiRing.on {malg R[K]}.
835+
HB.instance Definition _ (K : monomType) (R : nzRingType) :=
836+
GRing.NzSemiRing.on {malg R[K]}.
837+
HB.instance Definition _ (K : conomType) (R : comPzRingType) :=
838+
GRing.ComPzSemiRing.on {malg R[K]}.
839+
HB.instance Definition _ (K : conomType) (R : comNzRingType) :=
840+
GRing.ComNzSemiRing.on {malg R[K]}.
826841
(* /FIXME *)
827842

828843
(* -------------------------------------------------------------------- *)
829844
Section MalgMorphism.
830845
Section Defs.
831846

832-
Context {K : choiceType} {G : nmodType} {S : semiRingType}.
847+
Context {K : choiceType} {G : nmodType} {S : pzSemiRingType}.
833848
Context (f : G -> S) (h : K -> S).
834849

835850
Definition mmap g := \sum_(k <- msupp g) f g@_k * h k.
@@ -843,7 +858,7 @@ Local Notation "g ^[ f , h ]" := (mmap f h g).
843858

844859
Section SemiAdditive.
845860

846-
Context {K : choiceType} {G : nmodType} {S : semiRingType}.
861+
Context {K : choiceType} {G : nmodType} {S : pzSemiRingType}.
847862

848863
Lemma mmapEw (d : {fset K}) g : msupp g `<=` d ->
849864
forall (f : {additive G -> S}) (h : K -> S),
@@ -879,7 +894,7 @@ End SemiAdditive.
879894

880895
Section Additive.
881896

882-
Context {K : choiceType} {G : zmodType} {S : ringType}.
897+
Context {K : choiceType} {G : zmodType} {S : pzRingType}.
883898
Context (f : {additive G -> S}) (h : K -> S).
884899

885900
Lemma mmapN : {morph mmap f h: x / - x} . Proof. exact: raddfN. Qed.
@@ -890,7 +905,7 @@ End Additive.
890905

891906
Section CommrMultiplicative.
892907

893-
Context {K : monomType} {R S : semiRingType}.
908+
Context {K : monomType} {R S : pzSemiRingType}.
894909
Context (f : {rmorphism R -> S}) (h : {mmorphism K -> S}).
895910

896911
Implicit Types (c : R) (g : {malg R[K]}).
@@ -922,7 +937,7 @@ End CommrMultiplicative.
922937
(* -------------------------------------------------------------------- *)
923938
Section Multiplicative.
924939

925-
Context {K : monomType} {R : semiRingType} {S : comSemiRingType}.
940+
Context {K : monomType} {R : pzSemiRingType} {S : comPzSemiRingType}.
926941
Context (f : {rmorphism R -> S}) (h : {mmorphism K -> S}).
927942

928943
Lemma mmap_is_multiplicative : multiplicative (mmap f h).
@@ -937,7 +952,7 @@ End Multiplicative.
937952
(* -------------------------------------------------------------------- *)
938953
Section Linear.
939954

940-
Context {K : monomType} {R : comSemiRingType} (h : {mmorphism K -> R}).
955+
Context {K : monomType} {R : comPzSemiRingType} (h : {mmorphism K -> R}).
941956

942957
Lemma mmap_is_linear : scalable_for *%R (mmap idfun h).
943958
Proof. by move=> /= c g; rewrite -mul_malgC rmorphM /= mmapC. Qed.
@@ -1037,7 +1052,7 @@ End MonalgOverOpp.
10371052
(* -------------------------------------------------------------------- *)
10381053
Section MonalgOverSemiring.
10391054

1040-
Context (K : monomType) (R : semiRingType) (S : semiringClosed R).
1055+
Context (K : monomType) (R : pzSemiRingType) (S : semiringClosed R).
10411056

10421057
Local Notation monalgOver := (@monalgOver K R).
10431058

0 commit comments

Comments
 (0)