Skip to content

Commit

Permalink
Merge pull request #169 from ppedrot/hint-locality-error
Browse files Browse the repository at this point in the history
Adapt w.r.t. coq/coq#16004.
  • Loading branch information
spitters authored Jul 7, 2022
2 parents 6fd70a3 + ca36714 commit e13df50
Show file tree
Hide file tree
Showing 119 changed files with 854 additions and 1 deletion.
3 changes: 3 additions & 0 deletions algebra/CAbGroups.v
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,9 @@ End Various.

End Abelian_Groups.

#[global]
Hint Resolve cag_commutes_unfolded: algebra.
#[global]
Hint Resolve cag_op_inv assoc_1 zero_minus minus_plus op_lft_resp_ap: algebra.

Module Export coercions.
Expand Down Expand Up @@ -523,6 +525,7 @@ Qed.

End Group_Extras.

#[global]
Hint Resolve nmult_wd nmult_one nmult_Zero nmult_plus nmult_inv nmult_mult
nmult_plus' zmult_wd zmult_one zmult_min_one zmult_zero zmult_Zero
zmult_plus zmult_mult zmult_plus': algebra.
Expand Down
1 change: 1 addition & 0 deletions algebra/CAbMonoids.v
Original file line number Diff line number Diff line change
Expand Up @@ -113,4 +113,5 @@ End SubCAbMonoids.

End Abelian_Monoids.

#[global]
Hint Resolve cam_commutes_unfolded: algebra.
5 changes: 5 additions & 0 deletions algebra/CFields.v
Original file line number Diff line number Diff line change
Expand Up @@ -181,6 +181,7 @@ Qed.

End Field_basics.

#[global]
Hint Resolve field_mult_inv field_mult_inv_op: algebra.

Section Field_multiplication.
Expand Down Expand Up @@ -384,6 +385,7 @@ Qed.
End x_square.


#[global]
Hint Resolve mult_resp_ap_zero: algebra.


Expand Down Expand Up @@ -700,6 +702,7 @@ Qed.

End Div_properties.

#[global]
Hint Resolve div_1 div_1' div_1'' div_wd x_div_x x_div_one div_div div_div2
mult_of_divs x_mult_y_div_z mult_of_divs div_dist div_dist' div_semi_sym
div_prop: algebra.
Expand Down Expand Up @@ -911,6 +914,8 @@ Notation "{1/} x" := (Frecip x) (at level 4, right associativity).
Arguments Fdiv [X].
Infix "{/}" := Fdiv (at level 41, no associativity).

#[global]
Hint Resolve included_FRecip included_FDiv : included.

#[global]
Hint Immediate included_FRecip' included_FDiv' included_FDiv'' : included.
9 changes: 9 additions & 0 deletions algebra/CGroups.v
Original file line number Diff line number Diff line change
Expand Up @@ -292,9 +292,13 @@ Proof.
apply cg_minus_wd; assumption.
Qed.

#[global]
Hint Resolve cg_rht_inv_unfolded cg_lft_inv_unfolded: algebra.
#[global]
Hint Resolve cg_inv_inv cg_minus_correct cg_zero_inv cg_inv_zero: algebra.
#[global]
Hint Resolve cg_minus_unfolded grp_inv_assoc cg_inv_op: algebra.
#[global]
Hint Resolve cg_minus_wd: algebra_c.

