From 25934cf7c785367062b1894f296ab780ce6919ce Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 13 Mar 2023 10:17:06 +0100 Subject: [PATCH 1/2] [CI] Test Coq 8.17 and MC 1.16.0 This drops support for Coq 8.13 and 8.14. --- .github/workflows/docker-action.yml | 11 ++---- _CoqProject | 6 ++- coq-coqeal.opam | 4 +- refinements/binnat.v | 4 +- refinements/examples/irred.v | 2 +- refinements/multipoly.v | 2 +- refinements/param.v | 2 +- refinements/poly_op.v | 10 ++--- refinements/refinements.v | 61 +++++++++++++++-------------- refinements/seqmx.v | 1 + refinements/seqmx_complements.v | 4 +- refinements/seqpoly.v | 4 +- theory/coherent.v | 2 +- theory/dvdring.v | 2 +- theory/fpmod.v | 10 ++--- theory/stronglydiscrete.v | 2 +- 16 files changed, 64 insertions(+), 63 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index a6f77b1..70a5d71 100644 --- 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 index 5f69d62..f42c0be 100644 --- 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 index cf50a66..82d1d5c 100644 --- 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/binnat.v b/refinements/binnat.v index 0bd865b..ffa8034 100644 --- a/refinements/binnat.v +++ b/refinements/binnat.v @@ -179,7 +179,7 @@ Qed. End positive_theory. -Typeclasses Opaque pos_of_positive positive_of_pos. +#[export] Typeclasses Opaque pos_of_positive positive_of_pos. Global Opaque pos_of_positive positive_of_pos. Section binnat_op. @@ -438,7 +438,7 @@ Qed. End binnat_theory. -Typeclasses Opaque nat_of_bin bin_of_nat. +#[export] Typeclasses Opaque nat_of_bin bin_of_nat. Global Opaque nat_of_bin bin_of_nat. Section test. diff --git a/refinements/examples/irred.v b/refinements/examples/irred.v index d75be0b..806f56d 100644 --- a/refinements/examples/irred.v +++ b/refinements/examples/irred.v @@ -80,7 +80,7 @@ Lemma big_coef_npoly (p : {poly_n R}) i : n <= i -> p`_i = 0. Proof. by move=> i_big; rewrite nth_default // (leq_trans _ i_big). Qed. End npoly_theory. -Hint Resolve size_npoly npoly_inj : core. +#[export] Hint Resolve size_npoly npoly_inj : core. Section fin_npoly. diff --git a/refinements/multipoly.v b/refinements/multipoly.v index 8ba3685..5631cdb 100644 --- a/refinements/multipoly.v +++ b/refinements/multipoly.v @@ -30,7 +30,7 @@ Local Open Scope ring_scope. (** BEGIN FIXME this is redundant with PR CoqEAL/CoqEAL#3 *) Arguments refines A%type B%type R%rel _ _. (* Fix a scope issue with refines *) -Hint Resolve list_R_nil_R : core. +#[export] Hint Resolve list_R_nil_R : core. (** END FIXME this is redundant with PR CoqEAL/CoqEAL#3 *) (** Tip to leverage a Boolean condition *) diff --git a/refinements/param.v b/refinements/param.v index 16582de..63bbfd8 100644 --- a/refinements/param.v +++ b/refinements/param.v @@ -27,7 +27,7 @@ Require Import ProofIrrelevance. (* for opaque terms *) Parametricity option. Parametricity unit. Parametricity bool. -Hint Resolve bool_R_true_R bool_R_false_R : core. +#[export] Hint Resolve bool_R_true_R bool_R_false_R : core. Parametricity nat. Parametricity list. Parametricity prod. diff --git a/refinements/poly_op.v b/refinements/poly_op.v index 9995d4e..f854c80 100644 --- a/refinements/poly_op.v +++ b/refinements/poly_op.v @@ -12,20 +12,20 @@ Module Poly. Module Op. Class shift_of polyA N := shift_op : N -> polyA -> polyA. -Hint Mode shift_of + + : typeclass_instances. +#[export] Hint Mode shift_of + + : typeclass_instances. Class split_of polyA N := split_op : N -> polyA -> polyA * polyA. -Hint Mode split_of + + : typeclass_instances. +#[export] Hint Mode split_of + + : typeclass_instances. Class lead_coef_of A polyA := lead_coef_op : polyA -> A. -Hint Mode lead_coef_of + + : typeclass_instances. +#[export] Hint Mode lead_coef_of + + : typeclass_instances. Class scal_of polyA N := scal_op : polyA -> polyA -> N. -Hint Mode scal_of + + : typeclass_instances. +#[export] Hint Mode scal_of + + : typeclass_instances. End Op. End Poly. Import Poly.Op. -Typeclasses Transparent shift_of split_of lead_coef_of scal_of. +#[export] Typeclasses Transparent shift_of split_of lead_coef_of scal_of. Section poly_op. diff --git a/refinements/refinements.v b/refinements/refinements.v index f8bb466..4245307 100644 --- a/refinements/refinements.v +++ b/refinements/refinements.v @@ -207,12 +207,12 @@ End refinements. Arguments refinesP {T T' R x y} _. -Hint Mode refines - - - + - : typeclass_instances. +#[export] Hint Mode refines - - - + - : typeclass_instances. -Hint Extern 0 (refines _ _ _) +#[export] Hint Extern 0 (refines _ _ _) => apply trivial_refines; eassumption : typeclass_instances. -Hint Extern 0 (refines (_ \o (@unify _))%rel _ _) +#[export] Hint Extern 0 (refines (_ \o (@unify _))%rel _ _) => eapply refines_trans : typeclass_instances. (* Tactic for doing parametricity proofs, it takes a parametricity @@ -262,51 +262,52 @@ Module Refinements. Module Op. Class zero_of A := zero_op : A. -Hint Mode zero_of + : typeclass_instances. +#[export] Hint Mode zero_of + : typeclass_instances. Class one_of A := one_op : A. -Hint Mode one_of + : typeclass_instances. +#[export] Hint Mode one_of + : typeclass_instances. Class opp_of A := opp_op : A -> A. -Hint Mode opp_of + : typeclass_instances. +#[export] Hint Mode opp_of + : typeclass_instances. Class add_of A := add_op : A -> A -> A. -Hint Mode add_of + : typeclass_instances. +#[export] Hint Mode add_of + : typeclass_instances. Class sub_of A := sub_op : A -> A -> A. -Hint Mode sub_of + : typeclass_instances. +#[export] Hint Mode sub_of + : typeclass_instances. Class mul_of A := mul_op : A -> A -> A. -Hint Mode mul_of + : typeclass_instances. +#[export] Hint Mode mul_of + : typeclass_instances. Class exp_of A B := exp_op : A -> B -> A. -Hint Mode exp_of + + : typeclass_instances. +#[export] Hint Mode exp_of + + : typeclass_instances. Class div_of A := div_op : A -> A -> A. -Hint Mode div_of + : typeclass_instances. +#[export] Hint Mode div_of + : typeclass_instances. Class inv_of A := inv_op : A -> A. -Hint Mode inv_of + : typeclass_instances. +#[export] Hint Mode inv_of + : typeclass_instances. Class mod_of A := mod_op : A -> A -> A. -Hint Mode mod_of + : typeclass_instances. +#[export] Hint Mode mod_of + : typeclass_instances. Class scale_of A B := scale_op : A -> B -> B. -Hint Mode scale_of + + : typeclass_instances. +#[export] Hint Mode scale_of + + : typeclass_instances. Class eq_of A := eq_op : A -> A -> bool. -Hint Mode eq_of + : typeclass_instances. +#[export] Hint Mode eq_of + : typeclass_instances. Class leq_of A := leq_op : A -> A -> bool. -Hint Mode leq_of + : typeclass_instances. +#[export] Hint Mode leq_of + : typeclass_instances. Class lt_of A := lt_op : A -> A -> bool. -Hint Mode lt_of + : typeclass_instances. +#[export] Hint Mode lt_of + : typeclass_instances. Class size_of A N := size_op : A -> N. -Hint Mode size_of + + : typeclass_instances. +#[export] Hint Mode size_of + + : typeclass_instances. Class spec_of A B := spec : A -> B. -Hint Mode spec_of + + : typeclass_instances. +#[export] Hint Mode spec_of + + : typeclass_instances. Definition spec_id {A : Type} : spec_of A A := id. Class implem_of A B := implem : A -> B. -Hint Mode implem_of + + : typeclass_instances. +#[export] Hint Mode implem_of + + : typeclass_instances. Definition implem_id {A : Type} : implem_of A A := id. Class cast_of A B := cast_op : A -> B. -Hint Mode cast_of + + : typeclass_instances. +#[export] Hint Mode cast_of + + : typeclass_instances. End Op. End Refinements. Import Refinements.Op. +#[export] Typeclasses Transparent zero_of one_of opp_of add_of sub_of mul_of exp_of div_of inv_of mod_of scale_of size_of eq_of leq_of lt_of spec_of implem_of cast_of. @@ -369,34 +370,34 @@ Tactic Notation "context" "[" ssrpatternarg(pat) "]" tactic3(tac) := Class strategy_class (C : forall T, T -> T -> Prop) := StrategyClass : C = @eq. -Hint Mode strategy_class + : typeclass_instances. +#[export] Hint Mode strategy_class + : typeclass_instances. Class native_compute T (x y : T) := NativeCompute : x = y. -Hint Mode native_compute - + - : typeclass_instances. -Hint Extern 0 (native_compute _ _) => +#[export] Hint Mode native_compute - + - : typeclass_instances. +#[export] Hint Extern 0 (native_compute _ _) => context [(X in native_compute X)] native_compute; reflexivity : typeclass_instances. #[global] Instance strategy_class_native_compute : strategy_class native_compute := erefl. Class vm_compute T (x y : T) := VmCompute : x = y. -Hint Mode vm_compute - + - : typeclass_instances. -Hint Extern 0 (vm_compute _ _) => +#[export] Hint Mode vm_compute - + - : typeclass_instances. +#[export] Hint Extern 0 (vm_compute _ _) => context [(X in vm_compute X)] vm_compute; reflexivity : typeclass_instances. #[global] Instance strategy_class_vm_compute : strategy_class vm_compute := erefl. Class compute T (x y : T) := Compute : x = y. -Hint Mode compute - + - : typeclass_instances. -Hint Extern 0 (compute _ _) => +#[export] Hint Mode compute - + - : typeclass_instances. +#[export] Hint Extern 0 (compute _ _) => context [(X in compute X)] compute; reflexivity : typeclass_instances. #[global] Instance strategy_class_compute : strategy_class compute := erefl. Class simpl T (x y : T) := Simpl : x = y. -Hint Mode simpl - + - : typeclass_instances. -Hint Extern 0 (simpl _ _) => +#[export] Hint Mode simpl - + - : typeclass_instances. +#[export] Hint Extern 0 (simpl _ _) => context [(X in simpl X)] simpl; reflexivity : typeclass_instances. #[global] Instance strategy_class_simpl : strategy_class simpl := erefl. diff --git a/refinements/seqmx.v b/refinements/seqmx.v index c78ef72..8df945e 100644 --- a/refinements/seqmx.v +++ b/refinements/seqmx.v @@ -66,6 +66,7 @@ Class map_mx_of A B C D := End classes. +#[export] Typeclasses Transparent hzero_of hmul_of heq_of top_left_of usubmx_of dsubmx_of lsubmx_of rsubmx_of ulsubmx_of ursubmx_of dlsubmx_of drsubmx_of row_mx_of col_mx_of block_mx_of const_mx_of map_mx_of. diff --git a/refinements/seqmx_complements.v b/refinements/seqmx_complements.v index f521cb2..a8f9d3e 100644 --- a/refinements/seqmx_complements.v +++ b/refinements/seqmx_complements.v @@ -19,7 +19,7 @@ Arguments refines A%type B%type R%rel _ _. (* Fix a scope issue with refines *) Arguments refinesP {T T' R x y} _. -Hint Resolve list_R_nil_R : core. +#[export] Hint Resolve list_R_nil_R : core. Notation ord_instN := (fun _ : nat => nat) (only parsing). @@ -43,7 +43,7 @@ Class trmx_of B := trmx_op : forall m n : nat, B m n -> B n m. End classes. -Typeclasses Transparent fun_of_of row_of store_of trmx_of. +#[export] Typeclasses Transparent fun_of_of row_of store_of trmx_of. Notation "A ^T" := (trmx_op A) : hetero_computable_scope. diff --git a/refinements/seqpoly.v b/refinements/seqpoly.v index eea0eb8..835057a 100644 --- a/refinements/seqpoly.v +++ b/refinements/seqpoly.v @@ -650,8 +650,8 @@ End seqpoly_theory. (* Always simpl Poly. Maybe have refinement instance instead? Is this *) (* more efficient? *) -Hint Extern 0 (refines _ (Poly _) _) => simpl : typeclass_instances. -Hint Extern 0 (refines _ _ (Poly _)) => simpl : typeclass_instances. +#[export] Hint Extern 0 (refines _ (Poly _) _) => simpl : typeclass_instances. +#[export] Hint Extern 0 (refines _ _ (Poly _)) => simpl : typeclass_instances. From mathcomp Require Import ssrint. From CoqEAL Require Import binnat binint. diff --git a/theory/coherent.v b/theory/coherent.v index 5861343..c1ae36c 100644 --- a/theory/coherent.v +++ b/theory/coherent.v @@ -315,7 +315,7 @@ Notation "M .-ker" := (ker_mod M) (at level 10, format "M .-ker") : mxpresentation_scope. Notation "M %| B" := (dvdmx M B) : mxpresentation_scope. -Hint Resolve dvdmx_refl dvdmx0 dvd1mx : core. +#[export] Hint Resolve dvdmx_refl dvdmx0 dvd1mx : core. (* It suffices to show how to solve xM = 0 when M is a column for the ring to diff --git a/theory/dvdring.v b/theory/dvdring.v index 6cdad3d..a7a47ae 100644 --- a/theory/dvdring.v +++ b/theory/dvdring.v @@ -629,7 +629,7 @@ Qed. End DvdRingTheory. -Hint Resolve dvdrr dvd1r eqdd : core. +#[export] Hint Resolve dvdrr dvd1r eqdd : core. (* Notation "x *d y" := (mulqr x y) *) (* (at level 40, left associativity, format "x *d y"). *) diff --git a/theory/fpmod.v b/theory/fpmod.v index 81d7e3e..1097f02 100644 --- a/theory/fpmod.v +++ b/theory/fpmod.v @@ -255,7 +255,7 @@ End morphismTheory. Arguments idm {_ _}. Infix "**" := mulmor. Infix "%=" := eqmor. -Hint Resolve eqmorxx : core. +#[export] Hint Resolve eqmorxx : core. Section KernelAndCo. Variable R : coherentRingType. @@ -504,8 +504,8 @@ Qed. End MonoTheory. -Hint Resolve kernel_eq0 : core. -Hint Resolve mono : core. +#[export] Hint Resolve kernel_eq0 : core. +#[export] Hint Resolve mono : core. Section EpiTheory. Variable (R : coherentRingType). @@ -536,8 +536,8 @@ Qed. End EpiTheory. -Hint Resolve coker_eq0 : core. -Hint Resolve epi : core. +#[export] Hint Resolve coker_eq0 : core. +#[export] Hint Resolve epi : core. Section IsoTheory. Variable (R : coherentRingType) (M N : {fpmod R}). diff --git a/theory/stronglydiscrete.v b/theory/stronglydiscrete.v index 32c4b84..981cdb4 100644 --- a/theory/stronglydiscrete.v +++ b/theory/stronglydiscrete.v @@ -704,4 +704,4 @@ Canonical Structure bezout_stronglyDiscreteType := Eval hnf in StronglyDiscreteType R bezout_stronglyDiscreteMixin. End BezoutStronglyDiscrete. -Hint Resolve subid_refl sub0id subid1 : core. +#[export] Hint Resolve subid_refl sub0id subid1 : core. From 9172275e03a3874ff59b8721d9de11b8927793a9 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 13 Mar 2023 11:23:38 +0100 Subject: [PATCH 2/2] Replace global attributes with export --- refinements/bareiss_eff.v | 22 ++-- refinements/binint.v | 66 ++++++------ refinements/binnat.v | 118 ++++++++++---------- refinements/binord.v | 44 ++++---- refinements/binrat.v | 64 +++++------ refinements/boolF2.v | 32 +++--- refinements/examples/irred.v | 36 +++---- refinements/hpoly.v | 84 +++++++-------- refinements/karatsuba.v | 6 +- refinements/multipoly.v | 58 +++++----- refinements/param.v | 4 +- refinements/poly_div.v | 18 ++-- refinements/pos.v | 20 ++-- refinements/rational.v | 60 +++++------ refinements/refinements.v | 58 +++++----- refinements/seqmx.v | 184 ++++++++++++++++---------------- refinements/seqmx_complements.v | 30 +++--- refinements/seqpoly.v | 86 +++++++-------- refinements/trivial_seq.v | 10 +- theory/ssralg_ring_tac.v | 8 +- 20 files changed, 504 insertions(+), 504 deletions(-) diff --git a/refinements/bareiss_eff.v b/refinements/bareiss_eff.v index fb7d14f..3c00782 100644 --- 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 index 5eb8829..d60dfd5 100644 --- 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,20 +72,20 @@ 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) @@ -93,36 +93,36 @@ Global Instance expZ : exp_of Z N := fun x n => 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 ->. diff --git a/refinements/binnat.v b/refinements/binnat.v index ffa8034..8b1066a 100644 --- a/refinements/binnat.v +++ b/refinements/binnat.v @@ -27,16 +27,16 @@ Section positive_op. Definition positive_of_pos (p : pos) : positive := Pos.of_nat (val p). Definition pos_of_positive (p : positive) : pos := insubd pos1 (Pos.to_nat p). -Global Instance spec_positive : spec_of positive pos := pos_of_positive. -Global Instance implem_positive : implem_of pos positive := positive_of_pos. -Global Instance one_positive : one_of positive := xH. -Global Instance add_positive : add_of positive := Pos.add. -Global Instance sub_positive : sub_of positive := Pos.sub. -Global Instance mul_positive : mul_of positive := Pos.mul. -Global Instance le_positive : leq_of positive := Pos.leb. -Global Instance lt_positive : lt_of positive := Pos.ltb. -Global Instance eq_positive : eq_of positive := Pos.eqb. -Global Instance exp_positive : exp_of positive positive := Pos.pow. +#[export] Instance spec_positive : spec_of positive pos := pos_of_positive. +#[export] Instance implem_positive : implem_of pos positive := positive_of_pos. +#[export] Instance one_positive : one_of positive := xH. +#[export] Instance add_positive : add_of positive := Pos.add. +#[export] Instance sub_positive : sub_of positive := Pos.sub. +#[export] Instance mul_positive : mul_of positive := Pos.mul. +#[export] Instance le_positive : leq_of positive := Pos.leb. +#[export] Instance lt_positive : lt_of positive := Pos.ltb. +#[export] Instance eq_positive : eq_of positive := Pos.eqb. +#[export] Instance exp_positive : exp_of positive positive := Pos.pow. End positive_op. Section positive_theory. @@ -79,10 +79,10 @@ Lemma RposI (p : pos) (x : positive) : refines Rpos p x -> x = positive_of_pos p. Proof. by move=> /RposE ->; rewrite pos_of_positiveK. Qed. -Global Instance Rpos_spec_pos_r x : refines Rpos (spec x) x. +#[export] Instance Rpos_spec_pos_r x : refines Rpos (spec x) x. Proof. by rewrite !refinesE. Qed. -(* Global Instance Rpos_spec_pos_l : refines (Rpos ==> pos_R) spec_id spec. *) +(* #[export] Instance Rpos_spec_pos_l : refines (Rpos ==> pos_R) spec_id spec. *) (* Proof. *) (* rewrite refinesE=> x x'. *) (* rewrite -[Rpos]refinesE=> rx. *) @@ -90,34 +90,34 @@ Proof. by rewrite !refinesE. Qed. (* exact: pos_Rxx. *) (* Qed. *) -Global Instance Rpos_spec : refines (Rpos ==> Logic.eq) spec_id spec. +#[export] Instance Rpos_spec : refines (Rpos ==> Logic.eq) spec_id spec. Proof. by rewrite refinesE. Qed. -Global Instance Rpos_implem : refines (Logic.eq ==> Rpos) implem_id implem. +#[export] Instance Rpos_implem : refines (Logic.eq ==> Rpos) implem_id implem. Proof. rewrite refinesE=> _ x ->. case: x=> n ngt0. by rewrite /Rpos /fun_hrel positive_of_posK. Qed. -Global Instance Rpos_1 : refines Rpos (pos1 : pos) (1%C : positive). +#[export] Instance Rpos_1 : refines Rpos (pos1 : pos) (1%C : positive). Proof. by rewrite !refinesE; apply: val_inj; rewrite /= insubdK. Qed. -Global Instance Rpos_add : refines (Rpos ==> Rpos ==> Rpos) add_pos +%C. +#[export] Instance Rpos_add : refines (Rpos ==> Rpos ==> Rpos) add_pos +%C. Proof. rewrite refinesE => _ x <- _ y <-; apply: val_inj. rewrite !val_insubd Pos2Nat.inj_add. by move: (Pos2Nat.is_pos x) (Pos2Nat.is_pos y) => /leP -> /leP ->. Qed. -Global Instance Rpos_mul : refines (Rpos ==> Rpos ==> Rpos) mul_pos *%C. +#[export] Instance Rpos_mul : refines (Rpos ==> Rpos ==> Rpos) mul_pos *%C. Proof. rewrite refinesE => _ x <- _ y <-; apply: val_inj. rewrite !val_insubd Pos2Nat.inj_mul. by move: (Pos2Nat.is_pos x) (Pos2Nat.is_pos y) => /leP -> /leP ->. Qed. -Global Instance Rpos_sub : refines (Rpos ==> Rpos ==> Rpos) sub_pos sub_op. +#[export] Instance Rpos_sub : refines (Rpos ==> Rpos ==> Rpos) sub_pos sub_op. Proof. rewrite refinesE => _ x <- _ y <-; apply: val_inj; rewrite !val_insubd. move: (Pos2Nat.is_pos x) (Pos2Nat.is_pos y) => /leP -> /leP ->. @@ -127,7 +127,7 @@ rewrite /sub_op /sub_positive Pos.sub_le ?Pos2Nat.inj_le //. by rewrite subn_gt0 !ltnNge; move/leP: h ->. Qed. -Global Instance Rpos_leq : refines (Rpos ==> Rpos ==> bool_R) leq_pos leq_op. +#[export] Instance Rpos_leq : refines (Rpos ==> Rpos ==> bool_R) leq_pos leq_op. Proof. rewrite refinesE=> _ x <- _ y <-; rewrite /leq_op /le_positive /leq_pos !val_insubd. @@ -136,7 +136,7 @@ Proof. [move ->|rewrite -eqbF_neg; move/eqP ->]. Qed. -Global Instance Rpos_lt : refines (Rpos ==> Rpos ==> bool_R) lt_pos lt_op. +#[export] Instance Rpos_lt : refines (Rpos ==> Rpos ==> bool_R) lt_pos lt_op. Proof. rewrite refinesE => /= _ x <- _ y <-; rewrite /lt_pos !val_insubd. move: (Pos2Nat.is_pos x) (Pos2Nat.is_pos y) => /leP -> /leP ->. @@ -145,7 +145,7 @@ have -> : (Pos.to_nat x < Pos.to_nat y) = (x < y)%C. exact: bool_Rxx. Qed. -Global Instance Rpos_eq : refines (Rpos ==> Rpos ==> bool_R) eq_pos eq_op. +#[export] Instance Rpos_eq : refines (Rpos ==> Rpos ==> bool_R) eq_pos eq_op. Proof. rewrite refinesE=> _ x <- _ y <-; rewrite /eq_op /eq_positive /eq_pos. case: (Pos.eqb_spec _ _)=> [->|h]. @@ -170,7 +170,7 @@ Proof. by rewrite Pos2Nat.inj_1 expn1 Pos.pow_1_r. Qed. -Global Instance Rpos_exp : refines (Rpos ==> Rpos ==> Rpos) exp_pos exp_op. +#[export] Instance Rpos_exp : refines (Rpos ==> Rpos ==> Rpos) exp_pos exp_op. Proof. rewrite refinesE /exp_op /exp_positive=> _ x <- _ y <-. apply: val_inj. @@ -180,31 +180,31 @@ Qed. End positive_theory. #[export] Typeclasses Opaque pos_of_positive positive_of_pos. -Global Opaque pos_of_positive positive_of_pos. +#[global] Opaque pos_of_positive positive_of_pos. Section binnat_op. -Global Instance zero_N : zero_of N := N.zero. -Global Instance one_N : one_of N := N.one. -Global Instance add_N : add_of N := N.add. +#[export] Instance zero_N : zero_of N := N.zero. +#[export] Instance one_N : one_of N := N.one. +#[export] Instance add_N : add_of N := N.add. Definition succN (n : N) : N := (1 + n)%C. -Global Instance sub_N : sub_of N := N.sub. -Global Instance exp_N : exp_of N N := N.pow. -Global Instance mul_N : mul_of N := N.mul. -Global Instance div_N : div_of N := N.div. -Global Instance mod_N : mod_of N := N.modulo. -Global Instance eq_N : eq_of N := N.eqb. -Global Instance leq_N : leq_of N := N.leb. -Global Instance lt_N : lt_of N := N.ltb. - -Global Instance cast_positive_N : cast_of positive N := Npos. -Global Instance cast_N_positive : cast_of N positive := +#[export] Instance sub_N : sub_of N := N.sub. +#[export] Instance exp_N : exp_of N N := N.pow. +#[export] Instance mul_N : mul_of N := N.mul. +#[export] Instance div_N : div_of N := N.div. +#[export] Instance mod_N : mod_of N := N.modulo. +#[export] Instance eq_N : eq_of N := N.eqb. +#[export] Instance leq_N : leq_of N := N.leb. +#[export] Instance lt_N : lt_of N := N.ltb. + +#[export] Instance cast_positive_N : cast_of positive N := Npos. +#[export] Instance cast_N_positive : cast_of N positive := fun n => if n is Npos p then p else 1%C. -Global Instance spec_N : spec_of N nat := nat_of_bin. -Global Instance implem_N : implem_of nat N := bin_of_nat. +#[export] Instance spec_N : spec_of N nat := nat_of_bin. +#[export] Instance implem_N : implem_of nat N := bin_of_nat. End binnat_op. @@ -217,37 +217,37 @@ Definition Rnat : nat -> N -> Type := fun_hrel nat_of_bin. Lemma RnatE (n : nat) (x : N) : refines Rnat n x -> n = x. Proof. by rewrite refinesE. Qed. -Global Instance Rnat_spec_r x : refines Rnat (spec x) x. +#[export] Instance Rnat_spec_r x : refines Rnat (spec x) x. Proof. by rewrite refinesE. Qed. -Global Instance Rnat_spec_l : refines (Rnat ==> nat_R) spec_id spec. +#[export] Instance Rnat_spec_l : refines (Rnat ==> nat_R) spec_id spec. Proof. rewrite refinesE=> x x' rx. rewrite [spec _]RnatE /spec_id [y in nat_R y _]RnatE. exact: nat_Rxx. Qed. -Global Instance Rnat_spec : refines (Rnat ==> Logic.eq) spec_id spec. +#[export] Instance Rnat_spec : refines (Rnat ==> Logic.eq) spec_id spec. Proof. by rewrite refinesE. Qed. -Global Instance Rnat_implem : refines (Logic.eq ==> Rnat) implem_id implem. +#[export] Instance Rnat_implem : refines (Logic.eq ==> Rnat) implem_id implem. Proof. rewrite !refinesE => x _ <-. by rewrite /Rnat /fun_hrel /implem /implem_N bin_of_natK. Qed. -Global Instance Rnat_0 : refines Rnat 0 0%C. +#[export] Instance Rnat_0 : refines Rnat 0 0%C. Proof. by rewrite refinesE. Qed. -Global Instance Rnat_1 : refines Rnat 1%nat 1%C. +#[export] Instance Rnat_1 : refines Rnat 1%nat 1%C. Proof. by rewrite refinesE. Qed. -Global Instance Rnat_add : refines (Rnat ==> Rnat ==> Rnat) addn +%C. +#[export] Instance Rnat_add : refines (Rnat ==> Rnat ==> Rnat) addn +%C. Proof. by rewrite refinesE => _ x <- _ y <-; rewrite /Rnat /fun_hrel nat_of_add_bin. Qed. -Global Instance Rnat_S : refines (Rnat ==> Rnat) S succN. +#[export] Instance Rnat_S : refines (Rnat ==> Rnat) S succN. Proof. by rewrite !refinesE => m n rmn; rewrite -add1n /succN; apply: refinesP. Qed. @@ -257,19 +257,19 @@ Proof. by case => //= p; apply: Nnat.N2Nat.inj; rewrite Nnat.Nat2N.id /= to_natE. Qed. -Global Instance Rnat_sub : refines (Rnat ==> Rnat ==> Rnat) subn sub_op. +#[export] Instance Rnat_sub : refines (Rnat ==> Rnat ==> Rnat) subn sub_op. Proof. rewrite refinesE => _ x <- _ y <-. by apply: Nnat.Nat2N.inj; rewrite Nnat.Nat2N.inj_sub !nat_of_binK. Qed. -Global Instance Rnat_mul : refines (Rnat ==> Rnat ==> Rnat) muln mul_op. +#[export] Instance Rnat_mul : refines (Rnat ==> Rnat ==> Rnat) muln mul_op. Proof. rewrite refinesE => _ x <- _ y <-; rewrite /Rnat /fun_hrel /=. by rewrite nat_of_mul_bin. Qed. -Global Instance Rnat_div_eucl : +#[export] Instance Rnat_div_eucl : refines (Rnat ==> Rnat ==> prod_R Rnat Rnat) edivn N.div_eucl. Proof. rewrite refinesE /Rnat /fun_hrel=> _ x <- _ y <-. @@ -292,19 +292,19 @@ Proof. by rewrite divn_small ?addn0 // ?to_natE. Qed. -Global Instance Rnat_div : refines (Rnat ==> Rnat ==> Rnat) divn div_op. +#[export] Instance Rnat_div : refines (Rnat ==> Rnat ==> Rnat) divn div_op. Proof. by apply refines_abstr2; rewrite /divn /div_op /div_N /N.div=> x x' rx y y' ry; tc. Qed. -Global Instance Rnat_mod : refines (Rnat ==> Rnat ==> Rnat) modn mod_op. +#[export] Instance Rnat_mod : refines (Rnat ==> Rnat ==> Rnat) modn mod_op. Proof. apply refines_abstr2; rewrite /mod_op /mod_N /N.modulo=> x x' rx y y' ry. rewrite modn_def. exact: refines_apply. Qed. -Global Instance Rnat_exp : refines (Rnat ==> Rnat ==> Rnat) expn exp_op. +#[export] Instance Rnat_exp : refines (Rnat ==> Rnat ==> Rnat) expn exp_op. Proof. rewrite refinesE => _ x <- _ y <-; rewrite /Rnat /fun_hrel /=. rewrite /exp_op /exp_N /N.pow. @@ -318,7 +318,7 @@ Proof. by rewrite !nat_of_binposE pos2nat_inj_exp. Qed. -Global Instance Rnat_eq : refines (Rnat ==> Rnat ==> bool_R) eqtype.eq_op eq_op. +#[export] Instance Rnat_eq : refines (Rnat ==> Rnat ==> bool_R) eqtype.eq_op eq_op. Proof. rewrite refinesE=> _ x <- _ y <-; rewrite /eq_op /eq_N. case: (N.eqb_spec _ _) => [->|/eqP hneq]. @@ -328,7 +328,7 @@ Proof. by apply/negP => [/eqP /(can_inj nat_of_binK)]; apply/eqP. Qed. -Global Instance Rnat_leq : refines (Rnat ==> Rnat ==> bool_R) ssrnat.leq leq_op. +#[export] Instance Rnat_leq : refines (Rnat ==> Rnat ==> bool_R) ssrnat.leq leq_op. Proof. rewrite refinesE=> _ x <- _ y <-; rewrite /leq_op /leq_N /leq. case: (N.leb_spec0 _ _)=> [/N.sub_0_le|]=> h. @@ -339,7 +339,7 @@ Proof. by move/(can_inj nat_of_binK)/N.sub_0_le. Qed. -Global Instance Rnat_lt : refines (Rnat ==> Rnat ==> bool_R) ltn lt_op. +#[export] Instance Rnat_lt : refines (Rnat ==> Rnat ==> bool_R) ltn lt_op. Proof. apply refines_abstr2 => x x' rx y y' ry; rewrite refinesE /Rnat /fun_hrel. rewrite /lt_op /lt_N N.ltb_antisym /ltn /= ltnNge [(y <= x)%N]refines_eq. @@ -347,14 +347,14 @@ exact: bool_Rxx. (* Cyril: this was wrong to do it like that, we should come back and fix *) Qed. -Global Instance Rnat_cast_positive_N : +#[export] Instance Rnat_cast_positive_N : refines (Rpos ==> Rnat) val (cast : positive -> N). Proof. rewrite refinesE /cast /Rnat /fun_hrel => x x' rx. by rewrite [x]RposE val_insubd to_nat_gt0 to_natE. Qed. -Global Instance Rnat_cast_N_positive : +#[export] Instance Rnat_cast_N_positive : refines (Rnat ==> Rpos) (insubd pos1) (cast : N -> positive). Proof. rewrite refinesE=> x x' rx; rewrite [x]RnatE. @@ -439,7 +439,7 @@ Qed. End binnat_theory. #[export] Typeclasses Opaque nat_of_bin bin_of_nat. -Global Opaque nat_of_bin bin_of_nat. +#[global] Opaque nat_of_bin bin_of_nat. Section test. diff --git a/refinements/binord.v b/refinements/binord.v index 045e481..17de32b 100644 --- a/refinements/binord.v +++ b/refinements/binord.v @@ -17,33 +17,33 @@ Section binord_op. Definition binord := fun (_ : nat) => N. -Global Instance zero_ord n : zero_of (binord n) := N.zero. +#[export] Instance zero_ord n : zero_of (binord n) := N.zero. -Global Instance one_ord n : one_of (binord n.+1) := +#[export] Instance one_ord n : one_of (binord n.+1) := if (n == 0)%N then N.zero else N.one. -Global Instance opp_ord n : opp_of (binord n) := +#[export] Instance opp_ord n : opp_of (binord n) := fun x => N.modulo ((implem n) - x) (implem n). -Global Instance add_ord n : add_of (binord n) := +#[export] Instance add_ord n : add_of (binord n) := fun x y => N.modulo (x + y) (implem n). -Global Instance sub_ord n : sub_of (binord n) := +#[export] Instance sub_ord n : sub_of (binord n) := fun x y => N.modulo (x + (N.modulo ((implem n) - y) (implem n))) (implem n). -Global Instance mul_ord n : mul_of (binord n) := +#[export] Instance mul_ord n : mul_of (binord n) := fun x y => N.modulo (x * y) (implem n). -Global Instance exp_ord n : exp_of (binord n) N := +#[export] Instance exp_ord n : exp_of (binord n) N := fun x y => N.modulo (x ^ y) (implem n). -Global Instance eq_ord n : eq_of (binord n) := N.eqb. +#[export] Instance eq_ord n : eq_of (binord n) := N.eqb. -Global Instance leq_ord n : leq_of (binord n) := N.leb. +#[export] Instance leq_ord n : leq_of (binord n) := N.leb. -Global Instance lt_ord n : lt_of (binord n) := N.ltb. +#[export] Instance lt_ord n : lt_of (binord n) := N.ltb. -Global Instance implem_ord n : implem_of 'I_n (binord n) := +#[export] Instance implem_ord n : implem_of 'I_n (binord n) := fun x => implem (x : nat). End binord_op. @@ -55,11 +55,11 @@ Local Open Scope rel_scope. Definition Rord n1 n2 (rn : nat_R n1 n2) : 'I_n1 -> binord n2 -> Type := fun x y => Rnat x y. -Global Instance Rord_0 n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rord_0 n1 n2 (rn : nat_R n1 n2) : refines (Rord (nat_R_S_R rn)) 0%R 0%C. Proof. by rewrite refinesE. Qed. -Global Instance Rord_1 n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rord_1 n1 n2 (rn : nat_R n1 n2) : refines (Rord (nat_R_S_R rn)) Zp1 1%C. Proof. rewrite refinesE /Rord /Zp1 /inZp /= modn_def (nat_R_eq rn). @@ -84,7 +84,7 @@ Local Arguments opp_op /. Local Arguments opp_ord /. Local Arguments N.sub : simpl nomatch. -Global Instance Rord_opp n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rord_opp n1 n2 (rn : nat_R n1 n2) : refines (Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn)) -%R -%C. Proof. rewrite refinesE=> x x' hx /=. @@ -94,7 +94,7 @@ Qed. Local Arguments add_op /. Local Arguments add_ord /. -Global Instance Rord_add n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rord_add n1 n2 (rn : nat_R n1 n2) : refines (Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn)) +%R +%C. Proof. @@ -105,7 +105,7 @@ Qed. Local Arguments sub_op /. Local Arguments sub_ord /. -Global Instance Rord_sub n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rord_sub n1 n2 (rn : nat_R n1 n2) : refines (Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn)) (fun x y => x - y) sub_op. Proof. @@ -116,7 +116,7 @@ Qed. Local Arguments mul_op /. Local Arguments mul_ord /. -Global Instance Rord_mul n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rord_mul n1 n2 (rn : nat_R n1 n2) : refines (Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn)) (@Zp_mul n1) *%C. Proof. @@ -127,7 +127,7 @@ Qed. Local Arguments eq_op /. Local Arguments eq_ord /. -Global Instance Rord_eq n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rord_eq n1 n2 (rn : nat_R n1 n2) : refines (Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn) ==> bool_R) eqtype.eq_op eq_op. Proof. @@ -139,7 +139,7 @@ Qed. Local Arguments leq_op /. Local Arguments leq_ord /. -Global Instance Rord_leq n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rord_leq n1 n2 (rn : nat_R n1 n2) : refines (Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn) ==> bool_R) (fun x y => (x <= y)%N) leq_op. Proof. @@ -151,7 +151,7 @@ Local Arguments lt_op /. Local Arguments lt_ord /. Local Opaque ltn. -Global Instance Rord_lt n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rord_lt n1 n2 (rn : nat_R n1 n2) : refines (Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn) ==> bool_R) (fun x y => ltn x y) lt_op. Proof. @@ -164,7 +164,7 @@ Local Arguments implem_id /. Local Arguments implem /. Local Arguments implem_ord /. -Global Instance Rord_implem n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rord_implem n1 n2 (rn : nat_R n1 n2) : refines (ordinal_R rn ==> Rord rn) implem_id implem. Proof. rewrite refinesE=> x y rxy /=. @@ -176,7 +176,7 @@ Proof. exact: refinesP. Qed. -Global Instance Rnat_nat_of_ord n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rnat_nat_of_ord n1 n2 (rn : nat_R n1 n2) : refines (Rord rn ==> Rnat) (@nat_of_ord n1) id. Proof. by rewrite refinesE. Qed. diff --git a/refinements/binrat.v b/refinements/binrat.v index 572768c..a31c97c 100644 --- a/refinements/binrat.v +++ b/refinements/binrat.v @@ -375,31 +375,31 @@ Definition r_ratBigQ := fun_hrel bigQ2rat. (** *** Main instances *) -Global Instance zero_bigQ : zero_of bigQ := 0%bigQ. -Global Instance one_bigQ : one_of bigQ := 1%bigQ. -Global Instance opp_bigQ : opp_of bigQ := BigQ.opp. -Global Instance add_bigQ : add_of bigQ := BigQ.add_norm. -Global Instance sub_bigQ : sub_of bigQ := BigQ.sub_norm. -Global Instance mul_bigQ : mul_of bigQ := BigQ.mul_norm. -Global Instance inv_bigQ : inv_of bigQ := BigQ.inv_norm. -Global Instance div_bigQ : div_of bigQ := BigQ.div_norm. -Global Instance eq_bigQ : eq_of bigQ := BigQ.eq_bool. -Global Instance lt_bigQ : lt_of bigQ := fun p q => if BigQ.compare p q is Lt then true else false. -Global Instance le_bigQ : leq_of bigQ := fun p q => if BigQ.compare q p is Lt then false else true. -Global Instance max_bigQ : max_of bigQ := BigQ.max. -Global Instance min_bigQ : min_of bigQ := BigQ.min. -Global Instance cast_of_nat_bigQ : cast_of nat bigQ := BigQ.of_Z \o Z.of_nat. -Global Instance spec_bigQ : spec_of bigQ rat := bigQ2rat. +#[export] Instance zero_bigQ : zero_of bigQ := 0%bigQ. +#[export] Instance one_bigQ : one_of bigQ := 1%bigQ. +#[export] Instance opp_bigQ : opp_of bigQ := BigQ.opp. +#[export] Instance add_bigQ : add_of bigQ := BigQ.add_norm. +#[export] Instance sub_bigQ : sub_of bigQ := BigQ.sub_norm. +#[export] Instance mul_bigQ : mul_of bigQ := BigQ.mul_norm. +#[export] Instance inv_bigQ : inv_of bigQ := BigQ.inv_norm. +#[export] Instance div_bigQ : div_of bigQ := BigQ.div_norm. +#[export] Instance eq_bigQ : eq_of bigQ := BigQ.eq_bool. +#[export] Instance lt_bigQ : lt_of bigQ := fun p q => if BigQ.compare p q is Lt then true else false. +#[export] Instance le_bigQ : leq_of bigQ := fun p q => if BigQ.compare q p is Lt then false else true. +#[export] Instance max_bigQ : max_of bigQ := BigQ.max. +#[export] Instance min_bigQ : min_of bigQ := BigQ.min. +#[export] Instance cast_of_nat_bigQ : cast_of nat bigQ := BigQ.of_Z \o Z.of_nat. +#[export] Instance spec_bigQ : spec_of bigQ rat := bigQ2rat. (** *** Proofs of refinement *) -Global Instance refine_ratBigQ_zero : refines r_ratBigQ 0%R 0%C. +#[export] Instance refine_ratBigQ_zero : refines r_ratBigQ 0%R 0%C. Proof. rewrite refinesE /r_ratBigQ unlock; red; exact: val_inj. Qed. -Global Instance refine_ratBigQ_one : refines r_ratBigQ 1%R 1%C. +#[export] Instance refine_ratBigQ_one : refines r_ratBigQ 1%R 1%C. Proof. rewrite refinesE /r_ratBigQ unlock; red; exact: val_inj. Qed. -Global Instance refine_ratBigQ_opp : refines (r_ratBigQ ==> r_ratBigQ) -%R -%C. +#[export] Instance refine_ratBigQ_opp : refines (r_ratBigQ ==> r_ratBigQ) -%R -%C. Proof. rewrite refinesE => _ a <-; rewrite /r_ratBigQ unlock /fun_hrel /=. rewrite BigQ.strong_spec_opp Qred_opp [in LHS]/Qnum /=. @@ -481,7 +481,7 @@ rewrite -[LHS]/(Z2int (Z.pos (Z.to_pos [dy]%bigN))) Z2Pos.id //. exact: BigQ.N_to_Z_pos. Qed. -Global Instance refine_ratBigQ_add : +#[export] Instance refine_ratBigQ_add : refines (r_ratBigQ ==> r_ratBigQ ==> r_ratBigQ) +%R +%C. Proof. rewrite refinesE => _ a <- _ b <-; rewrite /r_ratBigQ unlock /fun_hrel /=. @@ -494,14 +494,14 @@ rewrite intrD PoszM !intrM. by rewrite [RHS]addf_div // intq_eq0 Posz_nat_of_pos_neq0. Qed. -Global Instance refine_ratBigQ_sub : +#[export] Instance refine_ratBigQ_sub : refines (r_ratBigQ ==> r_ratBigQ ==> r_ratBigQ) (fun x y => x - y)%R sub_op. Proof. apply refines_abstr2=> a b rab c d rcd. rewrite /sub_op /sub_bigQ /BigQ.sub_norm; eapply refines_apply; tc. Qed. -Global Instance refine_ratBigQ_mul : +#[export] Instance refine_ratBigQ_mul : refines (r_ratBigQ ==> r_ratBigQ ==> r_ratBigQ) *%R *%C. Proof. rewrite refinesE => _ a <- _ b <-; rewrite /r_ratBigQ unlock /fun_hrel /=. @@ -514,7 +514,7 @@ rewrite PoszM !intrM. by rewrite [RHS]mulf_div. Qed. -Global Instance refine_ratBigQ_inv : +#[export] Instance refine_ratBigQ_inv : refines (r_ratBigQ ==> r_ratBigQ)%rel GRing.inv inv_op. Proof. rewrite refinesE => _ a <-; rewrite /r_ratBigQ unlock /fun_hrel /=. @@ -528,7 +528,7 @@ rewrite [Qden (_ #da)]/= !Z2int_Qred invf_div. by rewrite -!Pos2Z.opp_pos !Z2int_opp !mulrNz mulNr invrN mulrN. Qed. -Global Instance refine_ratBigQ_div : +#[export] Instance refine_ratBigQ_div : refines (r_ratBigQ ==> r_ratBigQ ==> r_ratBigQ)%rel (fun x y => x / y)%R div_op. Proof. apply: refines_abstr2 => x1 x2 rx y1 y2 ry. @@ -536,7 +536,7 @@ rewrite /div_op /div_bigQ /BigQ.div_norm. exact: refines_apply. Qed. -Global Instance refine_ratBigQ_eq : +#[export] Instance refine_ratBigQ_eq : refines (r_ratBigQ ==> r_ratBigQ ==> eq) eqtype.eq_op eq_op. Proof. rewrite refinesE => _ a <- _ b <-; rewrite /r_ratBigQ unlock /fun_hrel /=. @@ -551,7 +551,7 @@ rewrite -!intrM -!Z2int_mul eqr_int. by case: Z.eqb_spec => [->|eq]; apply/eqP => // eq'; apply/eq/Z2int_inj. Qed. -Global Instance refine_ratBigQ_eq' : +#[export] Instance refine_ratBigQ_eq' : refines (r_ratBigQ ==> r_ratBigQ ==> bool_R)%rel eqtype.eq_op eq_op. Proof. rewrite refinesE => x1 x2 rx y1 y2 ry. @@ -559,7 +559,7 @@ move: refine_ratBigQ_eq; rewrite refinesE => /(_ _ _ rx _ _ ry) <-. case: (_ == _); constructor. Qed. -Global Instance refine_ratBigQ_lt : +#[export] Instance refine_ratBigQ_lt : refines (r_ratBigQ ==> r_ratBigQ ==> bool_R) Num.lt lt_op. Proof. rewrite refinesE => _ a <- _ b <-; rewrite /r_ratBigQ unlock /fun_hrel /=. @@ -577,7 +577,7 @@ case: ltP. by move=> /(proj1 (Z2int_le _ _)) /(proj2 (Z.ltb_ge _ _)) => ->. Qed. -Global Instance refine_ratBigQ_le : +#[export] Instance refine_ratBigQ_le : refines (r_ratBigQ ==> r_ratBigQ ==> bool_R) Num.le leq_op. Proof. rewrite refinesE => _ a <- _ b <-; rewrite /r_ratBigQ unlock /fun_hrel /=. @@ -596,7 +596,7 @@ case: leP. by move=> /(proj1 (Z2int_lt _ _)) /Zlt_compare; case: Z.compare. Qed. -Global Instance refine_ratBigQ_max : +#[export] Instance refine_ratBigQ_max : refines (r_ratBigQ ==> r_ratBigQ ==> r_ratBigQ)%rel Num.max max_op. Proof. apply: refines_abstr2 => x1 x2 rx y1 y2 ry. @@ -606,7 +606,7 @@ rewrite /lt_op /lt_bigQ /max_op /max_bigQ /BigQ.max. by case: (_ ?= _)%bigQ. Qed. -Global Instance refine_ratBigQ_min : +#[export] Instance refine_ratBigQ_min : refines (r_ratBigQ ==> r_ratBigQ ==> r_ratBigQ)%rel Num.min min_op. Proof. apply: refines_abstr2 => x1 x2 rx y1 y2 ry. @@ -617,7 +617,7 @@ rewrite !BigQ.spec_compare -QArith_base.Qcompare_antisym. by case: QArith_base.Qcompare. Qed. -Global Instance refine_ratBigQ_of_nat : +#[export] Instance refine_ratBigQ_of_nat : refines (nat_R ==> r_ratBigQ)%rel (fun n => n%:~R%R) cast_op. Proof. rewrite refinesE => n _ /nat_R_eq <-; rewrite /r_ratBigQ unlock /fun_hrel. @@ -625,11 +625,11 @@ rewrite /= Z_ggcd_1_r /= BigZ.spec_of_Z mulr1. by apply/eqP; rewrite eqr_int Z2int_Z_of_nat. Qed. -Global Instance refine_ratBigQ_spec : +#[export] Instance refine_ratBigQ_spec : refines (eq ==> r_ratBigQ)%rel spec spec_id. Proof. by rewrite refinesE => x _ <-. Qed. -Global Instance refine_ratBigQ_bigQ2rat a : refines r_ratBigQ (bigQ2rat a) a. +#[export] Instance refine_ratBigQ_bigQ2rat a : refines r_ratBigQ (bigQ2rat a) a. Proof. by rewrite refinesE. Qed. End binrat_theory. diff --git a/refinements/boolF2.v b/refinements/boolF2.v index fc0b52b..571c2d2 100644 --- a/refinements/boolF2.v +++ b/refinements/boolF2.v @@ -9,21 +9,21 @@ Import Refinements.Op. Section operations. -Global Instance zero_bool : zero_of bool := false. +#[export] Instance zero_bool : zero_of bool := false. -Global Instance one_bool : one_of bool := true. +#[export] Instance one_bool : one_of bool := true. -Global Instance opp_bool : opp_of bool := id. +#[export] Instance opp_bool : opp_of bool := id. -Global Instance add_bool : add_of bool := xorb. +#[export] Instance add_bool : add_of bool := xorb. -Global Instance sub_bool : sub_of bool := xorb. +#[export] Instance sub_bool : sub_of bool := xorb. -Global Instance mul_bool : mul_of bool := andb. +#[export] Instance mul_bool : mul_of bool := andb. -Global Instance inv_bool : inv_of bool := id. +#[export] Instance inv_bool : inv_of bool := id. -Global Instance eq_bool : eq_of bool := eqtype.eq_op. +#[export] Instance eq_bool : eq_of bool := eqtype.eq_op. End operations. @@ -36,19 +36,19 @@ Definition F2_of_bool (x : bool) : 'F_2 := x%:R. Definition Rbool := fun_hrel F2_of_bool. -Global Instance Rbool_zero : refines Rbool 0 0%C. +#[export] Instance Rbool_zero : refines Rbool 0 0%C. Proof. by rewrite refinesE. Qed. -Global Instance Rbool_one : refines Rbool 1 1%C. +#[export] Instance Rbool_one : refines Rbool 1 1%C. Proof. by rewrite refinesE. Qed. -Global Instance Rbool_opp : refines (Rbool ==> Rbool) -%R -%C. +#[export] Instance Rbool_opp : refines (Rbool ==> Rbool) -%R -%C. Proof. rewrite refinesE=> x []; rewrite /Rbool /F2_of_bool /fun_hrel /= => <- //. by rewrite GRing.mulr0n GRing.oppr0. Qed. -Global Instance Rbool_add : refines (Rbool ==> Rbool ==> Rbool) +%R +%C. +#[export] Instance Rbool_add : refines (Rbool ==> Rbool ==> Rbool) +%R +%C. Proof. rewrite refinesE /Rbool /F2_of_bool /fun_hrel => x [] <- y [] <- //=. by rewrite -GRing.natrD char_Zp. @@ -56,14 +56,14 @@ by rewrite GRing.add0r. Qed. (* TODO: lemma for sub *) -Global Instance Rbool_sub : +#[export] Instance Rbool_sub : refines (Rbool ==> Rbool ==> Rbool) (fun x y => x - y) sub_op. Proof. rewrite refinesE /Rbool /F2_of_bool /fun_hrel=> x [] <- y [] <- //=; by apply/eqP; rewrite eq_sym GRing.subr_eq0. Qed. -Global Instance Rbool_mul : refines (Rbool ==> Rbool ==> Rbool) *%R *%C. +#[export] Instance Rbool_mul : refines (Rbool ==> Rbool ==> Rbool) *%R *%C. Proof. rewrite refinesE /Rbool /F2_of_bool /fun_hrel => x [] <- y [] <- //=. + by rewrite GRing.mulr0. @@ -71,12 +71,12 @@ rewrite refinesE /Rbool /F2_of_bool /fun_hrel => x [] <- y [] <- //=. by rewrite GRing.mul0r. Qed. -Global Instance Rbool_inv : refines (Rbool ==> Rbool) GRing.inv inv_bool. +#[export] Instance Rbool_inv : refines (Rbool ==> Rbool) GRing.inv inv_bool. Proof. by rewrite refinesE=> x []; rewrite /Rbool /F2_of_bool /fun_hrel /= => <- //. Qed. -Global Instance Rbool_eq : +#[export] Instance Rbool_eq : refines (Rbool ==> Rbool ==> bool_R) eqtype.eq_op eq_op. Proof. by rewrite refinesE /Rbool /F2_of_bool /fun_hrel=> x [] <- y [] <-. diff --git a/refinements/examples/irred.v b/refinements/examples/irred.v index 806f56d..65de891 100644 --- a/refinements/examples/irred.v +++ b/refinements/examples/irred.v @@ -165,21 +165,21 @@ Qed. End Irreducible. -Module nat_ops. +Module Import nat_ops. -#[global] Instance zero_nat : zero_of nat := 0%N. -#[global] Instance one_nat : one_of nat := 1%N. -#[global] Instance add_nat : add_of nat := addn. -#[global] Instance sub_nat : sub_of nat := subn. -#[global] Instance mul_nat : mul_of nat := muln. -#[global] Instance exp_nat : exp_of nat nat := expn. -#[global] Instance leq_nat : leq_of nat := ssrnat.leq. -#[global] Instance lt_nat : lt_of nat := ssrnat.ltn. -#[global] Instance eq_nat : eq_of nat := eqtype.eq_op. +#[export] Instance zero_nat : zero_of nat := 0%N. +#[export] Instance one_nat : one_of nat := 1%N. +#[export] Instance add_nat : add_of nat := addn. +#[export] Instance sub_nat : sub_of nat := subn. +#[export] Instance mul_nat : mul_of nat := muln. +#[export] Instance exp_nat : exp_of nat nat := expn. +#[export] Instance leq_nat : leq_of nat := ssrnat.leq. +#[export] Instance lt_nat : lt_of nat := ssrnat.ltn. +#[export] Instance eq_nat : eq_of nat := eqtype.eq_op. -#[global] Instance spec_nat : spec_of nat nat := spec_id. +#[export] Instance spec_nat : spec_of nat nat := spec_id. -#[global] Instance implem_nat : implem_of nat nat := implem_id. +#[export] Instance implem_nat : implem_of nat nat := implem_id. End nat_ops. @@ -216,7 +216,7 @@ Context `{!refines rN 1%N 1%C}. Context `{!refines (rN ==> rN ==> rN)%rel addn add_op}. Context (P : pred T) (P' : pred T'). -Global Instance refines_card : +#[export] Instance refines_card : (forall x x' `{!refines RT x x'}, refines (bool_R \o (@unify _)) (P x) (P' x')) -> refines rN #|[pred x | P x]| (card' enumT' P'). Proof. @@ -237,7 +237,7 @@ End enum_boolF2. Parametricity enum_boolF2. -Global Instance refines_enum_boolF2 : +#[export] Instance refines_enum_boolF2 : refines (perm_eq \o list_R Rbool) (Finite.enum [finType of 'F_2]) (enum_boolF2). Proof. rewrite -enumT; refines_trans; last first. @@ -295,7 +295,7 @@ Definition Rnpoly : {poly_n A} -> {poly A} -> Type := Definition RnpolyC : {poly_n A} -> seqpoly C -> Type := (Rnpoly \o (RseqpolyC rAC))%rel. -Global Instance refines_enum_npoly : +#[export] Instance refines_enum_npoly : refines (perm_eq \o list_R RnpolyC) (Finite.enum [finType of {poly_n A}]) (enum_npoly n' iter' enumC id). Proof. @@ -306,13 +306,13 @@ param enum_npoly_R. Admitted. -Global Instance refines_RnpolyCpoly (x : {poly_n A}) (y : seqpoly C) +#[export] Instance refines_RnpolyCpoly (x : {poly_n A}) (y : seqpoly C) `{!refines RnpolyC x y} : refines (RseqpolyC rAC) (poly_of_npoly x) y. Admitted. End RnpolyC. -Global Instance refines_iter T T' RT : +#[export] Instance refines_iter T T' RT : refines (Rnat ==> (RT ==> RT) ==> RT ==> RT) (@iter T) (@iter T'). Proof. param iter_R. @@ -320,7 +320,7 @@ Admitted. Section LaurentsProblem. -Global Instance refines_predn : refines (Rnat ==> Rnat) predn (fun n => (n - 1)%C). +#[export] Instance refines_predn : refines (Rnat ==> Rnat) predn (fun n => (n - 1)%C). Admitted. Lemma test_irred : irreducible_poly ('X^5 + 'X^2 + 1 : {poly 'F_2}). diff --git a/refinements/hpoly.v b/refinements/hpoly.v index ca1cb0d..9ccad6f 100644 --- a/refinements/hpoly.v +++ b/refinements/hpoly.v @@ -53,18 +53,18 @@ Fixpoint from_seq (p : seq A) : hpoly A := match p with | x :: xs => PX x 1 (from_seq xs) end. -Global Instance cast_hpoly : cast_of A (hpoly A) := fun x => Pc x. +#[export] Instance cast_hpoly : cast_of A (hpoly A) := fun x => Pc x. -Global Instance zero_hpoly : zero_of (hpoly A) := Pc 0. -Global Instance one_hpoly : one_of (hpoly A) := Pc 1. +#[export] Instance zero_hpoly : zero_of (hpoly A) := Pc 0. +#[export] Instance one_hpoly : one_of (hpoly A) := Pc 1. Fixpoint map_hpoly A B (f : A -> B) (p : hpoly A) : hpoly B := match p with | Pc c => Pc (f c) | PX a n p => PX (f a) n (map_hpoly f p) end. -Global Instance opp_hpoly : opp_of (hpoly A) := map_hpoly -%C. -Global Instance scale_hpoly : scale_of A (hpoly A) := +#[export] Instance opp_hpoly : opp_of (hpoly A) := map_hpoly -%C. +#[export] Instance scale_hpoly : scale_of A (hpoly A) := fun a => map_hpoly [eta *%C a]. Fixpoint addXn_const (n : N) a (q : hpoly A) := match q with @@ -99,13 +99,13 @@ Fixpoint addXn (n : N) p q {struct p} := match p, q with (* else PX (a + b) m (add_hpoly_op q (PX 0 (n - m) p)) *) (* end. *) -Global Instance add_hpoly : add_of (hpoly A) := addXn 0. -Global Instance sub_hpoly : sub_of (hpoly A) := fun p q => p + - q. +#[export] Instance add_hpoly : add_of (hpoly A) := addXn 0. +#[export] Instance sub_hpoly : sub_of (hpoly A) := fun p q => p + - q. -Global Instance shift_hpoly : shift_of (hpoly A) N := +#[export] Instance shift_hpoly : shift_of (hpoly A) N := fun n p => if (n == 0)%C then p else PX 0 (cast n) p. -Global Instance mul_hpoly : mul_of (hpoly A) := fix f p q := match p, q with +#[export] Instance mul_hpoly : mul_of (hpoly A) := fix f p q := match p, q with | Pc a, q => a *: q | p, Pc b => map_hpoly (fun x => (x * b)%C) p | PX a n p, PX b m q => @@ -113,7 +113,7 @@ Global Instance mul_hpoly : mul_of (hpoly A) := fix f p q := match p, q with (shift_hpoly (cast n) (map_hpoly (fun x => (x * b)%C) p) + Pc (a * b)) end. -Global Instance exp_hpoly : exp_of (hpoly A) N := +#[export] Instance exp_hpoly : exp_of (hpoly A) N := fun p n => iter (spec n) (mul_hpoly p) 1. Fixpoint eq0_hpoly (p : hpoly A) : bool := match p with @@ -121,7 +121,7 @@ Fixpoint eq0_hpoly (p : hpoly A) : bool := match p with | PX a n p' => (eq0_hpoly p') && (a == 0)%C end. -Global Instance eq_hpoly : eq_of (hpoly A) := fun p q => eq0_hpoly (p - q). +#[export] Instance eq_hpoly : eq_of (hpoly A) := fun p q => eq0_hpoly (p - q). (* Alternative definition, should be used with normalize: *) (* Fixpoint eq_hpoly_op p q {struct p} := match p, q with *) @@ -130,7 +130,7 @@ Global Instance eq_hpoly : eq_of (hpoly A) := fun p q => eq0_hpoly (p - q). (* | _, _ => false *) (* end. *) -Global Instance size_hpoly : size_of (hpoly A) N := +#[export] Instance size_hpoly : size_of (hpoly A) N := fix f p := if eq0_hpoly p then 0%C else match p with | Pc a => 1%C @@ -138,7 +138,7 @@ Global Instance size_hpoly : size_of (hpoly A) N := else (cast n + f p')%C end. -Global Instance lead_coef_hpoly : lead_coef_of A (hpoly A) := +#[export] Instance lead_coef_hpoly : lead_coef_of A (hpoly A) := fix f p := match p with | Pc a => a @@ -146,7 +146,7 @@ Global Instance lead_coef_hpoly : lead_coef_of A (hpoly A) := if (b == 0)%C then a else b end. -Global Instance split_hpoly : split_of (hpoly A) N := +#[export] Instance split_hpoly : split_of (hpoly A) N := fix f m p:= if (m == 0)%C then (p, Pc 0)%C else match p with @@ -227,7 +227,7 @@ Fixpoint spec_hpoly_aux n (p : @hpoly pos C) : {poly R} := (spec_hpoly_aux k p) + mon end. -Global Instance spec_hpoly : spec_of (hpoly C) {poly R} := spec_hpoly_aux 0%N. +#[export] Instance spec_hpoly : spec_of (hpoly C) {poly R} := spec_hpoly_aux 0%N. Lemma spec_aux_shift n p : spec_hpoly_aux n p = spec_hpoly_aux 0%N p * 'X^n. @@ -686,28 +686,28 @@ Context `{!refines (rN ==> nat_R) spec_id spec}. Definition RhpolyC := (Rhpoly \o (hpoly_R rP rAC)). -Global Instance RhpolyC_0 : refines RhpolyC 0%R 0%C. +#[export] Instance RhpolyC_0 : refines RhpolyC 0%R 0%C. Proof. param_comp zero_hpoly_R. Qed. -Global Instance RhpolyC_1 : refines RhpolyC 1%R 1%C. +#[export] Instance RhpolyC_1 : refines RhpolyC 1%R 1%C. Proof. param_comp one_hpoly_R. Qed. -Global Instance RhpolyCD : refines (RhpolyC ==> RhpolyC ==> RhpolyC) +#[export] Instance RhpolyCD : refines (RhpolyC ==> RhpolyC ==> RhpolyC) +%R (add_hpoly (N:=N)). Proof. param_comp add_hpoly_R. Qed. -Global Instance RhpolyCN : refines (RhpolyC ==> RhpolyC) -%R -%C. +#[export] Instance RhpolyCN : refines (RhpolyC ==> RhpolyC) -%R -%C. Proof. param_comp opp_hpoly_R. Qed. -Global Instance RhpolyC_sub : refines (RhpolyC ==> RhpolyC ==> RhpolyC) +#[export] Instance RhpolyC_sub : refines (RhpolyC ==> RhpolyC ==> RhpolyC) (fun x y => x - y) (sub_hpoly (N:=N)). Proof. param_comp sub_hpoly_R. Qed. -Global Instance RhpolyCM : +#[export] Instance RhpolyCM : refines (RhpolyC ==> RhpolyC ==> RhpolyC) *%R (mul_hpoly (N:=N)). Proof. param_comp mul_hpoly_R. Qed. -Global Instance RhpolyC_exp : +#[export] Instance RhpolyC_exp : refines (RhpolyC ==> rN ==> RhpolyC) (@GRing.exp _) exp_op. Proof. eapply refines_trans; tc. @@ -716,29 +716,29 @@ Proof. exact: refinesP. Qed. -Global Instance RhpolyC_size : +#[export] Instance RhpolyC_size : refines (RhpolyC ==> rN) (sizep (R:=A)) size_hpoly. Proof. param_comp size_hpoly_R. Qed. -Global Instance RhpolyC_lead_coef : +#[export] Instance RhpolyC_lead_coef : refines (RhpolyC ==> rAC) lead_coef lead_coef_op. Proof. rewrite /lead_coef_op. param_comp lead_coef_hpoly_R. Qed. -Global Instance RhpolyC_polyC : +#[export] Instance RhpolyC_polyC : refines (rAC ==> RhpolyC) (fun a => a%:P) cast. Proof. param_comp cast_hpoly_R. Qed. -Global Instance RhpolyC_eq : refines (RhpolyC ==> RhpolyC ==> bool_R) +#[export] Instance RhpolyC_eq : refines (RhpolyC ==> RhpolyC ==> bool_R) eqtype.eq_op (eq_hpoly (N:=N)). Proof. param_comp eq_hpoly_R. Qed. -Global Instance RhpolyC_scale : refines (rAC ==> RhpolyC ==> RhpolyC) *:%R *:%C. +#[export] Instance RhpolyC_scale : refines (rAC ==> RhpolyC ==> RhpolyC) *:%R *:%C. Proof. param_comp scale_hpoly_R. Qed. -Global Instance RhpolyC_shift : refines (rN ==> RhpolyC ==> RhpolyC) +#[export] Instance RhpolyC_shift : refines (rN ==> RhpolyC ==> RhpolyC) (shiftp (R:=A)) shift_hpoly. Proof. eapply refines_trans; tc. @@ -747,17 +747,17 @@ Proof. exact: refinesP. Qed. -Global Instance RhpolyCMXn p sp n rn : +#[export] Instance RhpolyCMXn p sp n rn : refines rN n rn -> refines RhpolyC p sp -> refines RhpolyC (p * 'X^n) (shift_op rn sp). Proof. by move=> hn hp; rewrite -[_ * 'X^_]/(shiftp _ _); tc. Qed. -Global Instance RhpolyC_Xnmul p sp n rn : +#[export] Instance RhpolyC_Xnmul p sp n rn : refines rN n rn -> refines RhpolyC p sp -> refines RhpolyC ('X^n * p) (shift_op rn sp). Proof. rewrite -mulXnC; exact: RhpolyCMXn. Qed. -Global Instance RhpolyC_scaleXn c rc n rn : +#[export] Instance RhpolyC_scaleXn c rc n rn : refines rN n rn -> refines rAC c rc -> refines RhpolyC (c *: 'X^n) (shift_op rn (cast rc)). Proof. @@ -765,20 +765,20 @@ Proof. exact: refines_apply. Qed. -Global Instance RhpolyCMX p sp : +#[export] Instance RhpolyCMX p sp : refines RhpolyC p sp -> refines RhpolyC (p * 'X) (shift_op (1%C : N) sp). Proof. rewrite -['X]expr1; exact: RhpolyCMXn. Qed. -Global Instance RhpolyC_Xmul p sp : +#[export] Instance RhpolyC_Xmul p sp : refines RhpolyC p sp -> refines RhpolyC ('X * p) (shift_op (1%C : N) sp). Proof. rewrite -['X]expr1 -mulXnC; exact: RhpolyCMX. Qed. -Global Instance RhpolyC_scaleX c rc : +#[export] Instance RhpolyC_scaleX c rc : refines rAC c rc -> refines RhpolyC (c *: 'X) (shift_op (1%C : N) (cast rc)). Proof. rewrite -['X]expr1; exact: RhpolyC_scaleXn. Qed. -Global Instance RhpolyC_split : +#[export] Instance RhpolyC_split : refines (rN ==> RhpolyC ==> prod_R RhpolyC RhpolyC) (splitp (R:=A)) split_op. Proof. @@ -788,7 +788,7 @@ refines_trans. exact: refinesP. Qed. -Global Instance RhpolyC_splitn n rn p sp : +#[export] Instance RhpolyC_splitn n rn p sp : refines rN n rn -> refines RhpolyC p sp -> refines (prod_R RhpolyC RhpolyC) (splitp n p) (split_op rn sp). Proof. by move=> hn hp; exact: refines_apply. Qed. @@ -798,7 +798,7 @@ Proof. by move=> hn hp; exact: refines_apply. Qed. Definition eq_prod_hpoly (x y : (@hpoly P C * @hpoly P C)) := (eq_hpoly (N:=N) x.1 y.1) && (eq_hpoly (N:=N) x.2 y.2). -Global Instance refines_prod_RhpolyC_eq : +#[export] Instance refines_prod_RhpolyC_eq : refines (prod_R RhpolyC RhpolyC ==> prod_R RhpolyC RhpolyC ==> bool_R) eqtype.eq_op eq_prod_hpoly. Proof. @@ -811,23 +811,23 @@ Proof. exact: bool_Rxx. Qed. -Global Instance RhpolyC_X : refines RhpolyC 'X (shift_op (1%C : N) 1)%C. +#[export] Instance RhpolyC_X : refines RhpolyC 'X (shift_op (1%C : N) 1)%C. Proof. rewrite -['X]mul1r; exact: RhpolyCMX. Qed. -Global Instance RhpolyC_Xn n rn : +#[export] Instance RhpolyC_Xn n rn : refines rN n rn -> refines RhpolyC 'X^n (shift_op rn 1)%C. Proof. move=> hn; rewrite -['X^_]mul1r; exact: RhpolyCMXn. Qed. -(* Global Instance RhpolyC_horner : param (RhpolyC ==> rAC ==> rAC) *) +(* #[export] Instance RhpolyC_horner : param (RhpolyC ==> rAC ==> rAC) *) (* (fun p x => p.[x]) (fun sp x => horner_seq sp x). *) (* Proof. admit. Qed. *) (* (* Proof. exact: param_trans. Qed. *) *) -Global Instance RhpolyC_head : +#[export] Instance RhpolyC_head : refines (RhpolyC ==> rAC) (fun p => p`_0) head_hpoly. Proof. param_comp head_hpoly_R. Qed. -Global Instance RhpolyC_spec : +#[export] Instance RhpolyC_spec : refines (RhpolyC ==> eq) spec_id (spec_hpoly (N:=N) (C:=C)). Proof. eapply refines_trans; tc. diff --git a/refinements/karatsuba.v b/refinements/karatsuba.v index 94c06b5..91302c2 100644 --- a/refinements/karatsuba.v +++ b/refinements/karatsuba.v @@ -110,18 +110,18 @@ Context `{!split_of polyC N}. Context `{!refines (rN ==> RpolyC ==> prod_R RpolyC RpolyC) split_polyR split_op}. -Global Instance RpolyC_karatsuba_rec : +#[export] Instance RpolyC_karatsuba_rec : refines (nat_R ==> RpolyC ==> RpolyC ==> RpolyC) (karatsuba_rec (polyA:={poly R}) (N:=nat)) (karatsuba_rec (polyA:=polyC) (N:=N)). Proof. param karatsuba_rec_R. Qed. -Global Instance RpolyC_karatsuba : +#[export] Instance RpolyC_karatsuba : refines (RpolyC ==> RpolyC ==> RpolyC) (karatsuba (polyA:={poly R}) (N:=nat)) (karatsuba (polyA:=polyC) (N:=N)). Proof. param karatsuba_R. Qed. -Global Instance RpolyC_karatsuba_mul p sp q sq : +#[export] Instance RpolyC_karatsuba_mul p sp q sq : refines RpolyC p sp -> refines RpolyC q sq -> refines RpolyC (p * q) (karatsuba (N:=N) sp sq). Proof. diff --git a/refinements/multipoly.v b/refinements/multipoly.v index 5631cdb..35e918b 100644 --- a/refinements/multipoly.v +++ b/refinements/multipoly.v @@ -563,7 +563,7 @@ case: (ltnP i k) => Hci. by exfalso; apply/Hneq/anti_leq; rewrite Hi. Qed. -Global Instance refine_mnm_add n : +#[export] Instance refine_mnm_add n : refines (Rseqmultinom ==> Rseqmultinom ==> Rseqmultinom) (@mnm_add n) mnm_add_seq. Proof. @@ -580,7 +580,7 @@ rewrite mnmDE -!refine_nth. exact: nat_of_add_bin. Qed. -Global Instance refine_mdeg n : +#[export] Instance refine_mdeg n : refines (Rseqmultinom ==> eq) (@mdeg n) mdeg_eff. Proof. rewrite refinesE. @@ -642,7 +642,7 @@ rewrite refinesE /Rseqmultinom /ofun_hrel; move/eqP=>->->. by move=> H; inversion H. Qed. -Global Instance refine_mnmc_lt n : +#[export] Instance refine_mnmc_lt n : refines (Rseqmultinom ==> Rseqmultinom ==> eq) (@mnmc_lt n) (mnmc_lt_seq). Proof. @@ -921,7 +921,7 @@ Instance : zero_of T := 0. Instance : one_of T := 1. Instance : add_of T := +%R. Instance : opp_of T := -%R. -Global Instance sub_instR : sub_of T := fun x y => (x - y). +#[export] Instance sub_instR : sub_of T := fun x y => (x - y). Instance mul_instR : mul_of T := *%R. Instance : eq_of T := fun x y => x == y. @@ -959,7 +959,7 @@ move: H; move/mapP=> [] x Hx Hx'; exists x=>//; move: Hx. by rewrite mem_filter=>/andP []. Qed. -Global Instance refine_list_of_mpoly_eff n : +#[export] Instance refine_list_of_mpoly_eff n : refines (Reffmpoly ==> list_R (prod_R Rseqmultinom eq)) (@list_of_mpoly T n) list_of_mpoly_eff. Proof. @@ -1041,14 +1041,14 @@ rewrite mem_filter Hmc2 /= in_InA_iff (surjective_pairing mc). by rewrite -F.elements_mapsto_iff; apply M.find_2. Qed. -Global Instance refine_mp0_eff n : refines (@Reffmpoly T n) 0 mp0_eff. +#[export] Instance refine_mp0_eff n : refines (@Reffmpoly T n) 0 mp0_eff. Proof. apply: refine_effmpolyP. - by move=> m /F.empty_in_iff Hm. - by move=> m m' ref_m; rewrite F.empty_o mcoeff0. Qed. -Global Instance refine_mp1_eff n : refines (@Reffmpoly T n) 1 (mp1_eff (n := n)). +#[export] Instance refine_mp1_eff n : refines (@Reffmpoly T n) 1 (mp1_eff (n := n)). Proof. apply refine_effmpolyP. - rewrite /mp1_eff => k /singleton_in_iff/mnmc_eq_seqP/eqP <-. @@ -1062,7 +1062,7 @@ apply refine_effmpolyP. by rewrite F.empty_o. Qed. -Global Instance refine_mpvar_eff {n1} : +#[export] Instance refine_mpvar_eff {n1} : refines (eq ==> Rnat ==> Rord0 ==> Reffmpoly (T := T) (n := n1)) mpvar (mpvar_eff (n := n1)). Proof. @@ -1090,7 +1090,7 @@ by apply/mnmc_eq_seqP; rewrite eq_sym Hm'. Qed. Arguments mpolyC {n R} c. -Global Instance refine_mpolyC_eff n : +#[export] Instance refine_mpolyC_eff n : refines (eq ==> Reffmpoly (T := T) (n := n)) mpolyC (mpolyC_eff (n := n)). Proof. @@ -1111,7 +1111,7 @@ by apply/mnmc_eq_seqP; move: Hm'; rewrite eq_sym =>->. Qed. Arguments mpolyX {n R} m. -Global Instance refine_mpolyX_eff n : +#[export] Instance refine_mpolyX_eff n : refines (Rseqmultinom ==> Reffmpoly (T := T) (n := n)) mpolyX mpolyX_eff. Proof. @@ -1150,7 +1150,7 @@ by move/F.not_find_in_iff: Hin ->. Qed. Arguments mpoly_scale {n R} c p. -Global Instance refine_mpoly_scale_eff n : +#[export] Instance refine_mpoly_scale_eff n : refines (eq ==> Reffmpoly ==> Reffmpoly (T := T) (n := n)) mpoly_scale mpoly_scale_eff. Proof. @@ -1172,7 +1172,7 @@ exact/F.map_in_iff. Qed. Arguments mpoly_add {n R} p q. -Global Instance refine_mpoly_add_eff n : +#[export] Instance refine_mpoly_add_eff n : refines (Reffmpoly ==> Reffmpoly ==> Reffmpoly (T := T) (n := n)) mpoly_add mpoly_add_eff. Proof. @@ -1209,7 +1209,7 @@ Qed. Definition mpoly_sub {n} (p : {mpoly T[n]}) q := mpoly_add p (mpoly_opp q). -Global Instance refine_mpoly_sub_eff n : +#[export] Instance refine_mpoly_sub_eff n : refines (Reffmpoly ==> Reffmpoly ==> Reffmpoly (T := T) (n := n)) mpoly_sub mpoly_sub_eff. apply refines_abstr => p p' ref_p. @@ -1464,7 +1464,7 @@ by rewrite -[RHS]commr_mpolyX -GRing.scalerAl commr_mpolyX. Qed. Arguments mpoly_mul {n R} p q. -Global Instance refine_mpoly_mul_eff n : +#[export] Instance refine_mpoly_mul_eff n : refines (Reffmpoly ==> Reffmpoly ==> Reffmpoly (T := T) (n := n)) mpoly_mul mpoly_mul_eff. Proof. @@ -1487,7 +1487,7 @@ Qed. Definition mpoly_exp {n} (p : {mpoly T[n]}) (n : nat) := p ^+ n. -Global Instance refine_mpoly_exp_eff n : +#[export] Instance refine_mpoly_exp_eff n : refines (Reffmpoly ==> Rnat ==> Reffmpoly (T := T) (n := n)) mpoly_exp (mpoly_exp_eff (n:=n)). Proof. @@ -1550,7 +1550,7 @@ by apply ord_inj; rewrite inordK //; move: (ltn_ord i). Qed. Arguments comp_mpoly {n R k} lq p. -Global Instance refine_comp_mpoly_eff n k : +#[export] Instance refine_comp_mpoly_eff n k : refines (@seq_Reffmpoly n k ==> Reffmpoly ==> Reffmpoly) comp_mpoly (comp_mpoly_eff (n:= n)). Proof. @@ -1862,7 +1862,7 @@ eapply IHt. - rewrite -H2 -H4; exact: Heqs. Qed. -Global Instance refine_filter A' B (rAB : A' -> B -> Type) : +#[export] Instance refine_filter A' B (rAB : A' -> B -> Type) : refines ((rAB ==> eq) ==> list_R rAB ==> list_R rAB) filter filter. Proof. @@ -1878,7 +1878,7 @@ specialize (IH t' (trivial_refines Ht)); rewrite refinesE in IH. by case (f' h') => //; apply list_R_cons_R. Qed. -Global Instance ReffmpolyC_list_of_mpoly_eff n : +#[export] Instance ReffmpolyC_list_of_mpoly_eff n : refines (@ReffmpolyC n ==> list_R (prod_R Rseqmultinom rAC)) (@list_of_mpoly A n) list_of_mpoly_eff. @@ -1923,14 +1923,14 @@ rewrite refinesE in rmc; inversion rmc as [a a' ref_a b b' ref_b]. apply refinesP; tc. Qed. -Global Instance ReffmpolyC_mp0_eff (n : nat) : +#[export] Instance ReffmpolyC_mp0_eff (n : nat) : refines (@ReffmpolyC n) 0 (@mp0_eff C). Proof. eapply refines_trans; [by apply composable_comp|by apply refine_mp0_eff|]. apply refine_M_hrel_empty. Qed. -Global Instance ReffmpolyC_mp1_eff (n : nat) : +#[export] Instance ReffmpolyC_mp1_eff (n : nat) : refines (@ReffmpolyC n) 1 (mp1_eff (n:=n)). Proof. eapply refines_trans; [by apply composable_comp|by apply refine_mp1_eff|]. @@ -1948,7 +1948,7 @@ rewrite !composableE => R123 fA fC [fB [RfAB RfBC]] a c rABac. apply: R123; exists (fB c); split; [ exact: RfAB | exact: RfBC ]. Qed. -Global Instance ReffmpolyC_mpvar_eff {n1 : nat} : +#[export] Instance ReffmpolyC_mpvar_eff {n1 : nat} : refines (rAC ==> Rnat ==> Rord0 ==> @ReffmpolyC n1) mpvar (mpvar_eff (n:=n1)). Proof. @@ -1967,7 +1967,7 @@ eapply refines_apply; [apply refine_M_hrel_singleton|apply trivial_refines]. by rewrite (refines_eq ref_d) (refines_eq ref_i). Qed. -Global Instance ReffmpolyC_mpolyC_eff (n : nat) : +#[export] Instance ReffmpolyC_mpolyC_eff (n : nat) : refines (rAC ==> ReffmpolyC) (@mpolyC n A) (mpolyC_eff (n:=n)). Proof. eapply refines_trans. @@ -1979,7 +1979,7 @@ rewrite /mpolyC_eff; eapply refines_apply; by [apply refine_M_hrel_singleton|apply trivial_refines]. Qed. -Global Instance ReffmpolyC_mpolyX_eff (n : nat) : +#[export] Instance ReffmpolyC_mpolyX_eff (n : nat) : refines (Rseqmultinom ==> ReffmpolyC) (@mpolyX n A) mpolyX_eff. Proof. eapply refines_trans; [|by apply refine_mpolyX_eff|]. @@ -2005,7 +2005,7 @@ eapply refinesP; refines_apply; rewrite refinesE. by eapply (Hp2 _ _ _ Ha2 Hc2). Qed. -Global Instance ReffmpolyC_mpoly_scale_eff (n : nat) : +#[export] Instance ReffmpolyC_mpoly_scale_eff (n : nat) : refines (rAC ==> ReffmpolyC ==> ReffmpolyC) (@mpoly_scale n A) mpoly_scale_eff. Proof. by eapply refines_trans; first eapply composable_imply_id1; tc. Qed. @@ -2021,7 +2021,7 @@ case: ref_a; case: ref_b => *; constructor =>//. by eapply refinesP; refines_apply. Qed. -Global Instance ReffmpolyC_mpoly_add_eff (n : nat) : +#[export] Instance ReffmpolyC_mpoly_add_eff (n : nat) : refines (ReffmpolyC ==> ReffmpolyC ==> ReffmpolyC) (@mpoly_add n A) mpoly_add_eff. Proof. by eapply refines_trans; first eapply composable_imply; tc. Qed. @@ -2038,7 +2038,7 @@ by eapply refinesP; refines_apply. by eapply refinesP; refines_apply. Qed. -Global Instance ReffmpolyC_mpoly_sub_eff (n : nat) : +#[export] Instance ReffmpolyC_mpoly_sub_eff (n : nat) : refines (ReffmpolyC ==> ReffmpolyC ==> ReffmpolyC) (@mpoly_sub A n) mpoly_sub_eff. Proof. by eapply refines_trans; first eapply composable_imply; tc. Qed. @@ -2092,7 +2092,7 @@ done. by tc. Qed. -Global Instance ReffmpolyC_mpoly_mul_eff (n : nat) : +#[export] Instance ReffmpolyC_mpoly_mul_eff (n : nat) : refines (ReffmpolyC ==> ReffmpolyC ==> ReffmpolyC) (@mpoly_mul n A) mpoly_mul_eff. Proof. by eapply refines_trans; first eapply composable_imply; tc. Qed. @@ -2112,7 +2112,7 @@ elim: nk {Ek} => [|nk IHnk] /=. eapply refines_apply; first eapply refines_apply; try by tc. Qed. -Global Instance ReffmpolyC_mpoly_exp_eff (n : nat) : +#[export] Instance ReffmpolyC_mpoly_exp_eff (n : nat) : refines (ReffmpolyC ==> Rnat ==> ReffmpolyC) (@mpoly_exp A n) (mpoly_exp_eff (n:=n)). Proof. by eapply refines_trans; first eapply composable_imply; tc. Qed. @@ -2165,7 +2165,7 @@ done. by tc. Qed. -Global Instance ReffmpolyC_comp_mpoly_eff (n k : nat) : +#[export] Instance ReffmpolyC_comp_mpoly_eff (n k : nat) : refines (seq_ReffmpolyC (k:=k) ==> ReffmpolyC ==> ReffmpolyC) (comp_mpoly (k:=n)) (comp_mpoly_eff (n:=n)). Proof. by eapply refines_trans; first eapply composable_imply; tc. Qed. diff --git a/refinements/param.v b/refinements/param.v index 63bbfd8..7632bcf 100644 --- a/refinements/param.v +++ b/refinements/param.v @@ -5,12 +5,12 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Global Ltac destruct_reflexivity := +#[global] Ltac destruct_reflexivity := intros ; repeat match goal with | [ x : _ |- _ = _ ] => destruct x; reflexivity; fail end. -Global Parametricity Tactic := destruct_reflexivity. +#[global] Parametricity Tactic := destruct_reflexivity. (** Automation: for turning [sth_R a b] goals into mere [a = b] goals, do [suff_eq sth_Rxx]. *) diff --git a/refinements/poly_div.v b/refinements/poly_div.v index 9ff663a..21c4857 100644 --- a/refinements/poly_div.v +++ b/refinements/poly_div.v @@ -34,17 +34,17 @@ Definition div_rec_poly (q : polyR) := let r1 := (r * cq - m * q)%C in if n is n1.+1 then loop (k + 1)%C qq1 r1 n1 else ((k + 1)%C, qq1, r1). -Global Instance div_poly : div_of polyR := +#[export] Instance div_poly : div_of polyR := fun p q => (if (q == 0)%C then (0%C, 0%C, p) else div_rec_poly q 0%C 0%C p (spec (size_op p : N))).1.2. -Global Instance mod_poly : mod_of polyR := +#[export] Instance mod_poly : mod_of polyR := fun p q => (if (q == 0)%C then (0%C, 0%C, p) else div_rec_poly q 0%C 0%C p (spec (size_op p : N))).2. -Global Instance scal_poly : scal_of polyR N := +#[export] Instance scal_poly : scal_of polyR N := fun p q => (if (q == 0)%C then (0%C, 0%C, p) else div_rec_poly q 0%C 0%C p (spec (size_op p : N))).1.1. @@ -134,13 +134,13 @@ Context `{!refines (RpolyC ==> RpolyC ==> RpolyC) sub_poly sub_op}. Context `{!refines (RpolyC ==> RpolyC ==> bool_R) eqtype.eq_op eq_op}. Context `{!refines RpolyC 0%R 0%C}. -Global Instance RpolyC_div_poly : +#[export] Instance RpolyC_div_poly : refines (RpolyC ==> RpolyC ==> RpolyC) (div_poly (N:=nat) (R:=R) (polyR:={poly R})) (div_poly (N:=N) (R:=C) (polyR:=polyC)). Proof. param div_poly_R. Qed. -Global Instance refine_div_poly : +#[export] Instance refine_div_poly : refines (RpolyC ==> RpolyC ==> RpolyC) (@rdivp R) (div_poly (N:=N) (R:=C) (polyR:=polyC)). Proof. @@ -149,13 +149,13 @@ Proof. exact: refinesP. Qed. -Global Instance RpolyC_mod_poly : +#[export] Instance RpolyC_mod_poly : refines (RpolyC ==> RpolyC ==> RpolyC) (mod_poly (N:=nat) (R:=R) (polyR:={poly R})) (mod_poly (N:=N) (R:=C) (polyR:=polyC)). Proof. param mod_poly_R. Qed. -Global Instance refine_mod_poly : +#[export] Instance refine_mod_poly : refines (RpolyC ==> RpolyC ==> RpolyC) (@rmodp R) (mod_poly (N:=N) (R:=C) (polyR:=polyC)). Proof. @@ -164,7 +164,7 @@ Proof. exact: refinesP. Qed. -Global Instance RpolyC_scal_poly : +#[export] Instance RpolyC_scal_poly : refines (RpolyC ==> RpolyC ==> rN) (scal_poly (N:=nat) (R:=R) (polyR:={poly R})) (scal_poly (N:=N) (R:=C) (polyR:=polyC)). @@ -175,7 +175,7 @@ Proof. do ?eapply refines_apply; tc. Qed. -Global Instance refine_scal_poly : +#[export] Instance refine_scal_poly : refines (RpolyC ==> RpolyC ==> rN) (@rscalp R) (scal_poly (N:=N) (R:=C) (polyR:=polyC)). Proof. diff --git a/refinements/pos.v b/refinements/pos.v index cd0e458..d41dc60 100644 --- a/refinements/pos.v +++ b/refinements/pos.v @@ -40,18 +40,18 @@ Import Refinements.Op. Definition posS (n : nat) : pos := @pos_of n.+1 isT. -Global Instance pos1 : one_of pos := posS 0. -Global Instance add_pos : add_of pos := fun m n => insubd pos1 (val m + val n). -Global Instance sub_pos : sub_of pos := fun m n => insubd pos1 (val m - val n). -Global Instance mul_pos : mul_of pos := fun m n => insubd pos1 (val m * val n). -Global Instance exp_pos : exp_of pos pos := +#[export] Instance pos1 : one_of pos := posS 0. +#[export] Instance add_pos : add_of pos := fun m n => insubd pos1 (val m + val n). +#[export] Instance sub_pos : sub_of pos := fun m n => insubd pos1 (val m - val n). +#[export] Instance mul_pos : mul_of pos := fun m n => insubd pos1 (val m * val n). +#[export] Instance exp_pos : exp_of pos pos := fun m n => insubd pos1 (val m ^ val n). -Global Instance leq_pos : leq_of pos := fun m n => val m <= val n. -Global Instance lt_pos : lt_of pos := fun m n => val m < val n. -Global Instance eq_pos : eq_of pos := eqtype.eq_op. +#[export] Instance leq_pos : leq_of pos := fun m n => val m <= val n. +#[export] Instance lt_pos : lt_of pos := fun m n => val m < val n. +#[export] Instance eq_pos : eq_of pos := eqtype.eq_op. -Global Instance cast_pos_nat : cast_of pos nat := val. -Global Instance cast_nat_pos : cast_of nat pos := insubd 1%C. +#[export] Instance cast_pos_nat : cast_of pos nat := val. +#[export] Instance cast_nat_pos : cast_of nat pos := insubd 1%C. Local Open Scope ring_scope. Definition pos_to_int (p : pos) : int := (val p)%:R. diff --git a/refinements/rational.v b/refinements/rational.v index c8ff4a2..3413447 100644 --- a/refinements/rational.v +++ b/refinements/rational.v @@ -42,31 +42,31 @@ Context `{one_of P, sub_of P, add_of P, mul_of P, eq_of P, leq_of P, lt_of P}. Context `{cast_of P Z, cast_of Z P}. Context `{spec_of Z int, spec_of P pos, spec_of N nat}. -Global Instance zeroQ : zero_of Q := (0, 1). -Global Instance oneQ : one_of Q := (1, 1). -Global Instance addQ : add_of Q := fun x y => +#[export] Instance zeroQ : zero_of Q := (0, 1). +#[export] Instance oneQ : one_of Q := (1, 1). +#[export] Instance addQ : add_of Q := fun x y => (x.1 * cast y.2 + y.1 * cast x.2, x.2 * y.2). -Global Instance mulQ : mul_of Q := fun x y => (x.1 * y.1, x.2 * y.2). -Global Instance oppQ : opp_of Q := fun x => (- x.1, x.2). -Global Instance eqQ : eq_of Q := +#[export] Instance mulQ : mul_of Q := fun x y => (x.1 * y.1, x.2 * y.2). +#[export] Instance oppQ : opp_of Q := fun x => (- x.1, x.2). +#[export] Instance eqQ : eq_of Q := fun x y => (x.1 * cast y.2 == y.1 * cast x.2). -Global Instance leqQ : leq_of Q := +#[export] Instance leqQ : leq_of Q := fun x y => (x.1 * cast y.2 <= y.1 * cast x.2). -Global Instance ltQ : lt_of Q := +#[export] Instance ltQ : lt_of Q := fun x y => (x.1 * cast y.2 < y.1 * cast x.2). -Global Instance invQ : inv_of Q := fun x => +#[export] Instance invQ : inv_of Q := fun x => if (x.1 == 0)%C then 0 else if (0 < x.1) then (cast x.2, cast x.1) else (- (cast x.2), cast (- x.1)). -Global Instance subQ : sub_of Q := fun x y => (x + - y). -Global Instance divQ : div_of Q := fun x y => (x * y^-1). -Global Instance expQnat : exp_of Q N := fun x n => iter (spec n) (mulQ x) 1. -Global Instance specQ : spec_of Q rat := +#[export] Instance subQ : sub_of Q := fun x y => (x + - y). +#[export] Instance divQ : div_of Q := fun x y => (x * y^-1). +#[export] Instance expQnat : exp_of Q N := fun x n => iter (spec n) (mulQ x) 1. +#[export] Instance specQ : spec_of Q rat := fun q => (spec q.1)%:~R / (cast (spec q.2 : pos))%:R. (* Embedding from Z to Q *) -Global Instance cast_ZQ : cast_of Z Q := fun x => (x, 1). -Global Instance cast_PQ : cast_of P Q := fun x => cast (cast x : Z). +#[export] Instance cast_ZQ : cast_of Z Q := fun x => (x, 1). +#[export] Instance cast_PQ : cast_of P Q := fun x => cast (cast x : Z). End Q_ops. End Q. @@ -299,25 +299,25 @@ Context `{!refines (Rpos ==> Logic.eq) spec_id spec}. Context `{!refines (Rnat ==> nat_R) spec_id spec}. -Global Instance RratC_zeroQ : refines RratC 0 0%C. +#[export] Instance RratC_zeroQ : refines RratC 0 0%C. Proof. param_comp zeroQ_R. Qed. -Global Instance RratC_oneQ : refines RratC 1 1%C. +#[export] Instance RratC_oneQ : refines RratC 1 1%C. Proof. param_comp oneQ_R. Qed. -Global Instance RratC_cast_ZQ : refines (Rint ==> RratC) intr cast. +#[export] Instance RratC_cast_ZQ : refines (Rint ==> RratC) intr cast. Proof. param_comp cast_ZQ_R. Qed. -Global Instance RratC_cast_PQ : refines (Rpos ==> RratC) pos_to_rat cast. +#[export] Instance RratC_cast_PQ : refines (Rpos ==> RratC) pos_to_rat cast. Proof. param_comp cast_PQ_R. Qed. -Global Instance RratC_addQ : refines (RratC ==> RratC ==> RratC) +%R +%C. +#[export] Instance RratC_addQ : refines (RratC ==> RratC ==> RratC) +%R +%C. Proof. param_comp addQ_R. Qed. -Global Instance RratC_mulQ : refines (RratC ==> RratC ==> RratC) *%R *%C. +#[export] Instance RratC_mulQ : refines (RratC ==> RratC ==> RratC) *%R *%C. Proof. param_comp mulQ_R. Qed. -Global Instance RratC_expQnat : +#[export] Instance RratC_expQnat : refines (RratC ==> Rnat ==> RratC) (@GRing.exp _) exp_op. Proof. eapply refines_trans; tc. @@ -326,30 +326,30 @@ Proof. exact: refinesP. Qed. -Global Instance RratC_oppQ : refines (RratC ==> RratC) -%R -%C. +#[export] Instance RratC_oppQ : refines (RratC ==> RratC) -%R -%C. Proof. param_comp oppQ_R. Qed. -Global Instance RratC_invQ : refines (RratC ==> RratC) GRing.inv inv_op. +#[export] Instance RratC_invQ : refines (RratC ==> RratC) GRing.inv inv_op. Proof. param_comp invQ_R. Qed. -Global Instance RratC_subQ : +#[export] Instance RratC_subQ : refines (RratC ==> RratC ==> RratC) (fun x y => x - y) sub_op. Proof. param_comp subQ_R. Qed. -Global Instance RratC_divq : refines (RratC ==> RratC ==> RratC) divq div_op. +#[export] Instance RratC_divq : refines (RratC ==> RratC ==> RratC) divq div_op. Proof. param_comp divQ_R. Qed. -Global Instance RratC_eqQ : +#[export] Instance RratC_eqQ : refines (RratC ==> RratC ==> bool_R) eqtype.eq_op eq_op. Proof. param_comp eqQ_R. Qed. -Global Instance RratC_leqQ : refines (RratC ==> RratC ==> bool_R) Num.le leq_op. +#[export] Instance RratC_leqQ : refines (RratC ==> RratC ==> bool_R) Num.le leq_op. Proof. param_comp leqQ_R. Qed. -Global Instance RratC_ltQ : refines (RratC ==> RratC ==> bool_R) Num.lt lt_op. +#[export] Instance RratC_ltQ : refines (RratC ==> RratC ==> bool_R) Num.lt lt_op. Proof. param_comp ltQ_R. Qed. -Global Instance RratC_spec : refines (RratC ==> Logic.eq) spec_id spec. +#[export] Instance RratC_spec : refines (RratC ==> Logic.eq) spec_id spec. Proof. eapply refines_trans; tc. rewrite refinesE -[Rint]refinesE -[Rpos]refinesE; move=> x y rxy. diff --git a/refinements/refinements.v b/refinements/refinements.v index 4245307..a1debfc 100644 --- a/refinements/refinements.v +++ b/refinements/refinements.v @@ -31,13 +31,13 @@ Proof. by rewrite /refines unlock. Qed. Lemma refines_eq T (x y : T) : refines eq x y -> x = y. Proof. by rewrite refinesE. Qed. -Global Instance refines_bool_eq x y : refines bool_R x y -> refines eq x y. +#[export] Instance refines_bool_eq x y : refines bool_R x y -> refines eq x y. Proof. by rewrite !refinesE=> [[]]. Qed. Lemma nat_R_eq x y : nat_R x y -> x = y. Proof. by elim=> // m n _ ->. Qed. -Global Instance refines_nat_eq x y : refines nat_R x y -> refines eq x y. +#[export] Instance refines_nat_eq x y : refines nat_R x y -> refines eq x y. Proof. rewrite !refinesE; exact: nat_R_eq. Qed. Lemma refinesP T T' (R : T -> T' -> Type) (x : T) (y : T') : @@ -67,32 +67,32 @@ Lemma trivial_refines T T' (R : T -> T' -> Type) (x : T) (y : T') : R x y -> refines R x y. Proof. by rewrite refinesE. Qed. -Global Instance refines_apply +#[export] Instance refines_apply A B (R : A -> B -> Type) C D (R' : C -> D -> Type) : forall (c : A -> C) (d : B -> D), refines (R ==> R') c d -> forall (a : A) (b : B), refines R a b -> refines R' (c a) (d b) | 99. Proof. by rewrite !refinesE => c d rcd a b rab; apply: rcd. Qed. -Global Instance composable_rid1 A B (R : A -> B -> Type) : +#[export] Instance composable_rid1 A B (R : A -> B -> Type) : composable eq R R | 1. Proof. rewrite composableE; apply: eq_hrelRL. by split; [ apply: comp_eql | move=> x y hxy; exists x ]. Qed. -Global Instance composable_bool_id1 B (R : bool -> B -> Type) : +#[export] Instance composable_bool_id1 B (R : bool -> B -> Type) : composable bool_R R R | 1. Proof. by rewrite composableE => x y [y' [[]]]. Qed. -(* Global Instance composable_nat_id1 B (R : nat -> B -> Type) : +(* #[export] Instance composable_nat_id1 B (R : nat -> B -> Type) : composable nat_R R R | 1. *) (* Proof. by rewrite composableE => x y [y' [/nat_R_eq ->]]. Qed. *) -Global Instance composable_comp A B C (rAB : A -> B -> Type) +#[export] Instance composable_comp A B C (rAB : A -> B -> Type) (rBC : B -> C -> Type) : composable rAB rBC (rAB \o rBC). Proof. by rewrite composableE. Qed. -Global Instance composable_imply A B C A' B' C' +#[export] Instance composable_imply A B C A' B' C' (rAB : A -> B -> Type) (rBC : B -> C -> Type) (R1 : A' -> B' -> Type) (R2 : B' -> C' -> Type) (R3 : A' -> C' -> Type) : composable R1 R2 R3 -> composable (rAB ==> R1) (rBC ==> R2) (rAB \o rBC ==> R3) | 0. @@ -101,7 +101,7 @@ rewrite !composableE => R123 fA fC [fB [RfAB RfBC]] a c [b [rABab rBCbc]]. apply: R123; exists (fB b); split; [ exact: RfAB | exact: RfBC ]. Qed. -Global Instance composable_imply_id1 A B A' B' C' +#[export] Instance composable_imply_id1 A B A' B' C' (rAB : A -> B -> Type) (R1 : A' -> B' -> Type) (R2 : B' -> C' -> Type) (R3 : A' -> C' -> Type) : composable R1 R2 R3 -> composable (eq ==> R1) (rAB ==> R2) (rAB ==> R3) | 1. @@ -123,7 +123,7 @@ Lemma refines_prod_R A A' B B' (rA : A -> A' -> Type) (rB : B -> B' -> Type) x y refines rA x.1 y.1 -> refines rB x.2 y.2 -> refines (prod_R rA rB) x y. Proof. by rewrite !refinesE => *; apply: prod_RI; split. Qed. -Global Instance composable_prod A A' B B' C C' +#[export] Instance composable_prod A A' B B' C C' (rAB : A -> B -> Type) (rAB' : A' -> B' -> Type) (rBC : B -> C -> Type) (rBC' : B' -> C' -> Type) (rAC : A -> C -> Type) (rAC' : A' -> C' -> Type) : @@ -173,25 +173,25 @@ Lemma refines_abstr2 A B A' B' A'' B'' refines (R ==> R' ==> R'') f g. Proof. by move=> H; do 2![eapply refines_abstr => *]; apply: H. Qed. -Global Instance refines_pair_R +#[export] Instance refines_pair_R A A' B B' (rA : A -> A' -> Type) (rB : B -> B' -> Type) : refines (rA ==> rB ==> prod_R rA rB)%rel (@pair _ _) (@pair _ _). Proof. by rewrite refinesE. Qed. -Global Instance refines_fst_R +#[export] Instance refines_fst_R A A' B B' (rA : A -> A' -> Type) (rB : B -> B' -> Type) : refines (prod_R rA rB ==> rA)%rel (@fst _ _) (@fst _ _). Proof. by rewrite !refinesE=> [??] [??]. Qed. -Global Instance refines_snd_R +#[export] Instance refines_snd_R A A' B B' (rA : A -> A' -> Type) (rB : B -> B' -> Type) : refines (prod_R rA rB ==> rB)%rel (@snd _ _) (@snd _ _). Proof. by rewrite !refinesE=> [??] [??]. Qed. Class unify A (x y : A) := unify_rel : x = y. -Global Instance unifyxx A (x : A) : unify x x := erefl. +#[export] Instance unifyxx A (x : A) : unify x x := erefl. -Global Instance refines_of_unify A x y : unify x y -> refines (@unify A) x y | 100. +#[export] Instance refines_of_unify A x y : unify x y -> refines (@unify A) x y | 100. Proof. by rewrite refinesE. Qed. Lemma refines_comp_unify A B (R : A -> B -> Type) x y : @@ -225,34 +225,34 @@ Ltac param x := (* Special tactic when relation is defined using \o *) Ltac param_comp x := eapply refines_trans; tc; param x. -Global Instance refines_true : refines _ _ _ := +#[export] Instance refines_true : refines _ _ _ := trivial_refines bool_R_true_R. -Global Instance refines_false : refines _ _ _ := +#[export] Instance refines_false : refines _ _ _ := trivial_refines bool_R_false_R. -Global Instance refines_negb : refines (bool_R ==> bool_R) negb negb. +#[export] Instance refines_negb : refines (bool_R ==> bool_R) negb negb. Proof. exact/trivial_refines/negb_R. Qed. -Global Instance refines_implb : refines (bool_R ==> bool_R ==> bool_R) implb implb. +#[export] Instance refines_implb : refines (bool_R ==> bool_R ==> bool_R) implb implb. Proof. exact/trivial_refines/implb_R. Qed. -Global Instance refines_andb : refines (bool_R ==> bool_R ==> bool_R) andb andb. +#[export] Instance refines_andb : refines (bool_R ==> bool_R ==> bool_R) andb andb. Proof. exact/trivial_refines/andb_R. Qed. -Global Instance refines_orb : refines (bool_R ==> bool_R ==> bool_R) orb orb. +#[export] Instance refines_orb : refines (bool_R ==> bool_R ==> bool_R) orb orb. Proof. exact/trivial_refines/orb_R. Qed. -Global Instance refines_addb : refines (bool_R ==> bool_R ==> bool_R) addb addb. +#[export] Instance refines_addb : refines (bool_R ==> bool_R ==> bool_R) addb addb. Proof. exact/trivial_refines/addb_R. Qed. -Global Instance refines_eqb : refines (bool_R ==> bool_R ==> bool_R) eqtype.eq_op eqtype.eq_op. +#[export] Instance refines_eqb : refines (bool_R ==> bool_R ==> bool_R) eqtype.eq_op eqtype.eq_op. Proof. exact/trivial_refines/eqb_R. Qed. Lemma refines_goal (G G' : Type) : refines (fun T T' => T' -> T) G G' -> G' -> G. Proof. by rewrite refinesE. Qed. -Global Instance refines_leibniz_eq (T : eqType) (x y : T) b : +#[export] Instance refines_leibniz_eq (T : eqType) (x y : T) b : refines bool_R (x == y) b -> refines (fun T' T => T -> T') (x = y) b. Proof. by move=> /refines_bool_eq; rewrite !refinesE => <- /eqP. Qed. @@ -377,7 +377,7 @@ Class native_compute T (x y : T) := NativeCompute : x = y. #[export] Hint Extern 0 (native_compute _ _) => context [(X in native_compute X)] native_compute; reflexivity : typeclass_instances. -#[global] +#[export] Instance strategy_class_native_compute : strategy_class native_compute := erefl. Class vm_compute T (x y : T) := VmCompute : x = y. @@ -385,7 +385,7 @@ Class vm_compute T (x y : T) := VmCompute : x = y. #[export] Hint Extern 0 (vm_compute _ _) => context [(X in vm_compute X)] vm_compute; reflexivity : typeclass_instances. -#[global] +#[export] Instance strategy_class_vm_compute : strategy_class vm_compute := erefl. Class compute T (x y : T) := Compute : x = y. @@ -393,14 +393,14 @@ Class compute T (x y : T) := Compute : x = y. #[export] Hint Extern 0 (compute _ _) => context [(X in compute X)] compute; reflexivity : typeclass_instances. -#[global] Instance strategy_class_compute : strategy_class compute := erefl. +#[export] Instance strategy_class_compute : strategy_class compute := erefl. Class simpl T (x y : T) := Simpl : x = y. #[export] Hint Mode simpl - + - : typeclass_instances. #[export] Hint Extern 0 (simpl _ _) => context [(X in simpl X)] simpl; reflexivity : typeclass_instances. -#[global] Instance strategy_class_simpl : strategy_class simpl := erefl. +#[export] Instance strategy_class_simpl : strategy_class simpl := erefl. Lemma coqeal_eq C {eqC : strategy_class C} {T T'} spec (x x' : T) {y y' : T'} {rxy : refines eq (spec_id x) (spec y)} {ry : C _ y y'} @@ -448,7 +448,7 @@ Proof. by []. Qed. (** Automation: for proving refinement lemmas involving options, do [rewrite !optionE; refines_apply]. *) -Global Instance refines_option +#[export] Instance refines_option (A B : Type) (rA : A -> A -> Type) (rB : B -> B -> Type) : refines ((rA ==> rB) ==> rB ==> option_R rA ==> rB) (@oapp _ _) (@oapp _ _). Proof. diff --git a/refinements/seqmx.v b/refinements/seqmx.v index 8df945e..d127e4c 100644 --- a/refinements/seqmx.v +++ b/refinements/seqmx.v @@ -121,16 +121,16 @@ Definition mkseqmx_ord m n (f : 'I_m -> 'I_n -> A) : seqmx := let enum_n := ord_enum_eq n in map (fun i => map (f i) enum_n) (ord_enum_eq m). -Global Instance const_seqmx : const_mx_of A hseqmx := +#[export] Instance const_seqmx : const_mx_of A hseqmx := fun m n (x : A) => nseq m (nseq n x). -Global Instance map_seqmx : map_mx_of A B seqmx seqmx := +#[export] Instance map_seqmx : map_mx_of A B seqmx seqmx := fun (f : A -> B) (M : seqmx) => map (map f) M. Definition zipwith_seqmx (f : A -> A -> A) (M N : seqmx) := zipwith (zipwith f) M N. -Global Instance seqmx0 : hzero_of hseqmx := +#[export] Instance seqmx0 : hzero_of hseqmx := fun m n => const_seqmx m n 0%C. Definition diag_seqmx (s : seqmx) := @@ -139,25 +139,25 @@ Definition diag_seqmx (s : seqmx) := Definition scalar_seqmx m (x : A) := diag_seqmx (const_seqmx 1%N m x). -Global Instance seqmx1 m : one_of seqmx := scalar_seqmx m 1%C. +#[export] Instance seqmx1 m : one_of seqmx := scalar_seqmx m 1%C. -Global Instance opp_seqmx : opp_of (@seqmx A) := map (map -%C). +#[export] Instance opp_seqmx : opp_of (@seqmx A) := map (map -%C). -Global Instance add_seqmx : add_of seqmx := zipwith_seqmx +%C. +#[export] Instance add_seqmx : add_of seqmx := zipwith_seqmx +%C. (* TODO: Implement better *) -Global Instance sub_seqmx : sub_of (@seqmx A) := fun a b => (a + - b)%C. +#[export] Instance sub_seqmx : sub_of (@seqmx A) := fun a b => (a + - b)%C. Definition trseqmx m n (M : @hseqmx A m n) := if eqn m 0 then nseq n [::] else foldr (zipwith cons) (nseq n [::]) M. -Global Instance mul_seqmx : @hmul_of nat hseqmx := +#[export] Instance mul_seqmx : @hmul_of nat hseqmx := fun _ n p M N => let N := trseqmx N in if n is O then seqmx0 (size M) p else map (fun r => map (foldl2 (fun z x y => (x * y) + z) 0 r)%C N) M. -Global Instance scale_seqmx : scale_of A seqmx := +#[export] Instance scale_seqmx : scale_of A seqmx := fun x M => map (map (mul_op x)) M. (* Inlining of && should provide lazyness here. *) @@ -168,46 +168,46 @@ Fixpoint eq_seq T f (s1 s2 : seq T) := | _, _ => false end. -Global Instance eq_seqmx : eq_of (@seqmx A) := eq_seq (eq_seq eq_op). +#[export] Instance eq_seqmx : eq_of (@seqmx A) := eq_seq (eq_seq eq_op). -Global Instance top_left_seqmx : top_left_of seqmx A := +#[export] Instance top_left_seqmx : top_left_of seqmx A := fun (M : seqmx) => nth 0%C (nth [::] M 0) 0. -Global Instance usubseqmx : usubmx_of hseqmx := +#[export] Instance usubseqmx : usubmx_of hseqmx := fun m1 m2 n (M : @seqmx A) => take m1 M. -Global Instance dsubseqmx : dsubmx_of hseqmx := +#[export] Instance dsubseqmx : dsubmx_of hseqmx := fun m1 m2 n (M : @seqmx A) => drop m1 M. -Global Instance lsubseqmx : lsubmx_of hseqmx := +#[export] Instance lsubseqmx : lsubmx_of hseqmx := fun m n1 n2 (M : @seqmx A) => map (take n1) M. -Global Instance rsubseqmx : rsubmx_of hseqmx := +#[export] Instance rsubseqmx : rsubmx_of hseqmx := fun m n1 n2 (M : @seqmx A) => map (drop n1) M. -Global Instance ulsubseqmx : ulsubmx_of hseqmx := +#[export] Instance ulsubseqmx : ulsubmx_of hseqmx := fun m1 m2 n1 n2 (M : hseqmx (m1 + m2)%N (n1 + n2)%N) => lsubseqmx (usubseqmx M). -Global Instance ursubseqmx : ursubmx_of hseqmx := +#[export] Instance ursubseqmx : ursubmx_of hseqmx := fun m1 m2 n1 n2 (M : hseqmx (m1 + m2)%N (n1 + n2)%N) => rsubseqmx (usubseqmx M). -Global Instance dlsubseqmx : dlsubmx_of hseqmx := +#[export] Instance dlsubseqmx : dlsubmx_of hseqmx := fun m1 m2 n1 n2 (M : hseqmx (m1 + m2)%N (n1 + n2)%N) => lsubseqmx (dsubseqmx M). -Global Instance drsubseqmx : drsubmx_of hseqmx := +#[export] Instance drsubseqmx : drsubmx_of hseqmx := fun m1 m2 n1 n2 (M : hseqmx (m1 + m2)%N (n1 + n2)%N) => rsubseqmx (dsubseqmx M). -Global Instance row_seqmx : row_mx_of hseqmx := +#[export] Instance row_seqmx : row_mx_of hseqmx := fun m n1 n2 (M N : @seqmx A) => zipwith cat M N. -Global Instance col_seqmx : col_mx_of hseqmx := +#[export] Instance col_seqmx : col_mx_of hseqmx := fun m1 m2 n (M N : @seqmx A) => M ++ N. -Global Instance block_seqmx : block_mx_of hseqmx := +#[export] Instance block_seqmx : block_mx_of hseqmx := fun m1 m2 n1 n2 Aul Aur Adl Adr => col_seqmx (row_seqmx Aul Aur) (row_seqmx Adl Adr). @@ -274,7 +274,7 @@ Context `{zero_of R}. Context (C : Type). Context `{spec_of C R}. -Global Instance spec_seqmx m n : spec_of (@seqmx C) 'M[R]_(m, n) := +#[export] Instance spec_seqmx m n : spec_of (@seqmx C) 'M[R]_(m, n) := fun s => \matrix_(i, j) nth 0%C (nth [::] (map_seqmx spec s) i) j. End seqmx_more_op. @@ -647,7 +647,7 @@ Proof. by rewrite refinesE=> _ x -> _ y ->. Qed. -Global Instance RseqmxC_seqmx_of_fun m1 m2 (rm : nat_R m1 m2) n1 n2 +#[export] Instance RseqmxC_seqmx_of_fun m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) f g `{forall x y, refines (rI rm) x y -> forall z t, refines (rI rn) z t -> @@ -662,7 +662,7 @@ Proof. eapply refines_comp_unify; tc. Qed. -Global Instance refine_seqmx_of_fun m n f g +#[export] Instance refine_seqmx_of_fun m n f g `{forall x y, refines (rI (nat_Rxx m)) x y -> forall z t, refines (rI (nat_Rxx n)) z t -> refines (rAC \o (@unify _)) (f x z) (g y t)} : @@ -670,177 +670,177 @@ Global Instance refine_seqmx_of_fun m n f g (\matrix_(i, j) f i j) (seqmx_of_fun (I:=I) g). Proof. exact: RseqmxC_seqmx_of_fun. Qed. -Global Instance RseqmxC_mkseqmx_ord m1 m2 (rm : nat_R m1 m2) n1 n2 +#[export] Instance RseqmxC_mkseqmx_ord m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines ((eq ==> eq ==> rAC) ==> RseqmxC rm rn) (matrix_of_fun matrix_key) (@mkseqmx_ord C m1 n1). Proof. param_comp mkseqmx_ord_R. Qed. -Global Instance refine_mkseqmx_ord m n : +#[export] Instance refine_mkseqmx_ord m n : refines ((eq ==> eq ==> rAC) ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) (matrix_of_fun matrix_key) (@mkseqmx_ord C m n). Proof. exact: RseqmxC_mkseqmx_ord. Qed. -Global Instance RseqmxC_const_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 +#[export] Instance RseqmxC_const_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (rAC ==> RseqmxC rm rn) (@matrix.const_mx R m1 n1) (const_seqmx m2 n2). Proof. param_comp const_seqmx_R. Qed. -Global Instance refine_const_seqmx m n : +#[export] Instance refine_const_seqmx m n : refines (rAC ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) (@matrix.const_mx R m n) (const_seqmx m n). Proof. exact: RseqmxC_const_seqmx. Qed. -Global Instance RseqmxC_0 m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : +#[export] Instance RseqmxC_0 m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC rm rn) (const_mx 0%C) (@hzero_op _ _ _ m2 n2). Proof. param_comp seqmx0_R. Qed. -Global Instance refine_0_seqmx m n : +#[export] Instance refine_0_seqmx m n : refines (RseqmxC (nat_Rxx m) (nat_Rxx n)) (const_mx 0%C) (@hzero_op _ _ _ m n). Proof. exact: RseqmxC_0. Qed. -Global Instance RseqmxC_top_left_seqmx m1 m2 (rm : nat_R m1 m2) : +#[export] Instance RseqmxC_top_left_seqmx m1 m2 (rm : nat_R m1 m2) : refines (RseqmxC (nat_R_S_R rm) (nat_R_S_R rm) ==> rAC) (fun M => M ord0 ord0) (@top_left_seqmx C _). Proof. param_comp top_left_seqmx_R. Qed. -Global Instance refine_top_left_seqmx m : +#[export] Instance refine_top_left_seqmx m : refines (RseqmxC (nat_R_S_R (nat_Rxx m)) (nat_R_S_R (nat_Rxx m)) ==> rAC) (fun M => M ord0 ord0) (@top_left_seqmx C _). Proof. exact: RseqmxC_top_left_seqmx. Qed. -Global Instance RseqmxC_usubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 +#[export] Instance RseqmxC_usubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC (addn_R rm1 rm2) rn ==> RseqmxC rm1 rn) (@matrix.usubmx R m11 m21 n1) (@usubseqmx C m12 m22 n2). Proof. param_comp usubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_usubseqmx m1 m2 n : +#[export] Instance refine_usubseqmx m1 m2 n : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) (nat_Rxx n) ==> RseqmxC (nat_Rxx m1) (nat_Rxx n)) (@matrix.usubmx R m1 m2 n) (@usubseqmx C m1 m2 n). Proof. exact: RseqmxC_usubseqmx. Qed. -Global Instance RseqmxC_dsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 +#[export] Instance RseqmxC_dsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC (addn_R rm1 rm2) rn ==> RseqmxC rm2 rn) (@matrix.dsubmx R m11 m21 n1) (@dsubseqmx C m12 m22 n2). Proof. param_comp dsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_dsubseqmx m1 m2 n : +#[export] Instance refine_dsubseqmx m1 m2 n : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) (nat_Rxx n) ==> RseqmxC (nat_Rxx m2) (nat_Rxx n)) (@matrix.dsubmx R m1 m2 n) (@dsubseqmx C m1 m2 n). Proof. exact: RseqmxC_dsubseqmx. Qed. -Global Instance RseqmxC_lsubseqmx m1 m2 (rm : nat_R m1 m2) n11 n12 +#[export] Instance RseqmxC_lsubseqmx m1 m2 (rm : nat_R m1 m2) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC rm (addn_R rn1 rn2) ==> RseqmxC rm rn1) (@matrix.lsubmx R m1 n11 n21) (@lsubseqmx C m2 n12 n22). Proof. param_comp lsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_lsubseqmx m n1 n2 : +#[export] Instance refine_lsubseqmx m n1 n2 : refines (RseqmxC (nat_Rxx m) (addn_R (nat_Rxx n1) (nat_Rxx n2)) ==> RseqmxC (nat_Rxx m) (nat_Rxx n1)) (@matrix.lsubmx R m n1 n2) (@lsubseqmx C m n1 n2). Proof. exact: RseqmxC_lsubseqmx. Qed. -Global Instance RseqmxC_rsubseqmx m1 m2 (rm : nat_R m1 m2) n11 n12 +#[export] Instance RseqmxC_rsubseqmx m1 m2 (rm : nat_R m1 m2) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC rm (addn_R rn1 rn2) ==> RseqmxC rm rn2) (@matrix.rsubmx R m1 n11 n21) (@rsubseqmx C m2 n12 n22). Proof. param_comp rsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_rsubseqmx m n1 n2 : +#[export] Instance refine_rsubseqmx m n1 n2 : refines (RseqmxC (nat_Rxx m) (addn_R (nat_Rxx n1) (nat_Rxx n2)) ==> RseqmxC (nat_Rxx m) (nat_Rxx n2)) (@matrix.rsubmx R m n1 n2) (@rsubseqmx C m n1 n2). Proof. exact: RseqmxC_rsubseqmx. Qed. -Global Instance RseqmxC_ulsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 +#[export] Instance RseqmxC_ulsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC (addn_R rm1 rm2) (addn_R rn1 rn2) ==> RseqmxC rm1 rn1) (@matrix.ulsubmx R m11 m21 n11 n21) (@ulsubseqmx C m12 m22 n12 n22). Proof. param_comp ulsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_ulsubseqmx m1 m2 n1 n2 : +#[export] Instance refine_ulsubseqmx m1 m2 n1 n2 : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) (addn_R (nat_Rxx n1) (nat_Rxx n2)) ==> RseqmxC (nat_Rxx m1) (nat_Rxx n1)) (@matrix.ulsubmx R m1 m2 n1 n2) (@ulsubseqmx C m1 m2 n1 n2). Proof. exact: RseqmxC_ulsubseqmx. Qed. -Global Instance RseqmxC_ursubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 +#[export] Instance RseqmxC_ursubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC (addn_R rm1 rm2) (addn_R rn1 rn2) ==> RseqmxC rm1 rn2) (@matrix.ursubmx R m11 m21 n11 n21) (@ursubseqmx C m12 m22 n12 n22). Proof. param_comp ursubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_ursubseqmx m1 m2 n1 n2 : +#[export] Instance refine_ursubseqmx m1 m2 n1 n2 : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) (addn_R (nat_Rxx n1) (nat_Rxx n2)) ==> RseqmxC (nat_Rxx m1) (nat_Rxx n2)) (@matrix.ursubmx R m1 m2 n1 n2) (@ursubseqmx C m1 m2 n1 n2). Proof. exact: RseqmxC_ursubseqmx. Qed. -Global Instance RseqmxC_dlsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 +#[export] Instance RseqmxC_dlsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC (addn_R rm1 rm2) (addn_R rn1 rn2) ==> RseqmxC rm2 rn1) (@matrix.dlsubmx R m11 m21 n11 n21) (@dlsubseqmx C m12 m22 n12 n22). Proof. param_comp dlsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_dlsubseqmx m1 m2 n1 n2 : +#[export] Instance refine_dlsubseqmx m1 m2 n1 n2 : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) (addn_R (nat_Rxx n1) (nat_Rxx n2)) ==> RseqmxC (nat_Rxx m2) (nat_Rxx n1)) (@matrix.dlsubmx R m1 m2 n1 n2) (@dlsubseqmx C m1 m2 n1 n2). Proof. exact: RseqmxC_dlsubseqmx. Qed. -Global Instance RseqmxC_drsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 +#[export] Instance RseqmxC_drsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC (addn_R rm1 rm2) (addn_R rn1 rn2) ==> RseqmxC rm2 rn2) (@matrix.drsubmx R m11 m21 n11 n21) (@drsubseqmx C m12 m22 n12 n22). Proof. param_comp drsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_drsubseqmx m1 m2 n1 n2 : +#[export] Instance refine_drsubseqmx m1 m2 n1 n2 : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) (addn_R (nat_Rxx n1) (nat_Rxx n2)) ==> RseqmxC (nat_Rxx m2) (nat_Rxx n2)) (@matrix.drsubmx R m1 m2 n1 n2) (@drsubseqmx C m1 m2 n1 n2). Proof. exact: RseqmxC_drsubseqmx. Qed. -Global Instance RseqmxC_row_seqmx m1 m2 (rm : nat_R m1 m2) n11 n12 +#[export] Instance RseqmxC_row_seqmx m1 m2 (rm : nat_R m1 m2) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC rm rn1 ==> RseqmxC rm rn2 ==> RseqmxC rm (addn_R rn1 rn2)) (@matrix.row_mx R m1 n11 n21) (@row_seqmx C m2 n12 n22). Proof. param_comp row_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_row_seqmx m n1 n2 : +#[export] Instance refine_row_seqmx m n1 n2 : refines (RseqmxC (nat_Rxx m) (nat_Rxx n1) ==> RseqmxC (nat_Rxx m) (nat_Rxx n2) ==> RseqmxC (nat_Rxx m) (addn_R (nat_Rxx n1) (nat_Rxx n2))) (@matrix.row_mx R m n1 n2) (@row_seqmx C m n1 n2). Proof. exact: RseqmxC_row_seqmx. Qed. -Global Instance RseqmxC_col_seqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 +#[export] Instance RseqmxC_col_seqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC rm1 rn ==> RseqmxC rm2 rn ==> RseqmxC (addn_R rm1 rm2) rn) (@matrix.col_mx R m11 m21 n1) (@col_seqmx C m12 m22 n2). Proof. param_comp col_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_col_seqmx m1 m2 n : +#[export] Instance refine_col_seqmx m1 m2 n : refines (RseqmxC (nat_Rxx m1) (nat_Rxx n) ==> RseqmxC (nat_Rxx m2) (nat_Rxx n) ==> RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) (nat_Rxx n)) (@matrix.col_mx R m1 m2 n) (@col_seqmx C m1 m2 n). Proof. exact: RseqmxC_col_seqmx. Qed. -Global Instance RseqmxC_block_seqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 +#[export] Instance RseqmxC_block_seqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC rm1 rn1 ==> RseqmxC rm1 rn2 ==> RseqmxC rm2 rn1 ==> @@ -848,7 +848,7 @@ Global Instance RseqmxC_block_seqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (@matrix.block_mx R m11 m21 n11 n21) (@block_seqmx C m12 m22 n12 n22). Proof. param_comp block_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_block_seqmx m1 m2 n1 n2 : +#[export] Instance refine_block_seqmx m1 m2 n1 n2 : refines (RseqmxC (nat_Rxx m1) (nat_Rxx n1) ==> RseqmxC (nat_Rxx m1) (nat_Rxx n2) ==> RseqmxC (nat_Rxx m2) (nat_Rxx n1) ==> @@ -858,11 +858,11 @@ Global Instance refine_block_seqmx m1 m2 n1 n2 : (@matrix.block_mx R m1 m2 n1 n2) (@block_seqmx C m1 m2 n1 n2). Proof. exact: RseqmxC_block_seqmx. Qed. -Global Instance RseqmxC_tr m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : +#[export] Instance RseqmxC_tr m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC rm rn ==> RseqmxC rn rm) trmx (@trseqmx C m2 n2). Proof. param_comp trseqmx_R. Qed. -Global Instance refine_trseqmx m n : +#[export] Instance refine_trseqmx m n : refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx n) (nat_Rxx m)) trmx (@trseqmx C m n). Proof. exact: RseqmxC_tr. Qed. @@ -874,8 +874,8 @@ Section seqmx_ring. Variable R : ringType. -(* The "Global" is needed for lemma RseqmxC_char_poly_mx below. *) -Global Instance zeroR : zero_of R := 0%R. +(* The "#[export]" is needed for lemma RseqmxC_char_poly_mx below. *) +#[export] Instance zeroR : zero_of R := 0%R. Local Instance oneR : one_of R := 1%R. Local Instance oppR : opp_of R := -%R. Local Instance addR : add_of R := +%R. @@ -1131,94 +1131,94 @@ Context `{forall n1 n2 (rn : nat_R n1 n2), Notation RseqmxC := (RseqmxC rAC). -Global Instance RseqmxC_diag_seqmx m1 m2 (rm : nat_R m1 m2) : +#[export] Instance RseqmxC_diag_seqmx m1 m2 (rm : nat_R m1 m2) : refines (RseqmxC (nat_R_S_R nat_R_O_R) rm ==> RseqmxC rm rm) diag_mx (diag_seqmx (A:=C)). Proof. param_comp diag_seqmx_R. Qed. -Global Instance refine_diag_seqmx m : +#[export] Instance refine_diag_seqmx m : refines (RseqmxC (nat_R_S_R nat_R_O_R) (nat_Rxx m) ==> RseqmxC (nat_Rxx m) (nat_Rxx m)) diag_mx (diag_seqmx (A:=C)). Proof. exact: RseqmxC_diag_seqmx. Qed. -Global Instance RseqmxC_scalar_seqmx m1 m2 (rm : nat_R m1 m2) : +#[export] Instance RseqmxC_scalar_seqmx m1 m2 (rm : nat_R m1 m2) : refines (rAC ==> RseqmxC rm rm) scalar_mx (scalar_seqmx m2). Proof. param_comp scalar_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_scalar_seqmx m : +#[export] Instance refine_scalar_seqmx m : refines (rAC ==> RseqmxC (nat_Rxx m) (nat_Rxx m)) scalar_mx (scalar_seqmx m). Proof. exact: RseqmxC_scalar_seqmx. Qed. -Global Instance RseqmxC_1 m1 m2 (rm : nat_R m1 m2) : +#[export] Instance RseqmxC_1 m1 m2 (rm : nat_R m1 m2) : refines (RseqmxC rm rm) 1%:M (seqmx1 m2). Proof. param_comp seqmx1_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_1_seqmx m : +#[export] Instance refine_1_seqmx m : refines (RseqmxC (nat_Rxx m) (nat_Rxx m)) 1%:M (seqmx1 m). Proof. exact: RseqmxC_1. Qed. -Global Instance RseqmxC_opp m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : +#[export] Instance RseqmxC_opp m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC rm rn ==> RseqmxC rm rn) -%R -%C. Proof. param_comp opp_seqmx_R. Qed. -Global Instance refine_opp_seqmx m n : +#[export] Instance refine_opp_seqmx m n : refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) -%R -%C. Proof. exact: RseqmxC_opp. Qed. -Global Instance RseqmxC_add m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : +#[export] Instance RseqmxC_add m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC rm rn ==> RseqmxC rm rn ==> RseqmxC rm rn) +%R +%C. Proof. param_comp add_seqmx_R. Qed. -Global Instance refine_add_seqmx m n : +#[export] Instance refine_add_seqmx m n : refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) +%R +%C. Proof. exact: RseqmxC_add. Qed. -Global Instance RseqmxC_sub m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : +#[export] Instance RseqmxC_sub m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC rm rn ==> RseqmxC rm rn ==> RseqmxC rm rn) (fun M N => M - N) sub_op. Proof. param_comp sub_seqmx_R. Qed. -Global Instance refine_sub_seqmx m n : +#[export] Instance refine_sub_seqmx m n : refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) (fun M N => M - N) sub_op. Proof. exact: RseqmxC_sub. Qed. -Global Instance RseqmxC_mul m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) +#[export] Instance RseqmxC_mul m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) p1 p2 (rp : nat_R p1 p2) : refines (RseqmxC rm rn ==> RseqmxC rn rp ==> RseqmxC rm rp) mulmx (@hmul_op _ _ _ m2 n2 p2). Proof. param_comp mul_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_mul_seqmx m n p : +#[export] Instance refine_mul_seqmx m n p : refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx n) (nat_Rxx p) ==> RseqmxC (nat_Rxx m) (nat_Rxx p)) mulmx (@hmul_op _ _ _ m n p). Proof. exact: RseqmxC_mul. Qed. -Global Instance RseqmxC_scale m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) +#[export] Instance RseqmxC_scale m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (rAC ==> RseqmxC rm rn ==> RseqmxC rm rn) *:%R *:%C. Proof. param_comp scale_seqmx_R. Qed. -Global Instance refine_scale_seqmx m n : +#[export] Instance refine_scale_seqmx m n : refines (rAC ==> RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) *:%R *:%C. Proof. exact: RseqmxC_scale. Qed. -Global Instance RseqmxC_eq m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : +#[export] Instance RseqmxC_eq m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC rm rn ==> RseqmxC rm rn ==> bool_R) eqtype.eq_op eq_op. Proof. param_comp eq_seqmx_R. Qed. -Global Instance refine_eq_seqmx m n : +#[export] Instance refine_eq_seqmx m n : refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n) ==> bool_R) eqtype.eq_op eq_op. Proof. exact: RseqmxC_eq. Qed. -Global Instance RseqmxC_delta_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 +#[export] Instance RseqmxC_delta_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) (i1 : 'I_m1) (i2 : 'I_m2) (ri : nat_R i1 i2) (j1 : 'I_n1) (j2 : 'I_n2) (rj : nat_R j1 j2) : refines (RseqmxC rm rn) (delta_mx i1 j1) (delta_seqmx (A:=C) m2 n2 i2 j2). @@ -1228,21 +1228,21 @@ Proof. rewrite refinesE; eapply delta_seqmx_R; try exact: refinesP; apply nat_Rxx. Qed. -Global Instance refine_delta_seqmx m n i j : +#[export] Instance refine_delta_seqmx m n i j : refines (RseqmxC (nat_Rxx m) (nat_Rxx n)) (delta_mx i j) (delta_seqmx m n i j). Proof. apply RseqmxC_delta_seqmx; exact: nat_Rxx. Qed. -Global Instance RseqmxC_trace_seqmx m1 m2 (rm : nat_R m1 m2) : +#[export] Instance RseqmxC_trace_seqmx m1 m2 (rm : nat_R m1 m2) : refines (RseqmxC rm rm ==> rAC) mxtrace (trace_seqmx (A:=C) (m:=m2)). Proof. param_comp trace_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. -Global Instance refine_trace_seqmx m : +#[export] Instance refine_trace_seqmx m : refines (RseqmxC (nat_Rxx m) (nat_Rxx m) ==> rAC) mxtrace (trace_seqmx (A:=C) (m:=m)). Proof. exact: RseqmxC_trace_seqmx. Qed. -Global Instance RseqmxC_pid_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 +#[export] Instance RseqmxC_pid_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) r1 r2 (rr : nat_R r1 r2) : refines (RseqmxC rm rn) (pid_mx r1) (pid_seqmx m2 n2 r2). Proof. @@ -1251,11 +1251,11 @@ Proof. rewrite refinesE; eapply pid_seqmx_R; try exact: refinesP; apply nat_Rxx. Qed. -Global Instance refine_pid_seqmx m n r : +#[export] Instance refine_pid_seqmx m n r : refines (RseqmxC (nat_Rxx m) (nat_Rxx n)) (pid_mx r) (pid_seqmx m n r). Proof. apply RseqmxC_pid_seqmx; exact: nat_Rxx. Qed. -Global Instance RseqmxC_copid_seqmx m1 m2 (rm : nat_R m1 m2) r1 r2 +#[export] Instance RseqmxC_copid_seqmx m1 m2 (rm : nat_R m1 m2) r1 r2 (rr : nat_R r1 r2) : refines (RseqmxC rm rm) (copid_mx r1) (copid_seqmx m2 r2). Proof. @@ -1265,11 +1265,11 @@ Proof. eapply copid_seqmx_R=> *; try exact: refinesP; apply nat_Rxx. Qed. -Global Instance refine_copid_seqmx m r : +#[export] Instance refine_copid_seqmx m r : refines (RseqmxC (nat_Rxx m) (nat_Rxx m)) (copid_mx r) (copid_seqmx m r). Proof. apply RseqmxC_copid_seqmx; exact: nat_Rxx. Qed. -Global Instance RseqmxC_spec m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : +#[export] Instance RseqmxC_spec m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC rm rn ==> Logic.eq) spec_id spec. Proof. eapply refines_trans; tc. @@ -1283,7 +1283,7 @@ Proof. by []. Qed. -Global Instance refine_spec_seqmx m n : +#[export] Instance refine_spec_seqmx m n : refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> Logic.eq) spec_id spec. Proof. exact: RseqmxC_spec. Qed. @@ -1315,12 +1315,12 @@ Section seqmx2_param. Context (C : Type) (rAC : R -> C -> Type). Context (D : Type) (rBD : R' -> D -> Type). -Global Instance RseqmxC_map_mx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) +#[export] Instance RseqmxC_map_mx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines ((rAC ==> rBD) ==> RseqmxC rAC rm rn ==> RseqmxC rBD rm rn) (fun f => @map_mx _ _ f m1 n1) map_mx_op. Proof. param_comp map_seqmx_R. Qed. -Global Instance refine_map_seqmx m n : +#[export] Instance refine_map_seqmx m n : refines ((rAC ==> rBD) ==> RseqmxC rAC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC rBD (nat_Rxx m) (nat_Rxx n)) (fun f => @map_mx _ _ f m n) map_mx_op. @@ -1347,7 +1347,7 @@ Context `{!refines (RpolyC ==> RpolyC ==> RpolyC) *%R *%C}. Context `{!refines (RpolyC ==> RpolyC) -%R -%C}. Context `{!refines (rAC ==> RpolyC) poly.polyC cast}. -Global Instance RseqmxC_char_poly_mx m1 m2 (rm : nat_R m1 m2) : +#[export] Instance RseqmxC_char_poly_mx m1 m2 (rm : nat_R m1 m2) : refines (RseqmxC rAC rm rm ==> RseqmxC RpolyC rm rm) (char_poly_mx (n:=m1)) (fun s => (scalar_seqmx m2 polyX) - (map_seqmx cast s))%C. @@ -1361,7 +1361,7 @@ rewrite -[map_mx _ (n:=_)]/((fun f => @map_mx _ _ f _ _) _). tc. Qed. -Global Instance refine_char_poly_seqmx m : +#[export] Instance refine_char_poly_seqmx m : refines (RseqmxC rAC (nat_Rxx m) (nat_Rxx m) ==> RseqmxC RpolyC (nat_Rxx m) (nat_Rxx m)) (char_poly_mx (n:=m)) @@ -1373,7 +1373,7 @@ End seqmx_poly. End seqmx_theory. From mathcomp Require Import ssrint poly. -From CoqEAL Require Import binint seqpoly binord. +From CoqEAL Require Import binnat binint seqpoly binord. Section testmx. diff --git a/refinements/seqmx_complements.v b/refinements/seqmx_complements.v index a8f9d3e..9947332 100644 --- a/refinements/seqmx_complements.v +++ b/refinements/seqmx_complements.v @@ -3,7 +3,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. From mathcomp Require Import choice fintype bigop matrix. -From CoqEAL Require Import hrel param refinements seqmx. +From CoqEAL Require Import hrel param refinements seqmx seqpoly. Set Implicit Arguments. Unset Strict Implicit. @@ -54,10 +54,10 @@ Section seqmx_op. Context {A : Type}. Context `{zero_of A}. -Global Instance fun_of_seqmx : fun_of_of A ord_instN hseqmx := +#[export] Instance fun_of_seqmx : fun_of_of A ord_instN hseqmx := fun (_ _ : nat) M i j => nth 0%C (nth [::] M i) j. -Global Instance row_seqmx : row_of ord_instN (@hseqmx A) := +#[export] Instance row_seqmx : row_of ord_instN (@hseqmx A) := fun (_ _ : nat) i M => [:: nth [::] M i]. Fixpoint store_aux T s k (v : T) := @@ -74,15 +74,15 @@ Fixpoint store_seqmx0 T m i j (v : T) := | h :: t, S i => h :: store_seqmx0 t i j v end. -Global Instance store_seqmx : store_of A ord_instN hseqmx := +#[export] Instance store_seqmx : store_of A ord_instN hseqmx := fun (_ _ : nat) M i j v => store_seqmx0 M i j v. -Global Instance trmx_seqmx : trmx_of hseqmx := +#[export] Instance trmx_seqmx : trmx_of hseqmx := fun m n : nat => @trseqmx A m n. Context `{eq_of A}. -Global Instance heq_seqmx : heq_of (@hseqmx A) := +#[export] Instance heq_seqmx : heq_of (@hseqmx A) := fun (_ _ : nat) => eq_seq (eq_seq eq_op). End seqmx_op. @@ -110,7 +110,7 @@ rewrite /map_seqmx /spec /spec_of_instance_0 /spec_id /=. by rewrite (nth_map [::]) ?Hm ?(ltn_ord i) // map_id. Qed. -Global Instance Rseqmx_fun_of_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rseqmx_fun_of_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (Rseqmx rm rn ==> Rord rm ==> Rord rn ==> eq) ((@fun_of_matrix A m1 n1) : matrix A m1 n1 -> ordinal m1 -> ordinal n1 -> A) (@fun_of_seqmx A _ m2 n2). @@ -119,7 +119,7 @@ rewrite refinesE => _ _ [M sM h1 h2 h3] i _ <- j _ <-. by rewrite /fun_of_seqmx. Qed. -Global Instance Rseqmx_row_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rseqmx_row_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (Rord rm ==> Rseqmx rm rn ==> Rseqmx (nat_R_S_R nat_R_O_R) rn) (@row A m1 n1) (@row_seqmx A m2 n2). Proof. @@ -161,12 +161,12 @@ case: j IHs => [|j] IHs //=; case: k IHs => [|k] IHs //=. by rewrite size_store_aux. Qed. -Global Instance store_ssr : store_of A ordinal (matrix A) := +#[export] Instance store_ssr : store_of A ordinal (matrix A) := fun m n (M : 'M[A]_(m, n)) (i : 'I_m) (j : 'I_n) v => \matrix_(i', j') if ((nat_of_ord i' == i) && (nat_of_ord j' == j))%N then v else M i' j'. -Global Instance Rseqmx_store_seqmx +#[export] Instance Rseqmx_store_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (Rseqmx rm rn ==> Rord rm ==> Rord rn ==> eq ==> Rseqmx rm rn) (@store_ssr m1 n1) (@store_seqmx A m2 n2). @@ -188,10 +188,10 @@ Qed. Context `{eq_of A}. -Global Instance heq_ssr : heq_of (matrix A) := +#[export] Instance heq_ssr : heq_of (matrix A) := fun n1 n2 a b => [forall i, [forall j, (a i j == b i j)%C]]. -Global Instance Rseqmx_heq_op m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : +#[export] Instance Rseqmx_heq_op m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (Rseqmx rm rn ==> Rseqmx rm rn ==> bool_R) (@heq_ssr m1 n1) (heq_seqmx (n:=n2)). Proof. @@ -245,7 +245,7 @@ Lemma RseqmxC_spec_seqmx m n (M : @seqmx C) : Proof. move=> /andP [] /eqP Hm /all_nthP Hn Hc; apply refinesP. eapply (refines_trans (b:=map_seqmx spec M)); [by tc| |]. -{ rewrite refinesE; split; [by rewrite size_map| |]. +{ rewrite refinesE; split; [by rewrite size_map| |]. { move=> i Hi; rewrite (nth_map 0%C) ?Hm // size_map. by apply/eqP/Hn; rewrite Hm. } by move=> i j; rewrite mxE. } @@ -274,13 +274,13 @@ apply nth_R_lt. rewrite h2 -?(nat_R_eq rm) -?(nat_R_eq rn); apply ltn_ord. Qed. -Global Instance refine_fun_of_seqmx m n : +#[export] Instance refine_fun_of_seqmx m n : refines (RseqmxC rAC (nat_Rxx m) (nat_Rxx n) ==> Rord (nat_Rxx m) ==> Rord (nat_Rxx n) ==> rAC) ((@fun_of_matrix A m n) : matrix A m n -> ordinal m -> ordinal n -> A) (@fun_of_seqmx C _ m n). Proof. exact: RseqmxC_fun_of_seqmx. Qed. -Global Instance refine_foldl +#[export] Instance refine_foldl (T1 T2 : Type) (rT : T1 -> T2 -> Type) (R1 R2 : Type) (rR : R1 -> R2 -> Type) : refines ((rR ==> rT ==> rR) ==> rR ==> list_R rT ==> rR) (@foldl T1 R1) (@foldl T2 R2). diff --git a/refinements/seqpoly.v b/refinements/seqpoly.v index 835057a..0d0b91a 100644 --- a/refinements/seqpoly.v +++ b/refinements/seqpoly.v @@ -25,11 +25,11 @@ Context `{add_of A, opp_of A, mul_of A, eq_of A}. Context `{zero_of N, one_of N, add_of N, eq_of N}. Context `{spec_of N nat}. -Global Instance cast_seqpoly : cast_of A seqpoly := fun x => [:: x]. +#[export] Instance cast_seqpoly : cast_of A seqpoly := fun x => [:: x]. -Global Instance seqpoly0 : zero_of seqpoly := [::]. -Global Instance seqpoly1 : one_of seqpoly := [:: 1]. -Global Instance opp_seqpoly : opp_of seqpoly := List.map -%C. +#[export] Instance seqpoly0 : zero_of seqpoly := [::]. +#[export] Instance seqpoly1 : one_of seqpoly := [:: 1]. +#[export] Instance opp_seqpoly : opp_of seqpoly := List.map -%C. Fixpoint add_seqpoly_fun (p q : seqpoly) : seqpoly := match p,q with | [::], q => q @@ -37,24 +37,24 @@ Fixpoint add_seqpoly_fun (p q : seqpoly) : seqpoly := match p,q with | a :: p', b :: q' => a + b :: add_seqpoly_fun p' q' end. -Global Instance add_seqpoly : add_of seqpoly := add_seqpoly_fun. -Global Instance sub_seqpoly : sub_of seqpoly := fun x y => (x + - y)%C. +#[export] Instance add_seqpoly : add_of seqpoly := add_seqpoly_fun. +#[export] Instance sub_seqpoly : sub_of seqpoly := fun x y => (x + - y)%C. Lemma sub_seqpoly_0 (s : seqpoly) : s - 0 = s. Proof. by elim: s. Qed. -Global Instance scale_seqpoly : scale_of A seqpoly := fun a => map ( *%C a). +#[export] Instance scale_seqpoly : scale_of A seqpoly := fun a => map ( *%C a). (* 0%C :: aux p = shift 1 (aux p) *) -Global Instance mul_seqpoly : mul_of seqpoly := fun p q => +#[export] Instance mul_seqpoly : mul_of seqpoly := fun p q => let fix aux p := if p is a :: p then (a *: q + (0%C :: aux p))%C else 0 in aux p. -Global Instance exp_seqpoly : exp_of seqpoly N := +#[export] Instance exp_seqpoly : exp_of seqpoly N := fun p n => iter (spec n) (mul_seqpoly p) 1. -Global Instance size_seqpoly : size_of seqpoly N := +#[export] Instance size_seqpoly : size_of seqpoly N := let fix aux p := if p is a :: p then let sp := aux p in @@ -63,16 +63,16 @@ Global Instance size_seqpoly : size_of seqpoly N := else 0%C in aux. -Global Instance eq_seqpoly : eq_of seqpoly := +#[export] Instance eq_seqpoly : eq_of seqpoly := fun p q => all (fun x => x == 0)%C (p - q)%C. -Global Instance shift_seqpoly : shift_of seqpoly N := +#[export] Instance shift_seqpoly : shift_of seqpoly N := fun n => ncons (spec n) 0%C. -Global Instance split_seqpoly : split_of seqpoly N := +#[export] Instance split_seqpoly : split_of seqpoly N := fun n p => (drop (spec n) p,take (spec n) p). -Global Instance lead_coef_seqpoly : lead_coef_of A seqpoly := +#[export] Instance lead_coef_seqpoly : lead_coef_of A seqpoly := fun p => nth 0 p (spec (size_seqpoly p)).-1. End seqpoly_op. @@ -116,7 +116,7 @@ Fixpoint spec_seqpoly_aux n (s : seqpoly C) : {poly R} := else (spec_seqpoly_aux n.+1 tl) + c end. -Global Instance spec_seqpoly : spec_of (seqpoly C) {poly R}:= +#[export] Instance spec_seqpoly : spec_of (seqpoly C) {poly R}:= spec_seqpoly_aux 0%N. Lemma spec_aux_shift n s : @@ -462,40 +462,40 @@ Context `{!refines (rN ==> nat_R) spec_id spec}. Definition RseqpolyC : {poly R} -> seq C -> Type := (Rseqpoly \o (list_R rAC)). -Global Instance RseqpolyC_cons : +#[export] Instance RseqpolyC_cons : refines (rAC ==> RseqpolyC ==> RseqpolyC) (@cons_poly R) cons. Proof. param_comp list_R_cons_R. Qed. -Global Instance RseqpolyC_cast : +#[export] Instance RseqpolyC_cast : refines (rAC ==> RseqpolyC) polyC cast_op. Proof. param_comp cast_seqpoly_R. Qed. -Global Instance RseqpolyC_0 : refines RseqpolyC 0%R 0%C. +#[export] Instance RseqpolyC_0 : refines RseqpolyC 0%R 0%C. Proof. param_comp seqpoly0_R. Qed. -Global Instance RseqpolyC_1 : refines RseqpolyC 1%R 1%C. +#[export] Instance RseqpolyC_1 : refines RseqpolyC 1%R 1%C. Proof. param_comp seqpoly1_R. Qed. -Global Instance RseqpolyCN : refines (RseqpolyC ==> RseqpolyC) -%R -%C. +#[export] Instance RseqpolyCN : refines (RseqpolyC ==> RseqpolyC) -%R -%C. Proof. param_comp opp_seqpoly_R. Qed. -Global Instance RseqpolyCD : +#[export] Instance RseqpolyCD : refines (RseqpolyC ==> RseqpolyC ==> RseqpolyC) +%R +%C. Proof. param_comp add_seqpoly_R. Qed. -Global Instance RseqpolyC_sub : +#[export] Instance RseqpolyC_sub : refines (RseqpolyC ==> RseqpolyC ==> RseqpolyC) (fun x y => x - y) sub_op. Proof. param_comp sub_seqpoly_R. Qed. -Global Instance RseqpolyC_scale : +#[export] Instance RseqpolyC_scale : refines (rAC ==> RseqpolyC ==> RseqpolyC) *:%R *:%C. Proof. param_comp scale_seqpoly_R. Qed. -Global Instance RseqpolyCM : +#[export] Instance RseqpolyCM : refines (RseqpolyC ==> RseqpolyC ==> RseqpolyC) *%R *%C. Proof. param_comp mul_seqpoly_R. Qed. -Global Instance RseqpolyC_exp : +#[export] Instance RseqpolyC_exp : refines (RseqpolyC ==> rN ==> RseqpolyC) (@GRing.exp _) exp_op. Proof. eapply refines_trans; tc. @@ -504,15 +504,15 @@ Proof. exact: refinesP. Qed. -Global Instance RseqpolyC_size : +#[export] Instance RseqpolyC_size : refines (RseqpolyC ==> rN) (sizep (R:=R)) size_op. Proof. rewrite /size_op; param_comp size_seqpoly_R. Qed. -Global Instance RseqpolyC_eq : +#[export] Instance RseqpolyC_eq : refines (RseqpolyC ==> RseqpolyC ==> bool_R) eqtype.eq_op eq_op. Proof. param_comp eq_seqpoly_R. Qed. -Global Instance RseqpolyC_shift : +#[export] Instance RseqpolyC_shift : refines (rN ==> RseqpolyC ==> RseqpolyC) (shiftp (R:=R)) shift_op. Proof. (* param_comp shift_seqpoly_R does a mistake on the instantiation of a @@ -523,7 +523,7 @@ Proof. exact: refinesP. Qed. -Global Instance RseqpolyCMXn p sp n rn : +#[export] Instance RseqpolyCMXn p sp n rn : refines rN n rn -> refines RseqpolyC p sp -> refines RseqpolyC (p * 'X^n) (shift_op rn sp). Proof. @@ -537,12 +537,12 @@ Proof. by rewrite coefMXn coefXnM. Qed. -Global Instance RseqpolyC_Xnmul p sp n rn : +#[export] Instance RseqpolyC_Xnmul p sp n rn : refines rN n rn -> refines RseqpolyC p sp -> refines RseqpolyC ('X^n * p) (shift_op rn sp). Proof. rewrite -mulXnC; exact: RseqpolyCMXn. Qed. -Global Instance RseqpolyC_scaleXn c rc n rn : +#[export] Instance RseqpolyC_scaleXn c rc n rn : refines rN n rn -> refines rAC c rc -> refines RseqpolyC (c *: 'X^n) (shift_op rn (cast rc)). Proof. @@ -550,21 +550,21 @@ Proof. apply: refines_apply. Qed. -Global Instance RseqpolyCMX p sp : +#[export] Instance RseqpolyCMX p sp : refines RseqpolyC p sp -> refines RseqpolyC (p * 'X) (shift_op (1%C : N) sp). Proof. rewrite -['X]expr1; exact: RseqpolyCMXn. Qed. -Global Instance RseqpolyC_Xmul p sp : +#[export] Instance RseqpolyC_Xmul p sp : refines RseqpolyC p sp -> refines RseqpolyC ('X * p) (shift_op (1%C : N) sp). Proof. rewrite -['X]expr1 -mulXnC; exact: RseqpolyCMX. Qed. -Global Instance RseqpolyC_scaleX c rc : +#[export] Instance RseqpolyC_scaleX c rc : refines rAC c rc -> refines RseqpolyC (c *: 'X) (shift_op (1%C : N) (cast rc)). Proof. rewrite -['X]expr1; exact: RseqpolyC_scaleXn. Qed. (* Uses composable_prod *) -Global Instance RseqpolyC_split : +#[export] Instance RseqpolyC_split : refines (rN ==> RseqpolyC ==> prod_R RseqpolyC RseqpolyC) (splitp (R:=R)) split_op. Proof. @@ -574,7 +574,7 @@ Proof. exact: refinesP. Qed. -Global Instance RseqpolyC_splitn n rn p sp : +#[export] Instance RseqpolyC_splitn n rn p sp : refines rN n rn -> refines RseqpolyC p sp -> refines (prod_R RseqpolyC RseqpolyC) (splitp n p) (split_op rn sp). Proof. by move=> hn hp; apply: refines_apply. Qed. @@ -582,7 +582,7 @@ Proof. by move=> hn hp; apply: refines_apply. Qed. Definition eq_prod_seqpoly (x y : (seqpoly C * seqpoly C)) := (eq_op x.1 y.1) && (eq_op x.2 y.2). -Global Instance refines_prod_RseqpolyC_eq : +#[export] Instance refines_prod_RseqpolyC_eq : refines (prod_R RseqpolyC RseqpolyC ==> prod_R RseqpolyC RseqpolyC ==> bool_R) eqtype.eq_op eq_prod_seqpoly. Proof. @@ -595,7 +595,7 @@ Proof. exact: bool_Rxx. Qed. -Global Instance RseqpolyC_lead_coef : +#[export] Instance RseqpolyC_lead_coef : refines (RseqpolyC ==> rAC) lead_coef (lead_coef_seqpoly (N:=N)). Proof. param_comp lead_coef_seqpoly_R. @@ -604,7 +604,7 @@ Qed. Local Instance refines_refl_nat : forall m, refines nat_R m m | 999. Proof. by rewrite refinesE; apply: nat_Rxx. Qed. -Global Instance RseqpolyC_head : +#[export] Instance RseqpolyC_head : refines (RseqpolyC ==> rAC) (fun p => p`_0) (fun sp => nth 0%C sp 0). Proof. eapply refines_trans; tc. @@ -612,10 +612,10 @@ Proof. apply nth_R; exact: refinesP. Qed. -Global Instance RseqpolyC_X : refines RseqpolyC 'X (shift_op (1%C : N) 1)%C. +#[export] Instance RseqpolyC_X : refines RseqpolyC 'X (shift_op (1%C : N) 1)%C. Proof. rewrite -['X]mul1r; exact: RseqpolyCMX. Qed. -Global Instance RseqpolyC_Xn n rn : +#[export] Instance RseqpolyC_Xn n rn : refines rN n rn -> refines RseqpolyC 'X^n (shift_op rn 1)%C. Proof. move=> hn; rewrite -['X^_]mul1r; exact: RseqpolyCMXn. Qed. @@ -623,13 +623,13 @@ Proof. move=> hn; rewrite -['X^_]mul1r; exact: RseqpolyCMXn. Qed. (* Proof. *) (* Admitted. *) -(* Global Instance RseqpolyC_spec_l : *) +(* #[export] Instance RseqpolyC_spec_l : *) (* refines (RseqpolyC ==> (@polynomial_R _ _ (gRing_Ring_type_Rxx R))) *) (* spec_id spec. *) (* Proof. *) (* Admitted. *) -Global Instance RseqpolyC_spec : refines (RseqpolyC ==> eq) spec_id spec. +#[export] Instance RseqpolyC_spec : refines (RseqpolyC ==> eq) spec_id spec. Proof. eapply refines_trans; tc. rewrite refinesE=> l l' rl. diff --git a/refinements/trivial_seq.v b/refinements/trivial_seq.v index 5e4a526..0aefc3f 100644 --- a/refinements/trivial_seq.v +++ b/refinements/trivial_seq.v @@ -11,7 +11,7 @@ Section size_seq. Context (A : Type) (N : Type) `{zero_of N} `{one_of N} `{add_of N}. -Global Instance size_seq : size_of (seq A) N := +#[export] Instance size_seq : size_of (seq A) N := fix size xs := if xs is x :: s then (size s + 1)%C else 0%C. End size_seq. @@ -34,7 +34,7 @@ Context `{!refines rN 0%N 0%C}. Context `{!refines rN 1%N 1%C}. Context `{!refines (rN ==> rN ==> rN) addn add_op}. -Global Instance refine_nth1 : +#[export] Instance refine_nth1 : refines (rAC ==> list_R rAC ==> rN ==> rAC) nth (fun x s (n : N) => nth x s (spec n)). Proof. @@ -42,7 +42,7 @@ Proof. rewrite -[X in refines _ X _]/(spec_id _); exact: refines_apply. Qed. -Global Instance refine_nth2 : +#[export] Instance refine_nth2 : refines (list_R (list_R rAC) ==> rN ==> list_R rAC) (nth [::]) (fun s (n : N) => nth [::] s (spec n)). Proof. @@ -51,7 +51,7 @@ Proof. rewrite -[X in refines _ X _]/(spec_id _); exact: refines_apply. Qed. -Global Instance refine_list_R2_implem s : +#[export] Instance refine_list_R2_implem s : refines (list_R (list_R rAC)) s (map (map implem) s). Proof. rewrite refinesE. @@ -68,7 +68,7 @@ Proof. exact: ihs. Qed. -Global Instance refine_size : refines (list_R rAC ==> rN) size size_op. +#[export] Instance refine_size : refines (list_R rAC ==> rN) size size_op. Proof. by rewrite refinesE => s s' rs; rewrite -[size s]size_seqE; param size_seq_R. Qed. diff --git a/theory/ssralg_ring_tac.v b/theory/ssralg_ring_tac.v index 0a5278c..c9134f1 100644 --- a/theory/ssralg_ring_tac.v +++ b/theory/ssralg_ring_tac.v @@ -8,11 +8,11 @@ Variable R : ringType. Import GRing.Theory. -Global Instance Rops: +#[export] Instance Rops: @Ring_ops R 0%R 1%R (@GRing.add R) (@GRing.mul R) (fun a b : R => a - b)%R (@GRing.opp R) eq := {}. -Global Instance R_is_ring: (@Ring _ _ _ _ _ _ _ _ Rops). +#[export] Instance R_is_ring: (@Ring _ _ _ _ _ _ _ _ Rops). constructor=> //. exact:eq_equivalence. by move=> x y H1 u v H2; rewrite H1 H2. @@ -30,10 +30,10 @@ constructor=> //. by move=> M; rewrite /addition /add_notation (addrC M) addNr. Qed. -Global Instance matrix_ops (n : nat) : @Ring_ops 'M[R]_n 0%R +#[export] Instance matrix_ops (n : nat) : @Ring_ops 'M[R]_n 0%R (scalar_mx 1) (@addmx R _ _) mulmx (fun M N => addmx M (oppmx N)) (@oppmx R _ _) eq := {}. -Global Instance matrix_is_ring (n : nat) : +#[export] Instance matrix_is_ring (n : nat) : (@Ring _ _ _ _ _ _ _ _ (matrix_ops n)). Proof. constructor=> //.