Skip to content

Commit

Permalink
Adapt w.r.t. coq/coq#18895. (#1859)
Browse files Browse the repository at this point in the history
  • Loading branch information
@ppedrot
ppedrot authored Apr 12, 2024
1 parent d7b2a6c commit d81081d
Show file tree
Hide file tree
Showing 10 changed files with 96 additions and 43 deletions.
9 changes: 5 additions & 4 deletions src/Experiments/SimplyTypedArithmetic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -551,10 +551,11 @@ Section mod_ops.
{ t_weight_with (@pow_ceil_mul_nat_multiples 2). }
{ intros; apply Z.gt_lt. t_weight_with (@pow_ceil_mul_nat_divide 2). }
Defined.
Local Hint Immediate (weight_0 wprops).
Local Hint Immediate (weight_positive wprops).
Local Hint Immediate (weight_multiples wprops).
Local Hint Immediate (weight_divides wprops).

Local Hint Extern 0 => simple apply (weight_0 wprops).
Local Hint Extern 0 => simple apply (weight_positive wprops).
Local Hint Extern 0 => simple apply (weight_multiples wprops).
Local Hint Extern 0 => simple apply (weight_divides wprops).
Local Hint Resolve Z.positive_is_nonzero Z.lt_gt.

Local Lemma weight_1_gt_1 : weight 1 > 1.
Expand Down
4 changes: 2 additions & 2 deletions src/LegacyArithmetic/Double/Proofs/Decode.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ Qed.
Global Hint Extern 1 (@is_add_with_carry _ _ (@tuple_decoder ?n ?W ?decode 1) ?adc)
=> apply (@is_add_with_carry_1tuple n W decode adc) : typeclass_instances.

Global Hint Resolve (fun n W decode pf => (@tuple_is_decode n W decode 2 pf : @is_decode (2 * n) (tuple W 2) (@tuple_decoder n W decode 2))) : typeclass_instances.
Global Hint Extern 1 => simple apply (fun n W decode pf => (@tuple_is_decode n W decode 2 pf : @is_decode (2 * n) (tuple W 2) (@tuple_decoder n W decode 2))) : typeclass_instances.
Global Hint Extern 3 (@is_decode _ (tuple ?W ?k) _) => let kv := (eval simpl in (Z.of_nat k)) in apply (fun n decode pf => (@tuple_is_decode n W decode k pf : @is_decode (kv * n) (tuple W k) (@tuple_decoder n W decode k : decoder (kv * n)%Z (tuple W k)))) : typeclass_instances.

#[global]
Expand Down Expand Up @@ -211,7 +211,7 @@ Module Export Hints.
Global Hint Extern 1 (@is_add_with_carry _ _ (@tuple_decoder ?n ?W ?decode 1) ?adc)
=> apply (@is_add_with_carry_1tuple n W decode adc) : typeclass_instances.

Global Hint Resolve (fun n W decode pf => (@tuple_is_decode n W decode 2 pf : @is_decode (2 * n) (tuple W 2) (@tuple_decoder n W decode 2))) : typeclass_instances.
Global Hint Extern 1 => simple apply (fun n W decode pf => (@tuple_is_decode n W decode 2 pf : @is_decode (2 * n) (tuple W 2) (@tuple_decoder n W decode 2))) : typeclass_instances.
Global Hint Extern 3 (@is_decode _ (tuple ?W ?k) _) => let kv := (eval simpl in (Z.of_nat k)) in apply (fun n decode pf => (@tuple_is_decode n W decode k pf : @is_decode (kv * n) (tuple W k) (@tuple_decoder n W decode k : decoder (kv * n)%Z (tuple W k)))) : typeclass_instances.

#[global]
Expand Down
4 changes: 2 additions & 2 deletions src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,7 +153,7 @@ End ripple_carry_adc.