(**
Expand Down Expand Up @@ -332,6 +336,7 @@ Qed.

End Assoc_properties.

#[global]
Hint Resolve assoc_2 minus_plus zero_minus cg_cancel_mixed plus_resp_eq:
algebra.

Expand Down Expand Up @@ -442,7 +447,9 @@ Proof.
Qed.

End cgroups_apartness.
#[global]
Hint Resolve op_rht_resp_ap: algebra.
#[global]
Hint Resolve minus_ap_zero zero_minus_apart inv_resp_ap_zero: algebra.

Section CGroup_Ops.
Expand Down Expand Up @@ -617,6 +624,8 @@ Notation "{--} x" := (Finv x) (at level 4, right associativity).
Arguments Fminus [G].
Infix "{-}" := Fminus (at level 50, left associativity).

#[global]
Hint Resolve included_FInv included_FMinus : included.

#[global]
Hint Immediate included_FInv' included_FMinus' included_FMinus'' : included.
1 change: 1 addition & 0 deletions algebra/CMonoids.v
Original file line number Diff line number Diff line change
Expand Up @@ -1040,4 +1040,5 @@ Definition Dbrack_as_CMonoid : CMonoid :=
End Th15.


#[global]
Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
2 changes: 2 additions & 0 deletions algebra/COrdFields.v
Original file line number Diff line number Diff line change
Expand Up @@ -430,6 +430,7 @@ Qed.

End Basic_Properties_of_leEq.

#[global]
Hint Resolve less_leEq : algebra.

Declare Left Step leEq_wdl.
Expand Down Expand Up @@ -773,6 +774,7 @@ End More_than_four.

End infinity_of_cordfields.

#[global]
Hint Resolve pos_one : algebra.

Declare Left Step leEq_wdl.
Expand Down
3 changes: 3 additions & 0 deletions algebra/COrdFields2.v
Original file line number Diff line number Diff line change
Expand Up @@ -885,6 +885,7 @@ Qed.

End Properties_of_leEq.

#[global]
Hint Resolve shift_leEq_lft mult_resp_nonneg plus_resp_nonneg: algebra.

(*---------------------------------*)
Expand Down Expand Up @@ -1084,6 +1085,7 @@ Qed.

End PosP_properties.

#[global]
Hint Resolve mult_resp_nonneg.

(**
Expand Down Expand Up @@ -1196,4 +1198,5 @@ Proof.
Qed.

End Half_properties.
#[global]
Hint Resolve half_1 half_1' half_2: algebra.
2 changes: 2 additions & 0 deletions algebra/CPoly_Degree.v
Original file line number Diff line number Diff line change
Expand Up @@ -581,7 +581,9 @@ Qed.

End Degree_props.

#[global]
Hint Resolve poly_as_sum'' poly_as_sum' poly_as_sum: algebra.
#[global]
Hint Resolve degree_mult_aux: algebra.


Expand Down
6 changes: 6 additions & 0 deletions algebra/CPoly_NthCoeff.v
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,7 @@ End NthCoeff_def.
Arguments nth_coeff [R].
Arguments nth_coeff_fun [R].

#[global]
Hint Resolve nth_coeff_wd: algebra_c.

Section NthCoeff_props.
Expand Down Expand Up @@ -469,8 +470,13 @@ Qed.

End NthCoeff_props.

#[global]
Hint Resolve nth_coeff_wd: algebra_c.
#[global]
Hint Resolve nth_coeff_complicated poly_at_zero nth_coeff_inv: algebra.
#[global]
Hint Resolve nth_coeff_inv' nth_coeff_c_mult_p nth_coeff_mult: algebra.
#[global]
Hint Resolve nth_coeff_zero nth_coeff_plus nth_coeff_minus: algebra.
#[global]
Hint Resolve nth_coeff_nexp_eq nth_coeff_nexp_neq: algebra.
12 changes: 12 additions & 0 deletions algebra/CPolynomials.v
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,9 @@
Require Import CoRN.algebra.CRing_Homomorphisms.
Require Import CoRN.tactics.Rational.

(* Backwards compatibility for Hint Rewrite locality attributes *)
Set Warnings "-unsupported-attributes".

(**
* Polynomials
The first section only proves the polynomials form a ring.
Expand Down Expand Up @@ -2422,15 +2425,23 @@ Proof (cpoly_double_ind0_cs CR).

End Poly_Prop_Induction.

#[global]
Hint Resolve poly_linear cpoly_lin: algebra.
#[global]
Hint Resolve apply_wd cpoly_const_eq: algebra_c.
#[global]
Hint Resolve c_apply x_apply inv_apply plus_apply minus_apply mult_apply
nexp_apply: algebra.
#[global]
Hint Resolve one_apply c_zero c_one c_mult: algebra.
#[global]
Hint Resolve poly_inv_apply: algebra.
#[global]
Hint Resolve c_mult_lin: algebra.

#[global]
Hint Rewrite one_apply c_apply x_apply mult_apply plus_apply minus_apply : apply.
#[global]
Hint Rewrite inv_apply nexp_apply c_mult_apply poly_inv_apply : apply.
Ltac poly_apply:= autorewrite with apply; simpl.
(** The tactic [poly_apply] applies polynomials to arguments *)
Expand Down Expand Up @@ -2592,6 +2603,7 @@ Qed.
End Derivative.
Notation "'_D_'" := (@cpolyder _).

#[global]
Hint Rewrite diff_zero diff_one diff_const diff_x diff_plus diff_c_mult diff_mult diff_linear : poly_diff.
Section Map.

Expand Down
6 changes: 6 additions & 0 deletions algebra/CRing_Homomorphisms.v
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,9 @@
Require Export CoRN.algebra.CRings.
Set Automatic Introduction.

(* Backwards compatibility for Hint Rewrite locality attributes *)
Set Warnings "-unsupported-attributes".

(**
* Ring Homomorphisms
** Definition of Ring Homomorphisms
Expand Down Expand Up @@ -178,8 +181,11 @@ End RingHom_Basics.

End RingHom_Lemmas.

#[global]
Hint Resolve rh_strext rh_pres_plus rh_pres_mult rh_pres_unit : algebra.
#[global]
Hint Resolve rh_pres_zero rh_pres_minus rh_pres_inv rh_apzero : algebra.
#[global]
Hint Rewrite rh_pres_zero rh_pres_plus rh_pres_minus rh_pres_inv rh_pres_mult rh_pres_unit : ringHomPush.

Definition RHid R : RingHom R R.
Expand Down
16 changes: 16 additions & 0 deletions algebra/CRings.v
Original file line number Diff line number Diff line change
Expand Up @@ -236,8 +236,11 @@ Proof.
Qed.

End Ring_unfolded.
#[global]
Hint Resolve mult_assoc_unfolded: algebra.
#[global]
Hint Resolve ring_non_triv mult_one one_mult mult_commut_unfolded: algebra.
#[global]
Hint Resolve ring_dist_unfolded ring_distl_unfolded: algebra.


Expand Down Expand Up @@ -368,11 +371,17 @@ Qed.


End Ring_basics.
#[global]
Hint Resolve cring_mult_zero cring_mult_zero_op: algebra.
#[global]
Hint Resolve inv_mult_invol: algebra.
#[global]
Hint Resolve cring_inv_mult_lft cring_inv_mult_rht: algebra.
#[global]
Hint Resolve ring_dist_minus: algebra.
#[global]
Hint Resolve ring_distl_minus: algebra.
#[global]
Hint Resolve mult_minus1 ring_distr1 ring_distr2: algebra.
(* Begin_SpecReals *)

Expand Down Expand Up @@ -467,6 +476,7 @@ Qed.

End nat_injection.

#[global]
Hint Resolve nring_comm_plus nring_comm_mult: algebra.

Arguments nring [R].
Expand Down Expand Up @@ -498,6 +508,7 @@ Proof.
simpl in |- *; algebra.
Qed.

#[global]
Hint Resolve one_plus_one x_plus_x: algebra.

(**
Expand Down Expand Up @@ -846,6 +857,7 @@ End int_injection.

Arguments zring [R].

#[global]
Hint Resolve pring_convert zring_zero zring_diff zring_plus_nat zring_inv_nat
zring_plus zring_inv zring_minus zring_mult zring_one zring_inv_one:
algebra.
Expand Down Expand Up @@ -991,6 +1003,7 @@ Qed.

End Dist_properties.

#[global]
Hint Resolve dist_1b dist_2a dist_2b mult_distr_sum_lft mult_distr_sum_rht
sumx_const: algebra.

Expand Down Expand Up @@ -1199,6 +1212,7 @@ Add Parametric Morphism c n : (nexp c n) with signature (@cs_eq (cr_crr c)) ==>
Proof.
intros. apply: nexp_wd. assumption. Qed.

#[global]
Hint Resolve nexp_wd nexp_Sn nexp_plus one_nexp mult_nexp nexp_mult zero_nexp
inv_nexp_even inv_nexp_two inv_nexp_odd nexp_one nexp_two nexp_funny
inv_one_even_nexp inv_one_odd_nexp nexp_funny' one_nexp square_plus
Expand Down Expand Up @@ -1371,7 +1385,9 @@ Section cr_Product.
End cr_Product.


#[global]
Hint Resolve included_FMult included_FScalMult included_FNth : included.

#[global]
Hint Immediate included_FMult' included_FMult'' included_FScalMult'
included_FNth' : included.
3 changes: 3 additions & 0 deletions algebra/CSemiGroups.v
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,7 @@ Qed.

(* End_SpecReals *)

#[global]
Hint Resolve plus_assoc_unfolded: algebra.

(**
Expand Down Expand Up @@ -230,8 +231,10 @@ End Part_Function_Plus.
Arguments Fplus [G].
Infix "{+}" := Fplus (at level 50, left associativity).

#[global]
Hint Resolve included_FPlus : included.

#[global]
Hint Immediate included_FPlus' included_FPlus'' : included.

(**
Expand Down
2 changes: 2 additions & 0 deletions algebra/CSetoidFun.v
Original file line number Diff line number Diff line change
Expand Up @@ -830,6 +830,7 @@ why we chose to altogether do away with this approach.
We now present some methods for defining partial functions.
*)

#[global]
Hint Resolve I: core.

Section CSetoid_Ops.
Expand Down Expand Up @@ -965,6 +966,7 @@ Notation FId := (Fid _).
Arguments Fcomp [S].
Infix "[o]" := Fcomp (at level 65, no associativity).

#[global]
Hint Resolve pfwdef bpfwdef: algebra.

Section bijections.
Expand Down
2 changes: 2 additions & 0 deletions algebra/CSetoidInc.v
Original file line number Diff line number Diff line change
Expand Up @@ -148,6 +148,8 @@ End inclusion.

Arguments included [S].

#[global]
Hint Resolve included_refl included_FComp : included.

#[global]
Hint Immediate included_trans included_FComp' : included.
6 changes: 6 additions & 0 deletions algebra/CSetoids.v
Original file line number Diff line number Diff line change
Expand Up @@ -409,8 +409,11 @@ Definition ProdCSetoid (A B : CSetoid) : CSetoid := Build_CSetoid
End product_csetoid.
Arguments ex_unq [S].

#[global]
Hint Resolve eq_reflexive_unfolded ap_irreflexive_unfolded: algebra_r.
#[global]
Hint Resolve eq_symmetric_unfolded ap_symmetric_unfolded: algebra_s.
#[global]
Hint Resolve eq_transitive_unfolded ap_cotransitive_unfolded: algebra_c.

Declare Left Step eq_wdl.
Expand Down Expand Up @@ -808,6 +811,7 @@ Definition bin_fun2fun_rht (S1 S2 S3:CSetoid) (f : CSetoid_bin_fun S1 S2 S3) (c
Definition bin_fun2fun_lft (S1 S2 S3:CSetoid) (f : CSetoid_bin_fun S1 S2 S3) (c : S2) : CSetoid_fun S1 S3 :=
Build_CSetoid_fun _ _ (fun x : S1 => f x c) (bin_fun_is_strext_fun_lft _ _ _ f c).

#[global]
Hint Resolve csf_wd_unfolded csbf_wd_unfolded csf_strext_unfolded: algebra_c.

Arguments fun_wd [S1 S2].
Expand Down Expand Up @@ -924,6 +928,7 @@ Arguments commutes [S].
Arguments associative [S].

(* Needs to be unfolded to be used as a Hint *)
#[global]
Hint Resolve ap_wdr_unfolded ap_wdl_unfolded bin_op_wd_unfolded un_op_wd_unfolded : algebra_c.

(**
Expand Down Expand Up @@ -955,6 +960,7 @@ Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun.
(* end hide *)

End csetoid_outer_ops.
#[global]
Hint Resolve csoo_wd_unfolded: algebra_c.

(**
Expand Down
Loading

0 comments on commit e13df50

Please sign in to comment.