Merge pull request #75 from proux01/hint_locality

[CI] Test Coq 8.17 and MC 1.16.0
coq-community · Mar 13, 2023 · e3806b2 · e3806b2
2 parents 47a7583 + 9172275
commit e3806b2
Show file tree

Hide file tree

Showing 28 changed files with 568 additions and 567 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,18 +17,15 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.15'
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
           - 'mathcomp/mathcomp:1.15.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.13'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.13'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp-dev:coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.16'
+          - 'mathcomp/mathcomp-dev:coq-8.17'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

diff --git a/_CoqProject b/_CoqProject
@@ -6,8 +6,10 @@
 -arg -w -arg +duplicate-clear
 -arg -w -arg +non-primitive-record
 -arg -w -arg +undeclared-scope
--arg -w -arg -deprecated-hint-without-locality
--arg -w -arg -deprecated-ident-entry
+-arg -w -arg +deprecated-hint-without-locality
+-arg -w -arg +deprecated-hint-rewrite-without-locality
+-arg -w -arg +deprecated-ident-entry
+-arg -w -arg +deprecated-typeclasses-transparency-without-locality
 -arg -w -arg -ambiguous-paths
 -arg -w -arg +implicit-core-hint-db
 

diff --git a/coq-coqeal.opam b/coq-coqeal.opam
@@ -21,11 +21,11 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.13" & < "8.17~") | (= "dev")}
+  "coq" {(>= "8.15" & < "8.18~") | (= "dev")}
   "coq-bignums" 
   "coq-paramcoq" {>= "1.1.3"}
   "coq-mathcomp-multinomials" {((>= "1.5.1" & < "1.7~") | = "dev")}
-  "coq-mathcomp-algebra" {((>= "1.13.0" & < "1.16~") | = "dev")}
+  "coq-mathcomp-algebra" {((>= "1.13.0" & < "1.17~") | = "dev")}
   "coq-mathcomp-real-closed" {(>= "1.1.2" & < "1.2~") | (= "dev")}
 ]
 

diff --git a/refinements/bareiss_eff.v b/refinements/bareiss_eff.v
@@ -309,32 +309,32 @@ Context `{forall n1 n2 (rn : nat_R n1 n2),
                   (@char_poly_mxC n2)}.
 Context `{!refines (RpolyC ==> rC) head headC}.
 
-Global Instance RpolyC_bareiss_rec m1 m2 (rm : nat_R m1 m2) :
+#[export] Instance RpolyC_bareiss_rec m1 m2 (rm : nat_R m1 m2) :
   refines (RpolyC ==> RmxpolyC (nat_R_S_R rm) (nat_R_S_R rm) ==> RpolyC)
           (bareiss_rec (polyR:={poly R}) (mxpolyR:=matrix {poly R}) (m:=m1))
           (bareiss_rec (polyR:=polyC) (mxpolyR:=mxpolyC) (m:=m2)).
 Proof. param bareiss_rec_R. Qed.
 
-Global Instance refine_bareiss_rec m :
+#[export] Instance refine_bareiss_rec m :
   refines (RpolyC ==> RmxpolyC (nat_R_S_R (nat_Rxx m)) (nat_R_S_R (nat_Rxx m))
                   ==> RpolyC)
           (bareiss_rec (polyR:={poly R}) (mxpolyR:=matrix {poly R}) (m:=m))
           (bareiss_rec (polyR:=polyC) (mxpolyR:=mxpolyC) (m:=m)).
 Proof. exact: RpolyC_bareiss_rec. Qed.
 
-Global Instance RpolyC_bareiss n1 n2 (rn : nat_R n1 n2) :
+#[export] Instance RpolyC_bareiss n1 n2 (rn : nat_R n1 n2) :
   refines (RmxpolyC (nat_R_S_R rn) (nat_R_S_R rn) ==> RpolyC)
           (bareiss (polyR:={poly R}) (mxpolyR:=matrix {poly R}) (n:=n1))
           (bareiss (polyR:=polyC) (mxpolyR:=mxpolyC) (n:=n2)).
 Proof. param bareiss_R. Qed.
 
-Global Instance refine_bareiss n :
+#[export] Instance refine_bareiss n :
   refines (RmxpolyC (nat_R_S_R (nat_Rxx n)) (nat_R_S_R (nat_Rxx n)) ==> RpolyC)
           (bareiss (polyR:={poly R}) (mxpolyR:=matrix {poly R}) (n:=n))
           (bareiss (polyR:=polyC) (mxpolyR:=mxpolyC) (n:=n)).
 Proof. exact: RpolyC_bareiss. Qed.
 