Global Hint Extern 2 (@is_add_with_carry _ (tuple ?W ?k) (@tuple_decoder ?n _ ?decode _) (@ripple_carry_adc _ ?adc _))
=> apply (@ripple_carry_is_add_with_carry n W decode adc k) : typeclass_instances.
Global Hint Resolve (fun n W decode adc isdecode isadc
Global Hint Extern 2 => simple apply (fun n W decode adc isdecode isadc
=> @ripple_carry_is_add_with_carry n W decode adc 2 isdecode isadc
: @is_add_with_carry (Z.of_nat 2 * n) (W * W) (@tuple_decoder n W decode 2) (@ripple_carry_adc W adc 2))
: typeclass_instances.
Expand Down Expand Up @@ -198,7 +198,7 @@ End ripple_carry_subc.

Global Hint Extern 2 (@is_sub_with_carry _ (tuple ?W ?k) (@tuple_decoder ?n _ ?decode _) (@ripple_carry_subc _ ?subc _))
=> apply (@ripple_carry_is_sub_with_carry n W decode subc k) : typeclass_instances.
Global Hint Resolve (fun n W decode subc isdecode issubc
Global Hint Extern 2 => simple apply (fun n W decode subc isdecode issubc
=> @ripple_carry_is_sub_with_carry n W decode subc 2 isdecode issubc
: @is_sub_with_carry (Z.of_nat 2 * n) (W * W) (@tuple_decoder n W decode 2) (@ripple_carry_subc W subc 2))
: typeclass_instances.
2 changes: 1 addition & 1 deletion src/Util/Equality.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ Section hprop.

Let hprop_encode {x y : A} (p : x = y) : unit := tt.

Local Hint Resolve (fun x => @isiso_encode A x (fun _ => unit)) : typeclass_instances.
Local Hint Extern 1 => simple apply (fun x => @isiso_encode A x (fun _ => unit)) : typeclass_instances.

Global Instance ishprop_path_hprop : IsHPropRel (@eq A).
Proof.
Expand Down
8 changes: 5 additions & 3 deletions src/Util/NatUtil.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,10 @@ Create HintDb natsimplify discriminated.
Global Existing Instance Nat.le_preorder.
Global Hint Resolve Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r: arith.
Global Hint Resolve Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r: arith.

Global Hint Resolve mod_bound_pos Nat.add_le_mono : arith.
Global Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith.

Global Hint Extern 2 (le _) => simple apply (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) : arith.
Global Hint Extern 2 => simple apply (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith.

#[global]
Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using lia : natsimplify.
Expand Down Expand Up @@ -474,7 +475,8 @@ Module Export Hints.
Global Hint Resolve Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r: arith.
Global Hint Resolve Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r: arith.
Global Hint Resolve mod_bound_pos Nat.add_le_mono : arith.
Global Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith.
Global Hint Extern 2 (le _) => simple apply (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) : arith.
Global Hint Extern 2 => simple apply (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith.
#[global]
Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using lia : natsimplify.
#[global]
Expand Down
8 changes: 4 additions & 4 deletions src/Util/ZUtil/Div.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -365,8 +365,8 @@ Module Z.
autorewrite with zsimplify; try reflexivity.
Qed.

Global Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1))
(fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.
Global Hint Extern 2 => simple apply (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.
Global Hint Extern 2 => simple apply (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.

Lemma sub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a <? b then -1 else 0.
Proof.
Expand Down Expand Up @@ -491,8 +491,8 @@ Module Export Hints.
Global Hint Resolve Z.div_mul_le_le_offset : zarith.
#[global]
Hint Rewrite Z.div_x_y_x using zutil_arith : zsimplify.
Global Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1))
(fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.
Global Hint Extern 2 => simple apply (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.
Global Hint Extern 2 => simple apply (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.
#[global]
Hint Rewrite Z.sub_pos_bound_div_eq Z.add_opp_pos_bound_div_eq using zutil_arith : zstrip_div.
Global Hint Resolve Z.div_small_sym : zarith.
Expand Down
6 changes: 4 additions & 2 deletions src/Util/ZUtil/Hints.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,10 @@ Require Export Crypto.Util.ZUtil.Hints.Ztestbit.
Require Export Crypto.Util.ZUtil.Hints.PullPush.
Require Export Crypto.Util.ZUtil.ZSimplify.Core.

Global Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2.
Global Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2.
Global Hint Extern 2 => simple apply (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) : concl_log2.
Global Hint Extern 2 => simple apply (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2.
Global Hint Extern 2 => simple apply (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) : hyp_log2.
Global Hint Extern 2 => simple apply (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : hyp_log2.

(** For the occasional lemma that can remove the use of [Z.div] *)
#[global]
Expand Down
10 changes: 6 additions & 4 deletions src/Util/ZUtil/Hints/ZArith.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,11 @@ Require Import Coq.ZArith.ZArith.
Require Export Crypto.Util.ZUtil.Hints.Core.

Global Hint Resolve Z.log2_nonneg Z.log2_up_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound Z.div_pos Zmult_lt_compat_r Z.pow_le_mono_r Z.pow_le_mono_l Z.div_lt Z.div_le_compat_l Z.div_le_mono Z.max_le_compat Z.min_le_compat Z.log2_up_le_mono Z.pow_nonneg : zarith.
Global Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) (fun a b pf => proj1 (Z.pow_gt_1 a b pf)) : zarith.
Global Hint Resolve (fun n m => proj1 (Z.opp_le_mono n m)) : zarith.
Global Hint Resolve (fun n m => proj1 (Z.pred_le_mono n m)) : zarith.
Global Hint Resolve (fun a b => proj2 (Z.lor_nonneg a b)) : zarith.
Global Hint Extern 1 => simple apply (fun a b H => proj1 (Z.mod_pos_bound a b H)) : zarith.
Global Hint Extern 1 => simple apply (fun a b H => proj2 (Z.mod_pos_bound a b H)) : zarith.
Global Hint Extern 2 => simple apply (fun a b pf => proj1 (Z.pow_gt_1 a b pf)) : zarith.
Global Hint Extern 1 => simple apply (fun n m => proj1 (Z.opp_le_mono n m)) : zarith.
Global Hint Extern 1 => simple apply (fun n m => proj1 (Z.pred_le_mono n m)) : zarith.
Global Hint Extern 1 => simple apply (fun a b => proj2 (Z.lor_nonneg a b)) : zarith.

Global Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.add_le_mono Z.sub_le_mono : zarith.
73 changes: 57 additions & 16 deletions src/Util/ZUtil/LandLorBounds.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -228,11 +228,15 @@ Module Z.
rewrite (Z.land_comm (Z.pos x)), Z.land_assoc.
apply Z.land_upper_bound_l; rewrite ?Z.land_nonneg; t.
Qed.
Global Hint Resolve land_round_bound_pos_r (fun v x => proj1 (land_round_bound_pos_r v x)) (fun v x => proj2 (land_round_bound_pos_r v x)) : zarith.
Global Hint Resolve land_round_bound_pos_r : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (land_round_bound_pos_r v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (land_round_bound_pos_r v x)) : zarith.
Lemma land_round_bound_pos_l v x
: 0 <= Z.land (Z.pos x) v <= Z.land (Z.round_lor_land_bound (Z.pos x)) v.
Proof. rewrite <- !(Z.land_comm v); apply land_round_bound_pos_r. Qed.
Global Hint Resolve land_round_bound_pos_l (fun v x => proj1 (land_round_bound_pos_l v x)) (fun v x => proj2 (land_round_bound_pos_l v x)) : zarith.
Global Hint Resolve land_round_bound_pos_l : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (land_round_bound_pos_l v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (land_round_bound_pos_l v x)) : zarith.

Lemma land_round_bound_neg_r v x
: Z.land v (Z.round_lor_land_bound (Z.neg x)) <= Z.land v (Z.neg x) <= v.
Expand All @@ -244,11 +248,15 @@ Module Z.
rewrite !Z.land_assoc.
etransitivity; [ apply Z.land_le; cbn; lia | ]; lia.
Qed.
Global Hint Resolve land_round_bound_neg_r (fun v x => proj1 (land_round_bound_neg_r v x)) (fun v x => proj2 (land_round_bound_neg_r v x)) : zarith.
Global Hint Resolve land_round_bound_neg_r : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (land_round_bound_neg_r v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (land_round_bound_neg_r v x)) : zarith.
Lemma land_round_bound_neg_l v x
: Z.land (Z.round_lor_land_bound (Z.neg x)) v <= Z.land (Z.neg x) v <= v.
Proof. rewrite <- !(Z.land_comm v); apply land_round_bound_neg_r. Qed.
Global Hint Resolve land_round_bound_neg_l (fun v x => proj1 (land_round_bound_neg_l v x)) (fun v x => proj2 (land_round_bound_neg_l v x)) : zarith.
Global Hint Resolve land_round_bound_neg_l : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (land_round_bound_neg_l v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (land_round_bound_neg_l v x)) : zarith.

Lemma lor_round_bound_neg_r v x
: Z.lor v (Z.round_lor_land_bound (Z.neg x)) <= Z.lor v (Z.neg x) <= -1.
Expand All @@ -262,11 +270,15 @@ Module Z.
Z.peel_le.
apply Z.land_upper_bound_l; rewrite ?Z.land_nonneg; t.
Qed.
Global Hint Resolve lor_round_bound_neg_r (fun v x => proj1 (lor_round_bound_neg_r v x)) (fun v x => proj2 (lor_round_bound_neg_r v x)) : zarith.
Global Hint Resolve lor_round_bound_neg_r : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (lor_round_bound_neg_r v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (lor_round_bound_neg_r v x)) : zarith.
Lemma lor_round_bound_neg_l v x
: Z.lor (Z.round_lor_land_bound (Z.neg x)) v <= Z.lor (Z.neg x) v <= -1.
Proof. rewrite <- !(Z.lor_comm v); apply lor_round_bound_neg_r. Qed.
Global Hint Resolve lor_round_bound_neg_l (fun v x => proj1 (lor_round_bound_neg_l v x)) (fun v x => proj2 (lor_round_bound_neg_l v x)) : zarith.
Global Hint Resolve lor_round_bound_neg_l : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (lor_round_bound_neg_l v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (lor_round_bound_neg_l v x)) : zarith.

Lemma lor_round_bound_pos_r v x
: v <= Z.lor v (Z.pos x) <= Z.lor v (Z.round_lor_land_bound (Z.pos x)).
Expand All @@ -278,11 +290,15 @@ Module Z.
rewrite !Z.lor_assoc.
etransitivity; [ | apply Z.lor_lower; rewrite ?Z.lor_nonneg; cbn; lia ]; lia.
Qed.
Global Hint Resolve lor_round_bound_pos_r (fun v x => proj1 (lor_round_bound_pos_r v x)) (fun v x => proj2 (lor_round_bound_pos_r v x)) : zarith.
Global Hint Resolve lor_round_bound_pos_r : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (lor_round_bound_pos_r v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (lor_round_bound_pos_r v x)) : zarith.
Lemma lor_round_bound_pos_l v x
: v <= Z.lor (Z.pos x) v <= Z.lor (Z.round_lor_land_bound (Z.pos x)) v.
Proof. rewrite <- !(Z.lor_comm v); apply lor_round_bound_pos_r. Qed.
Global Hint Resolve lor_round_bound_pos_l (fun v x => proj1 (lor_round_bound_pos_l v x)) (fun v x => proj2 (lor_round_bound_pos_l v x)) : zarith.
Global Hint Resolve lor_round_bound_pos_l : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (lor_round_bound_pos_l v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (lor_round_bound_pos_l v x)) : zarith.

Lemma land_round_bound_pos_r' v x : Z.land v (Z.pos x) <= Z.land v (Z.round_lor_land_bound (Z.pos x)). Proof. auto with zarith. Qed.
Lemma land_round_bound_pos_l' v x : Z.land (Z.pos x) v <= Z.land (Z.round_lor_land_bound (Z.pos x)) v. Proof. auto with zarith. Qed.
Expand Down Expand Up @@ -324,12 +340,37 @@ Module Export Hints.
Hint Rewrite Z.lor_round_lor_land_bound_r : zsimplify_fast zsimplify.
#[global]
Hint Rewrite Z.lor_round_lor_land_bound_l : zsimplify_fast zsimplify.
Global Hint Resolve Z.land_round_bound_pos_r (fun v x => proj1 (Z.land_round_bound_pos_r v x)) (fun v x => proj2 (Z.land_round_bound_pos_r v x)) : zarith.
Global Hint Resolve Z.land_round_bound_pos_l (fun v x => proj1 (Z.land_round_bound_pos_l v x)) (fun v x => proj2 (Z.land_round_bound_pos_l v x)) : zarith.
Global Hint Resolve Z.land_round_bound_neg_r (fun v x => proj1 (Z.land_round_bound_neg_r v x)) (fun v x => proj2 (Z.land_round_bound_neg_r v x)) : zarith.
Global Hint Resolve Z.land_round_bound_neg_l (fun v x => proj1 (Z.land_round_bound_neg_l v x)) (fun v x => proj2 (Z.land_round_bound_neg_l v x)) : zarith.
Global Hint Resolve Z.lor_round_bound_neg_r (fun v x => proj1 (Z.lor_round_bound_neg_r v x)) (fun v x => proj2 (Z.lor_round_bound_neg_r v x)) : zarith.
Global Hint Resolve Z.lor_round_bound_neg_l (fun v x => proj1 (Z.lor_round_bound_neg_l v x)) (fun v x => proj2 (Z.lor_round_bound_neg_l v x)) : zarith.
Global Hint Resolve Z.lor_round_bound_pos_r (fun v x => proj1 (Z.lor_round_bound_pos_r v x)) (fun v x => proj2 (Z.lor_round_bound_pos_r v x)) : zarith.
Global Hint Resolve Z.lor_round_bound_pos_l (fun v x => proj1 (Z.lor_round_bound_pos_l v x)) (fun v x => proj2 (Z.lor_round_bound_pos_l v x)) : zarith.

Global Hint Resolve Z.land_round_bound_pos_r : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (Z.land_round_bound_pos_r v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (Z.land_round_bound_pos_r v x)) : zarith.

Global Hint Resolve Z.land_round_bound_pos_l : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (Z.land_round_bound_pos_l v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (Z.land_round_bound_pos_l v x)) : zarith.

Global Hint Resolve Z.land_round_bound_neg_r : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (Z.land_round_bound_neg_r v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (Z.land_round_bound_neg_r v x)) : zarith.

Global Hint Resolve Z.land_round_bound_neg_l : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (Z.land_round_bound_neg_l v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (Z.land_round_bound_neg_l v x)) : zarith.

Global Hint Resolve Z.lor_round_bound_neg_r : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (Z.lor_round_bound_neg_r v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (Z.lor_round_bound_neg_r v x)) : zarith.

Global Hint Resolve Z.lor_round_bound_neg_l : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (Z.lor_round_bound_neg_l v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (Z.lor_round_bound_neg_l v x)) : zarith.

Global Hint Resolve Z.lor_round_bound_pos_r : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (Z.lor_round_bound_pos_r v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (Z.lor_round_bound_pos_r v x)) : zarith.

Global Hint Resolve Z.lor_round_bound_pos_l : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj1 (Z.lor_round_bound_pos_l v x)) : zarith.
Global Hint Extern 0 => simple apply (fun v x => proj2 (Z.lor_round_bound_pos_l v x)) : zarith.

End Hints.
15 changes: 10 additions & 5 deletions src/Util/ZUtil/Pow.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,12 @@ Module Z.
erewrite Z.pow_neg_r in * by eassumption.
lia.
Qed.
Global Hint Resolve nonneg_pow_pos (fun n => nonneg_pow_pos 2 n Z.lt_0_2) : zarith.
Global Hint Resolve nonneg_pow_pos : zarith.
Global Hint Extern 1 => simple apply (fun n => nonneg_pow_pos 2 n Z.lt_0_2) : zarith.
Lemma nonneg_pow_pos_helper a b dummy : 0 < a -> 0 <= dummy < a^b -> 0 <= b.
Proof. eauto with zarith lia. Qed.
Global Hint Resolve nonneg_pow_pos_helper (fun n dummy => nonneg_pow_pos_helper 2 n dummy Z.lt_0_2) : zarith.
Global Hint Resolve nonneg_pow_pos_helper : zarith.
Global Hint Extern 2 => simple apply (fun n dummy => nonneg_pow_pos_helper 2 n dummy Z.lt_0_2) : zarith.

Lemma div_pow2succ : forall n x, (0 <= x) ->
n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x).
Expand All @@ -45,7 +47,10 @@ Module Export Hints.
#[global]
Hint Rewrite <- Z.two_p_two_eq_four : push_Zpow.
Global Hint Resolve Z.pow_sub_r' Z.pow_sub_r'_sym Z.eq_le_incl : zarith.
Global Hint Resolve (fun b => f_equal (fun e => b ^ e)) (fun e => f_equal (fun b => b ^ e)) : zarith.
Global Hint Resolve Z.nonneg_pow_pos (fun n => Z.nonneg_pow_pos 2 n Z.lt_0_2) : zarith.
Global Hint Resolve Z.nonneg_pow_pos_helper (fun n dummy => Z.nonneg_pow_pos_helper 2 n dummy Z.lt_0_2) : zarith.
Global Hint Extern 1 (@eq Z _ _) => simple apply (fun b => f_equal (fun e => b ^ e)) : zarith.
Global Hint Extern 1 (@eq Z _ _) => simple apply (fun e => f_equal (fun b => b ^ e)) : zarith.
Global Hint Resolve Z.nonneg_pow_pos : zarith.
Global Hint Extern 1 => simple apply (fun n => Z.nonneg_pow_pos 2 n Z.lt_0_2) : zarith.
Global Hint Resolve Z.nonneg_pow_pos_helper : zarith.
Global Hint Extern 2 => simple apply (fun n dummy => Z.nonneg_pow_pos_helper 2 n dummy Z.lt_0_2) : zarith.
End Hints.

0 comments on commit d81081d

Please sign in to comment.