diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-09-14 08:54:05 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-09-14 08:54:05 -0400 |
| commit | 6ae005c290f557a9a719792909edb93311f07dd5 (patch) | |
| tree | ac27ef42adb29e7345c3b4ae5fe6528fb530db90 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | da6198e85db84579511c6f636e540846790bb97d (diff) | |
Tweaked automation for 8.4 compatibility
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 0fe663049..fc1097b17 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -475,7 +475,6 @@ Section CanonicalizationProofs. (two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus). Local Hint Resolve (@limb_widths_nonneg _ prm) sum_firstn_limb_widths_nonneg. Local Hint Resolve log_cap_nonneg. - Local Notation pred := Init.Nat.pred. Lemma nth_default_carry_and_reduce_full : forall n i us, nth_default 0 (carry_and_reduce i us) n @@ -616,6 +615,11 @@ Section CanonicalizationProofs. auto using limb_widths_pos. Qed. + Lemma carry_sequence_nil_l : forall us, carry_sequence nil us = us. + Proof. + reflexivity. + Qed. + Ltac bound_during_loop := repeat match goal with @@ -625,7 +629,7 @@ Section CanonicalizationProofs. | |- _ => progress rewrite ?Z.add_0_r, ?Z.sub_0_r in * | |- _ => rewrite nth_default_carry_sequence_make_chain_full by auto | H : forall n, 0 <= _ [n] < _ |- appcontext [ _ [?n] ] => pose proof (H (pred n)); specialize (H n) - | |- appcontext [make_chain 0] => simpl make_chain; simpl carry_sequence + | |- appcontext [make_chain 0] => simpl make_chain; rewrite carry_sequence_nil_l | |- 0 <= ?a + c * ?b < 2 * ?d => unique assert (c * b <= d); [ | solve [pose proof c_pos; rewrite <-Z.add_diag; split; zero_bounds] ] | |- c * (?e >> (limb_widths[?i])) <= ?b => |