-Global Instance RpolyC_bareiss_char_poly n1 n2 (rn : nat_R n1 n2) :
+#[export] Instance RpolyC_bareiss_char_poly n1 n2 (rn : nat_R n1 n2) :
   refines (RmxC (nat_R_S_R rn) (nat_R_S_R rn) ==> RpolyC)
           (bareiss_char_poly (polyR:={poly R}) (mxR:=matrix R)
                              (mxpolyR:=matrix {poly R}) (@char_poly_mx R)
@@ -343,7 +343,7 @@ Global Instance RpolyC_bareiss_char_poly n1 n2 (rn : nat_R n1 n2) :
                              char_poly_mxC (n:=n2)).
 Proof. param bareiss_char_poly_R. Qed.
 
-Global Instance refine_bareiss_char_poly n :
+#[export] Instance refine_bareiss_char_poly n :
   refines (RmxC (nat_R_S_R (nat_Rxx n)) (nat_R_S_R (nat_Rxx n)) ==> RpolyC)
           (bareiss_char_poly (polyR:={poly R}) (mxR:=matrix R)
                              (mxpolyR:=matrix {poly R}) (@char_poly_mx R)
@@ -352,7 +352,7 @@ Global Instance refine_bareiss_char_poly n :
                              char_poly_mxC (n:=n)).
 Proof. exact: RpolyC_bareiss_char_poly. Qed.
 
-Global Instance RC_bdet n1 n2 (rn : nat_R n1 n2) :
+#[export] Instance RC_bdet n1 n2 (rn : nat_R n1 n2) :
   refines (RmxC (nat_R_S_R rn) (nat_R_S_R rn) ==> rC)
           (bdet (R:=R) (polyR:={poly R}) (mxR:=matrix R)
                 (mxpolyR:=matrix {poly R}) (@char_poly_mx R) head
@@ -361,7 +361,7 @@ Global Instance RC_bdet n1 n2 (rn : nat_R n1 n2) :
                 char_poly_mxC headC (n:=n2)).
 Proof. param bdet_R. Qed.
 
-Global Instance refine_bdet n :
+#[export] Instance refine_bdet n :
   refines (RmxC (nat_R_S_R (nat_Rxx n)) (nat_R_S_R (nat_Rxx n)) ==> rC)
           (bdet (R:=R) (polyR:={poly R}) (mxR:=matrix R)
                 (mxpolyR:=matrix {poly R}) (@char_poly_mx R) head
@@ -370,7 +370,7 @@ Global Instance refine_bdet n :
                 char_poly_mxC headC (n:=n)).
 Proof. exact: RC_bdet. Qed.
 
-Global Instance RC_det_bdet n1 n2 (rn : nat_R n1 n2) :
+#[export] Instance RC_det_bdet n1 n2 (rn : nat_R n1 n2) :
   refines (RmxC (nat_R_S_R rn) (nat_R_S_R rn) ==> rC) determinant
           (bdet (R:=C) (polyR:=polyC) (mxpolyR:=mxpolyC) char_poly_mxC headC
                 (n:=n2)).
@@ -380,7 +380,7 @@ Proof.
   exact: refinesP.
 Qed.
 
-Global Instance refine_det n :
+#[export] Instance refine_det n :
   refines (RmxC (nat_R_S_R (nat_Rxx n)) (nat_R_S_R (nat_Rxx n)) ==> rC)
           determinant (bdet (R:=C) (polyR:=polyC) (mxpolyR:=mxpolyC)
                             char_poly_mxC headC (n:=n)).
@@ -393,7 +393,7 @@ End bareiss_param.
 End bareiss_correctness.
 
 From mathcomp Require Import ssrint.
-From CoqEAL Require Import binint seqpoly poly_div binord.
+From CoqEAL Require Import binnat binint seqpoly poly_div binord trivial_seq.
 
 Section test_bareiss.
 

