diff options
-rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 30 | ||||
-rw-r--r-- | src/Util/Tactics.v | 6 |
2 files changed, 21 insertions, 15 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index c863c2e8f..1723769e9 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -244,13 +244,13 @@ Section Pow2BaseProofs. clear limb_widths limb_widths_nonneg. Admitted. - + (* TODO : move *) Lemma pow2_mod_add_shiftl_low : forall a b n m, m <= n -> Z.pow2_mod (a + b << n) m = Z.pow2_mod a m. Proof. clear limb_widths limb_widths_nonneg. Admitted. - + (* TODO : move *) Lemma pow2_mod_subst : forall a n m, n <= m -> Z.pow2_mod a n = a -> Z.pow2_mod a m = Z.pow2_mod a n. Proof. @@ -261,7 +261,7 @@ Section Pow2BaseProofs. Lemma pow2_mod_0_r : forall a, Z.pow2_mod a 0 = 0. Proof. clear limb_widths limb_widths_nonneg. intros. - rewrite Z.pow2_mod_spec, Z.mod_1_r; reflexivity. + rewrite Z.pow2_mod_spec, Z.mod_1_r; reflexivity. Qed. Lemma digit_select : forall us i, bounded limb_widths us -> @@ -302,7 +302,7 @@ Section Pow2BaseProofs. rewrite <-Z.shiftl_mul_pow2 by auto using in_eq. rewrite bounded_iff in *. rewrite Z.shiftr_add_shiftl_high by first - [ pose proof (sum_firstn_nonnegative i lw); split; auto using in_eq; specialize_by auto; omega + [ pose proof (sum_firstn_nonnegative i lw); split; auto using in_eq; specialize_by auto using in_cons; omega | specialize (H 0%nat); rewrite !nth_default_cons in H; omega ]. rewrite IHus with (limb_widths := lw) by (auto using in_cons; rewrite ?bounded_iff; intro j; specialize (H (S j)); @@ -348,7 +348,7 @@ Section Pow2BaseProofs. | |- _ => rewrite sum_firstn_succ_default in *; pose proof (nth_default_limb_widths_nonneg i); omega end. - + Qed. Lemma testbit_decode_firstn_high : forall us i n, @@ -365,7 +365,7 @@ Section Pow2BaseProofs. | |- _ => rewrite testbit_pow2_mod | |- _ => break_if | |- _ => assumption - | |- _ => solve [auto] + | |- _ => solve [auto] | H : ?a <= ?b |- 0 <= ?b => assert (0 <= a) by (omega || auto); omega end. Qed. @@ -391,8 +391,8 @@ Section Pow2BaseProofs. repeat match goal with | |- _ => progress intros | |- _ => progress autorewrite with Ztestbit - | |- _ => progress change BaseSystem.decode with BaseSystem.decode' - | |- _ => rewrite sum_firstn_succ_default in * + | |- _ => progress change BaseSystem.decode with BaseSystem.decode' + | |- _ => rewrite sum_firstn_succ_default in * | |- _ => apply Z.bits_inj' | |- _ => break_if | |- appcontext [Z.testbit _ (?a - sum_firstn ?l ?i)] => @@ -723,7 +723,7 @@ Section UniformBase. Proof. induction n; destruct ls; boring. Qed. - + (* TODO : move *) Lemma firstn_base_from_limb_widths : forall n lw, firstn n (base_from_limb_widths lw) = base_from_limb_widths (firstn n lw). @@ -748,12 +748,12 @@ Section UniformBase. f_equal. transitivity x; [|symmetry]; eauto using in_eq, in_cons. Qed. - + Lemma decode_tl_base : forall us, (length us < length limb_widths)%nat -> BaseSystem.decode base us = BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us. Proof. intros. - match goal with |- BaseSystem.decode ?b1 _ = BaseSystem.decode ?b2 _ => + match goal with |- BaseSystem.decode ?b1 _ = BaseSystem.decode ?b2 _ => rewrite (decode_truncate_base b1), (decode_truncate_base b2) end. rewrite !firstn_base_from_limb_widths. do 2 f_equal. @@ -824,7 +824,7 @@ Section TestbitDecode. | |- _ => progress autorewrite with push_nth_default distr_length in * | |- _ => rewrite Nat.sub_diag | |- _ => rewrite sum_firstn_nil in * - | |- _ => rewrite sum_firstn_succ_cons in * + | |- _ => rewrite sum_firstn_succ_cons in * | |- _ => progress (simpl fst; simpl snd) | H : _ -> ?x < _ |- ?x < _ => eapply Z.lt_le_trans; [ apply H; omega | ] | |- ?xs # (?a - S ?b) <= (_ :: ?xs) # (?a - ?b) => @@ -844,10 +844,10 @@ Section TestbitDecode. | |- _ => progress (simpl fst; simpl snd) | |- appcontext[(fst (split_index' ?i (S ?idx) ?lw) - ?idx)%nat] => pose proof (split_index'_ge_index i (S idx) lw); - replace (fst (split_index' i (S idx) lw) - idx)%nat with + replace (fst (split_index' i (S idx) lw) - idx)%nat with (S (fst (split_index' i (S idx) lw) - S idx))%nat end. - Qed. + Qed. Context limb_widths (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w). Local Hint Resolve limb_widths_nonneg. @@ -870,7 +870,7 @@ Section TestbitDecode. repeat match goal with | |- _ => progress autorewrite with Ztestbit natsimplify in * | |- _ => erewrite digit_select by eassumption - | |- _ => break_if + | |- _ => break_if | |- _ => rewrite testbit_pow2_mod by auto using nth_default_limb_widths_nonneg | |- _ => omega | |- _ => f_equal; omega diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 4559a1757..880f5824a 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -252,6 +252,12 @@ Ltac specialize_by' tac := Ltac specialize_by tac := repeat specialize_by' tac. +(** [specialize_by auto] should not mean [specialize_by ltac:( auto + with * )]!!!!!!! (see + https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design + flaw. *) +Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac. + (** If [tac_in H] operates in [H] and leaves side-conditions before the original goal, then [side_conditions_before_to_side_conditions_after tac_in H] does |