diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-16 18:37:36 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-16 18:37:41 -0700 |
| commit | 42a122726ea5a1d42009718e965a9860fab83463 (patch) | |
| tree | 99a20d72367afc1f30b997aa663f03e82d7cbf7e /src/ModularArithmetic/Pow2BaseProofs.v | |
| parent | bc6311b1c912522e1babf593c5eb85a284cf564c (diff) | |
More 8.4 compat
Diffstat (limited to 'src/ModularArithmetic/Pow2BaseProofs.v')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 8a1de034a..d4ea129fb 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -49,8 +49,10 @@ Section Pow2BaseProofs. induction limb_widths as [|l ls IHls]; intros [|n]; try reflexivity. autorewrite with push_base_from_limb_widths push_firstn; boring. Qed. - Hint Rewrite <- @firstn_base_from_limb_widths : push_base_from_limb_widths pull_firstn. - Hint Rewrite @firstn_base_from_limb_widths : pull_base_from_limb_widths push_firstn. + Hint Rewrite <- @firstn_base_from_limb_widths : push_base_from_limb_widths. + Hint Rewrite <- @firstn_base_from_limb_widths : pull_firstn. + Hint Rewrite @firstn_base_from_limb_widths : pull_base_from_limb_widths. + Hint Rewrite @firstn_base_from_limb_widths : push_firstn. Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n. Proof. @@ -198,8 +200,10 @@ Section Pow2BaseProofs. unfold sum_firstn; autorewrite with natsimplify simpl_skipn simpl_firstn; reflexivity. Qed. - Hint Rewrite <- @skipn_base_from_limb_widths : push_base_from_limb_widths pull_skipn. - Hint Rewrite @skipn_base_from_limb_widths : pull_base_from_limb_widths push_skipn. + Hint Rewrite <- @skipn_base_from_limb_widths : push_base_from_limb_widths. + Hint Rewrite <- @skipn_base_from_limb_widths : pull_skipn. + Hint Rewrite @skipn_base_from_limb_widths : pull_base_from_limb_widths. + Hint Rewrite @skipn_base_from_limb_widths : push_skipn. Lemma pow2_mod_bounded :forall lw us i, (forall w, In w lw -> 0 <= w) -> bounded lw us -> Z.pow2_mod (nth_default 0 us i) (nth_default 0 lw i) = nth_default 0 us i. @@ -574,10 +578,14 @@ End Pow2BaseProofs. Hint Rewrite base_from_limb_widths_cons base_from_limb_widths_nil : push_base_from_limb_widths. Hint Rewrite <- base_from_limb_widths_cons : pull_base_from_limb_widths. -Hint Rewrite <- @firstn_base_from_limb_widths : push_base_from_limb_widths pull_firstn. -Hint Rewrite @firstn_base_from_limb_widths : pull_base_from_limb_widths push_firstn. -Hint Rewrite <- @skipn_base_from_limb_widths : push_base_from_limb_widths pull_skipn. -Hint Rewrite @skipn_base_from_limb_widths : pull_base_from_limb_widths push_skipn. +Hint Rewrite <- @firstn_base_from_limb_widths : push_base_from_limb_widths. +Hint Rewrite <- @firstn_base_from_limb_widths : pull_firstn. +Hint Rewrite @firstn_base_from_limb_widths : pull_base_from_limb_widths. +Hint Rewrite @firstn_base_from_limb_widths : push_firstn. +Hint Rewrite <- @skipn_base_from_limb_widths : push_base_from_limb_widths. +Hint Rewrite <- @skipn_base_from_limb_widths : pull_skipn. +Hint Rewrite @skipn_base_from_limb_widths : pull_base_from_limb_widths. +Hint Rewrite @skipn_base_from_limb_widths : push_skipn. Hint Rewrite @base_from_limb_widths_length : distr_length. Hint Rewrite @upper_bound_nil @upper_bound_cons @upper_bound_app using solve [ eauto with znonzero ] : push_upper_bound. |