diff --git a/refinements/binint.v b/refinements/binint.v
@@ -45,10 +45,10 @@ Context `{cast_of N P, cast_of P N}.
 Context `{spec_of N nat, spec_of P pos}.
 Context `{implem_of nat N, implem_of pos P}.
 
-Global Instance zeroZ : zero_of Z := Zpos 0.
-Global Instance oneZ : one_of Z := Zpos 1.
+#[export] Instance zeroZ : zero_of Z := Zpos 0.
+#[export] Instance oneZ : one_of Z := Zpos 1.
 
-Global Instance addZ : add_of Z := fun x y : Z => match x, y with
+#[export] Instance addZ : add_of Z := fun x y : Z => match x, y with
   | Zpos x, Zpos y => Zpos (x + y)
   | Zneg x, Zneg y => Zneg (x + y)
   | Zpos x, Zneg y => if (cast y <= x) then Zpos (x - cast y)
@@ -57,12 +57,12 @@ Global Instance addZ : add_of Z := fun x y : Z => match x, y with
                                        else Zneg (cast (cast x - y))
   end.
 
-Global Instance oppZ : opp_of Z := fun x : Z => match x with
+#[export] Instance oppZ : opp_of Z := fun x : Z => match x with
   | Zpos x => if (x == 0)%C then 0%C else Zneg (cast x)
   | Zneg x => Zpos (cast x)
   end.
 
-Global Instance subZ : sub_of Z := fun x y : Z => match x, y with
+#[export] Instance subZ : sub_of Z := fun x y : Z => match x, y with
   | Zpos x, Zneg y => Zpos (x + cast y)
   | Zneg x, Zpos y => if (y == 0)%C then Zneg x else Zneg (x + cast y)
   | Zpos x, Zpos y => if (y <= x) then Zpos (x - y)
@@ -72,57 +72,57 @@ Global Instance subZ : sub_of Z := fun x y : Z => match x, y with
                       else Zneg (cast ((cast x : N) - cast y))
   end.
 
-Global Instance eqZ : eq_of Z := fun x y : Z => match x, y with
+#[export] Instance eqZ : eq_of Z := fun x y : Z => match x, y with
   | Zpos x, Zpos y => (x == y)
   | Zneg x, Zneg y => (x == y)
   | _, _ => false
   end.
 
-Global Instance mulZ : mul_of Z := fun x y : Z => match x, y with
+#[export] Instance mulZ : mul_of Z := fun x y : Z => match x, y with
   | Zpos x, Zpos y => Zpos (x * y)
   | Zneg x, Zpos y => if (y == 0)%C then 0%C else Zneg (x * cast y)
   | Zpos x, Zneg y => if (x == 0)%C then 0%C else Zneg (cast x * y)
   | Zneg x, Zneg y => Zpos (cast x * cast y)
   end.
 
-Global Instance expZ : exp_of Z N := fun x n =>
+#[export] Instance expZ : exp_of Z N := fun x n =>
   if (n == 0)%C then 1%C else
     match x with
     | Zpos x => Zpos (x ^ n)
     | Zneg x => if (n %% (1 + 1) == 0)%C then Zpos (cast (x ^ (cast n : P)))
                 else Zneg (x ^ (cast n : P))
     end.
 
-Global Instance leqZ : leq_of Z := fun x y : Z => match x, y with
+#[export] Instance leqZ : leq_of Z := fun x y : Z => match x, y with
   | Zpos x, Zpos y => (x <= y)
   | Zneg x, Zneg y => (y <= x)
   | Zneg _, Zpos _ => true
   | Zpos _, Zneg _ => false
   end.
 
-Global Instance ltZ : lt_of Z := fun x y : Z => match x, y with
+#[export] Instance ltZ : lt_of Z := fun x y : Z => match x, y with
   | Zpos x, Zpos y => (x < y)
   | Zneg x, Zneg y => (y < x)
   | Zneg _, Zpos _ => true
   | Zpos _, Zneg _ => false
   end.
 
-Global Instance cast_NZ : cast_of N Z := fun n : N => Zpos n.
+#[export] Instance cast_NZ : cast_of N Z := fun n : N => Zpos n.
 
-Global Instance cast_PZ : cast_of P Z := fun n : P => Zpos (cast n).
+#[export] Instance cast_PZ : cast_of P Z := fun n : P => Zpos (cast n).
 
-Global Instance cast_ZN : cast_of Z N := fun z =>
+#[export] Instance cast_ZN : cast_of Z N := fun z =>
   if z is Zpos n then n else 0.
 
-Global Instance cast_ZP : cast_of Z P := fun z => cast (cast_ZN z).
+#[export] Instance cast_ZP : cast_of Z P := fun z => cast (cast_ZN z).
 
-Global Instance specZ : spec_of Z int :=
+#[export] Instance specZ : spec_of Z int :=
   fun x => (match x with
              | Zpos p => (spec p : nat)%:Z
              | Zneg n => - (spec (cast n : N): nat)%:Z
            end)%R.
 
-Global Instance implemZ : implem_of int Z :=
+#[export] Instance implemZ : implem_of int Z :=
   fun x => (match x with
             | Posz n => Zpos (implem n)
             | Negz n => Zneg (implem (posS n))
@@ -388,57 +388,57 @@ Context `{!refines (Logic.eq ==> Rnat) implem_id implem,
 
 Local Notation Z := (Z N P).
 
-Global Instance RZNP_zeroZ  : refines RZNP 0 0%C.
+#[export] Instance RZNP_zeroZ  : refines RZNP 0 0%C.
 Proof. param_comp zeroZ_R. Qed.
 
-Global Instance RZNP_oneZ  : refines RZNP 1 1%C.
+#[export] Instance RZNP_oneZ  : refines RZNP 1 1%C.
 Proof. param_comp oneZ_R. Qed.
 
-Global Instance RZNP_castNZ : refines (Rnat ==> RZNP) Posz cast.
+#[export] Instance RZNP_castNZ : refines (Rnat ==> RZNP) Posz cast.
 Proof. param_comp cast_NZ_R. Qed.
 
-Global Instance RZNP_castPZ : refines (Rpos ==> RZNP) pos_to_int cast.
+#[export] Instance RZNP_castPZ : refines (Rpos ==> RZNP) pos_to_int cast.
 Proof. param_comp cast_PZ_R. Qed.
 
-Global Instance RZNP_castZN: refines (RZNP ==> Rnat) int_to_nat cast.
+#[export] Instance RZNP_castZN: refines (RZNP ==> Rnat) int_to_nat cast.
 Proof. rewrite /cast; param_comp cast_ZN_R. Qed.
 
-Global Instance RZNP_castZP: refines (RZNP ==> Rpos) int_to_pos cast.
+#[export] Instance RZNP_castZP: refines (RZNP ==> Rpos) int_to_pos cast.
 Proof. rewrite /cast; param_comp cast_ZP_R. Qed.
 
-Global Instance RZNP_addZ : refines (RZNP ==> RZNP ==> RZNP) +%R +%C.
+#[export] Instance RZNP_addZ : refines (RZNP ==> RZNP ==> RZNP) +%R +%C.
 Proof. param_comp addZ_R. Qed.
 
-Global Instance RZNP_mulZ : refines (RZNP ==> RZNP ==> RZNP) *%R *%C.
+#[export] Instance RZNP_mulZ : refines (RZNP ==> RZNP ==> RZNP) *%R *%C.
 Proof. param_comp mulZ_R. Qed.
 
-Global Instance RZNP_oppZ : refines (RZNP ==> RZNP) -%R -%C.
+#[export] Instance RZNP_oppZ : refines (RZNP ==> RZNP) -%R -%C.
 Proof. param_comp oppZ_R. Qed.
 
-Global Instance RZNP_subZ :
+#[export] Instance RZNP_subZ :
   refines (RZNP ==> RZNP ==> RZNP) (fun x y => x - y) sub_op.
 Proof. param_comp subZ_R. Qed.
 
-Global Instance RZNP_expZ :
+#[export] Instance RZNP_expZ :
   refines (RZNP ==> Rnat ==> RZNP) (@GRing.exp _) exp_op.
 Proof. param_comp expZ_R. Qed.
 
-Global Instance RZNP_eqZ :
+#[export] Instance RZNP_eqZ :
   refines (RZNP ==> RZNP ==> bool_R) eqtype.eq_op (@Op.eq_op Z _).
 Proof. param_comp eqZ_R. Qed.
 
-Global Instance RZNP_leqZ :
+#[export] Instance RZNP_leqZ :
   refines (RZNP ==> RZNP ==> bool_R) Num.le (@Op.leq_op Z _).
 Proof. param_comp leqZ_R. Qed.
 
-Global Instance RZNP_ltZ :
+#[export] Instance RZNP_ltZ :
   refines (RZNP ==> RZNP ==> bool_R) Num.lt (@Op.lt_op Z _).
 Proof. param_comp ltZ_R. Qed.
 
-(* Global Instance RZNP_specZ_l : refines (RZNP ==> int_R) spec_id spec. *)
+(* #[export] Instance RZNP_specZ_l : refines (RZNP ==> int_R) spec_id spec. *)
 (* Proof. param_comp specZ_R. Qed. *)
 
-Global Instance RZNP_specZ : refines (RZNP ==> Logic.eq) spec_id spec.
+#[export] Instance RZNP_specZ : refines (RZNP ==> Logic.eq) spec_id spec.
 Proof.
   eapply refines_trans; tc.
   rewrite refinesE=> x y rxy.
@@ -447,7 +447,7 @@ Proof.
   apply: congr1; exact: refinesP.
 Qed.
 
-Global Instance RZNP_implemZ : refines (Logic.eq ==> RZNP) implem_id implem.
+#[export] Instance RZNP_implemZ : refines (Logic.eq ==> RZNP) implem_id implem.
 Proof.
   eapply refines_trans; tc.
   rewrite refinesE=> _ x ->.