diff options
| -rw-r--r-- | src/BoundedArithmetic/BaseSystem.v | 175 | ||||
| -rw-r--r-- | src/BoundedArithmetic/BaseSystemProofs.v | 631 | ||||
| -rw-r--r-- | src/BoundedArithmetic/Double/Core.v | 6 | ||||
| -rw-r--r-- | src/BoundedArithmetic/Double/Proofs/Decode.v | 29 | ||||
| -rw-r--r-- | src/BoundedArithmetic/Pow2Base.v | 70 | ||||
| -rw-r--r-- | src/BoundedArithmetic/Pow2BaseProofs.v | 1036 |
6 files changed, 63 insertions, 1884 deletions
diff --git a/src/BoundedArithmetic/BaseSystem.v b/src/BoundedArithmetic/BaseSystem.v index 5d48c0977..e870e62fb 100644 --- a/src/BoundedArithmetic/BaseSystem.v +++ b/src/BoundedArithmetic/BaseSystem.v @@ -35,178 +35,5 @@ Section BaseSystem. Definition accumulate p acc := fst p * snd p + acc. Definition decode' bs u := fold_right accumulate 0 (combine u bs). Definition decode := decode' base. - - (* i is current index, counts down *) - Fixpoint encode' z max i : digits := - match i with - | O => nil - | S i' => let b := nth_default max base in - encode' z max i' ++ ((z mod (b i)) / (b i')) :: nil - end. - - (* max must be greater than input; this is used to truncate last digit *) - Definition encode z max := encode' z max (length base). - - Lemma decode'_truncate : forall bs us, decode' bs us = decode' bs (firstn (length bs) us). - Proof using Type. - unfold decode'; intros; f_equal; apply combine_truncate_l. - Qed. - - Fixpoint add (us vs:digits) : digits := - match us,vs with - | u::us', v::vs' => u+v :: add us' vs' - | _, nil => us - | _, _ => vs - end. - Infix ".+" := add. - - Hint Extern 1 (@eq Z _ _) => ring. - Definition mul_each u := map (Z.mul u). - Fixpoint sub (us vs:digits) : digits := - match us,vs with - | u::us', v::vs' => u-v :: sub us' vs' - | _, nil => us - | nil, v::vs' => (0-v)::sub nil vs' - end. - - Definition crosscoef i j : Z := - let b := nth_default 0 base in - (b(i) * b(j)) / b(i+j)%nat. - Hint Unfold crosscoef. - - Fixpoint zeros n := match n with O => nil | S n' => 0::zeros n' end. - - (* mul' is multiplication with the SECOND ARGUMENT REVERSED and OUTPUT REVERSED *) - Fixpoint mul_bi' (i:nat) (vsr:digits) := - match vsr with - | v::vsr' => v * crosscoef i (length vsr') :: mul_bi' i vsr' - | nil => nil - end. - Definition mul_bi (i:nat) (vs:digits) : digits := - zeros i ++ rev (mul_bi' i (rev vs)). - - (* mul' is multiplication with the FIRST ARGUMENT REVERSED *) - Fixpoint mul' (usr vs:digits) : digits := - match usr with - | u::usr' => - mul_each u (mul_bi (length usr') vs) .+ mul' usr' vs - | _ => nil - end. - Definition mul us := mul' (rev us). - -End BaseSystem. - -(* Example : polynomial base system *) -Section PolynomialBaseCoefs. - Context (b1 : positive) (baseLength : nat) (baseLengthNonzero : ltb 0 baseLength = true). - (** PolynomialBaseCoefs generates base vectors for [BaseSystem]. *) - Definition bi i := (Zpos b1)^(Z.of_nat i). - Definition poly_base := map bi (seq 0 baseLength). - - Lemma poly_b0_1 : forall x, nth_default x poly_base 0 = 1. - Proof using baseLengthNonzero. - - unfold poly_base, bi, nth_default. - case_eq baseLength; intros. { - assert ((0 < baseLength)%nat) by - (rewrite <-ltb_lt; apply baseLengthNonzero). - subst; omega. - } - auto. - Qed. - - Lemma poly_base_positive : forall b, In b poly_base -> b > 0. - Proof using Type. - unfold poly_base. - intros until 0; intro H. - rewrite in_map_iff in *. - destruct H; destruct H. - subst. - apply Z.pos_pow_nat_pos. - Qed. - - Lemma poly_base_defn : forall i, (i < length poly_base)%nat -> - nth_default 0 poly_base i = bi i. - Proof using Type. - unfold poly_base, nth_default; nth_tac. - Qed. - - Lemma poly_base_succ : - forall i, ((S i) < length poly_base)%nat -> - let b := nth_default 0 poly_base in - let r := (b (S i) / b i) in - b (S i) = r * b i. - Proof using Type. - intros; subst b; subst r. - repeat rewrite poly_base_defn in * by omega. - unfold bi. - replace (Z.pos b1 ^ Z.of_nat (S i)) - with (Z.pos b1 * (Z.pos b1 ^ Z.of_nat i)) by - (rewrite Nat2Z.inj_succ; rewrite <- Z.pow_succ_r; intuition auto with zarith). - replace (Z.pos b1 * Z.pos b1 ^ Z.of_nat i / Z.pos b1 ^ Z.of_nat i) - with (Z.pos b1); auto. - rewrite Z_div_mult_full; auto. - apply Z.pow_nonzero; intuition auto with lia. - Qed. - - Lemma poly_base_good: - forall i j, (i + j < length poly_base)%nat -> - let b := nth_default 0 poly_base in - let r := (b i * b j) / b (i+j)%nat in - b i * b j = r * b (i+j)%nat. - Proof using Type. - unfold poly_base, nth_default; nth_tac. - - clear. - unfold bi. - rewrite Nat2Z.inj_add, Zpower_exp by - (replace 0 with (Z.of_nat 0) by auto; rewrite <- Nat2Z.inj_ge; omega). - rewrite Z_div_same_full; try ring. - rewrite <- Z.neq_mul_0. - split; apply Z.pow_nonzero; try apply Zle_0_nat; try solve [intro H; inversion H]. - Qed. - - Instance PolyBaseVector : BaseVector poly_base := { - base_positive := poly_base_positive; - b0_1 := poly_b0_1; - base_good := poly_base_good - }. - -End PolynomialBaseCoefs. - -Import ListNotations. - -Section BaseSystemExample. - Definition baseLength := 32%nat. - Lemma baseLengthNonzero : ltb 0 baseLength = true. - compute; reflexivity. - Qed. - Definition base2 := poly_base 2 baseLength. - - Example three_times_two : mul base2 [1;1;0] [0;1;0] = [0;1;1;0;0]. - Proof. - reflexivity. - Qed. - - (* python -c "e = lambda x: '['+''.join(reversed(bin(x)[2:])).replace('1','1;').replace('0','0;')[:-1]+']'; print(e(19259)); print(e(41781))" *) - Definition a := [1;1;0;1;1;1;0;0;1;1;0;1;0;0;1]. - Definition b := [1;0;1;0;1;1;0;0;1;1;0;0;0;1;0;1]. - Example da : decode base2 a = 19259. - Proof. - reflexivity. - Qed. - Example db : decode base2 b = 41781. - Proof. - reflexivity. - Qed. - Example encoded_ab : - mul base2 a b =[1;1;1;2;2;4;2;2;4;5;3;3;3;6;4;2;5;3;4;3;2;1;2;2;2;0;1;1;0;1]. - Proof. - reflexivity. - Qed. - Example dab : decode base2 (mul base2 a b) = 804660279. - Proof. - reflexivity. - Qed. -End BaseSystemExample. +End BaseSystem.
\ No newline at end of file diff --git a/src/BoundedArithmetic/BaseSystemProofs.v b/src/BoundedArithmetic/BaseSystemProofs.v index 409d8b7db..9eb694778 100644 --- a/src/BoundedArithmetic/BaseSystemProofs.v +++ b/src/BoundedArithmetic/BaseSystemProofs.v @@ -2,13 +2,12 @@ Require Import Coq.Lists.List Coq.micromega.Psatz. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. -Require Import Crypto.BaseSystem. +Require Import Crypto.BoundedArithmetic.BaseSystem. +Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Notations. Import Morphisms. Local Open Scope Z. -Local Infix ".+" := add. - Local Hint Extern 1 (@eq Z _ _) => ring. Section BaseSystemProofs. @@ -31,11 +30,6 @@ Section BaseSystemProofs. apply Z.add_assoc. Qed. - Lemma add_rep : forall bs us vs, decode' bs (add us vs) = decode' bs us + decode' bs vs. - Proof using Type. - unfold decode', accumulate; induction bs; destruct us, vs; boring; ring. - Qed. - Lemma decode_nil : forall bs, decode' bs nil = 0. Proof using Type. @@ -48,8 +42,6 @@ Section BaseSystemProofs. intros; rewrite decode'_truncate; auto. Qed. - Hint Rewrite decode_base_nil. - Lemma mul_each_rep : forall bs u vs, decode' bs (mul_each u vs) = u * decode' bs vs. Proof using Type. @@ -93,31 +85,6 @@ Section BaseSystemProofs. unfold decode; intros; apply decode'_map_mul. Qed. - Lemma sub_rep : forall bs us vs, decode' bs (sub us vs) = decode' bs us - decode' bs vs. - Proof using Type. - induction bs; destruct us; destruct vs; boring; ring. - Qed. - - Lemma nth_default_base_nonzero : forall d, d <> 0 -> - forall i, nth_default d base i <> 0. - Proof using Type*. - intros. - rewrite nth_default_eq. - destruct (nth_in_or_default i base d). - + auto using Z.positive_is_nonzero, base_positive. - + congruence. - Qed. - - Lemma nth_default_base_pos : forall d, 0 < d -> - forall i, 0 < nth_default d base i. - Proof using Type*. - intros. - rewrite nth_default_eq. - destruct (nth_in_or_default i base d). - + apply Z.gt_lt; auto using base_positive. - + congruence. - Qed. - Lemma mul_each_base : forall us bs c, decode' bs (mul_each c us) = decode' (mul_each c bs) us. Proof using Type. @@ -128,583 +95,39 @@ Section BaseSystemProofs. Hint Rewrite (@firstn_nil Z). Hint Rewrite (@skipn_nil Z). - Lemma base_app : forall us low high, - decode' (low ++ high) us = decode' low (firstn (length low) us) + decode' high (skipn (length low) us). - Proof using Type. - induction us; destruct low; boring. - Qed. - - Lemma base_mul_app : forall low c us, - decode' (low ++ mul_each c low) us = decode' low (firstn (length low) us) + - c * decode' low (skipn (length low) us). - Proof using Type. - intros. - rewrite base_app; f_equal. - rewrite <- mul_each_rep. - rewrite mul_each_base. - reflexivity. - Qed. - - Lemma zeros_rep : forall bs n, decode' bs (zeros n) = 0. - Proof using Type. - - induction bs; destruct n; boring. - Qed. - Lemma length_zeros : forall n, length (zeros n) = n. - Proof using Type. - - induction n; boring. - Qed. - Hint Rewrite length_zeros. - - Lemma app_zeros_zeros : forall n m, zeros n ++ zeros m = zeros (n + m)%nat. - Proof using Type. - induction n; boring. - Qed. - Hint Rewrite app_zeros_zeros. - - Lemma zeros_app0 : forall m, zeros m ++ 0 :: nil = zeros (S m). - Proof using Type. - induction m; boring. - Qed. - Hint Rewrite zeros_app0. - - Lemma nth_default_zeros : forall n i, nth_default 0 (BaseSystem.zeros n) i = 0. - Proof using Type. - induction n; intros; [ cbv [BaseSystem.zeros]; apply nth_default_nil | ]. - rewrite <-zeros_app0, nth_default_app. - rewrite length_zeros. - destruct (lt_dec i n); auto. - destruct (eq_nat_dec i n); subst. - + rewrite Nat.sub_diag; apply nth_default_cons. - + apply nth_default_out_of_bounds. - cbv [length]; omega. - Qed. - - Lemma rev_zeros : forall n, rev (zeros n) = zeros n. - Proof using Type. - induction n; boring. - Qed. - Hint Rewrite rev_zeros. - - Hint Unfold nth_default. - - Lemma decode_single : forall n bs x, - decode' bs (zeros n ++ x :: nil) = nth_default 0 bs n * x. - Proof using Type. - induction n; destruct bs; boring. - Qed. - Hint Rewrite decode_single. - Lemma peel_decode : forall xs ys x y, decode' (x::xs) (y::ys) = x*y + decode' xs ys. Proof using Type. boring. Qed. - Hint Rewrite zeros_rep peel_decode. - - Lemma decode_Proper : Proper (Logic.eq ==> (Forall2 Logic.eq) ==> Logic.eq) decode'. - Proof using Type. - repeat intro; subst. - revert y y0 H0; induction x0; intros. - + inversion H0. rewrite !decode_nil. - reflexivity. - + inversion H0; subst. - destruct y as [|y0 y]; [rewrite !decode_base_nil; reflexivity | ]. - specialize (IHx0 y _ H4). - rewrite !peel_decode. - f_equal; auto. - Qed. - - Lemma decode_highzeros : forall xs bs n, decode' bs (xs ++ zeros n) = decode' bs xs. - Proof using Type. - induction xs; destruct bs; boring. - Qed. - - Lemma mul_bi'_zeros : forall n m, mul_bi' base n (zeros m) = zeros m. - Proof using Type. - - induction m; boring. - Qed. - Hint Rewrite mul_bi'_zeros. - - Lemma nth_error_base_nonzero : forall n x, - nth_error base n = Some x -> x <> 0. - Proof using Type*. - eauto using (@nth_error_value_In Z), Z.gt0_neq0, base_positive. - Qed. + Hint Rewrite peel_decode. Hint Rewrite plus_0_r. - Lemma mul_bi_single : forall m n x, - (n + m < length base)%nat -> - decode base (mul_bi base n (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n. - Proof using Type*. - unfold mul_bi, decode. - destruct m; simpl; simpl_list; simpl; intros. { - pose proof nth_error_base_nonzero as nth_nonzero. - case_eq base; [intros; boring | intros z l base_eq]. - specialize (b0_1 0); intro b0_1'. - rewrite base_eq in *. - rewrite nth_default_cons in b0_1'. - rewrite b0_1' in *. - unfold crosscoef. - autounfold; autorewrite with core. - unfold nth_default. - nth_tac. - rewrite Z.mul_1_r. - rewrite Z_div_same_full. - destruct x; ring. - eapply nth_nonzero; eauto. - } { - ssimpl_list. - autorewrite with core. - rewrite app_assoc. - autorewrite with core. - unfold crosscoef; simpl; ring_simplify. - rewrite Nat.add_1_r. - rewrite base_good by auto. - rewrite Z_div_mult by (apply base_positive; rewrite nth_default_eq; apply nth_In; auto). - rewrite <- Z.mul_assoc. - rewrite <- Z.mul_comm. - rewrite <- Z.mul_assoc. - rewrite <- Z.mul_assoc. - destruct (Z.eq_dec x 0); subst; try ring. - rewrite Z.mul_cancel_l by auto. - rewrite <- base_good by auto. - ring. - } - Qed. - - Lemma set_higher' : forall vs x, vs++x::nil = vs .+ (zeros (length vs) ++ x :: nil). - Proof using Type. - - induction vs; boring; f_equal; ring. - Qed. - Lemma set_higher : forall bs vs x, decode' bs (vs++x::nil) = decode' bs vs + nth_default 0 bs (length vs) * x. Proof using Type. intros. - rewrite set_higher'. - rewrite add_rep. - f_equal. - apply decode_single. - Qed. - - Lemma zeros_plus_zeros : forall n, zeros n = zeros n .+ zeros n. - Proof using Type. - - induction n; auto. - simpl; f_equal; auto. - Qed. - - Lemma mul_bi'_n_nil : forall n, mul_bi' base n nil = nil. - Proof using Type. - unfold mul_bi; auto. - Qed. - Hint Rewrite mul_bi'_n_nil. - - Lemma add_nil_l : forall us, nil .+ us = us. - Proof using Type. - - induction us; auto. - Qed. - Hint Rewrite add_nil_l. - - Lemma add_nil_r : forall us, us .+ nil = us. - Proof using Type. - - induction us; auto. - Qed. - Hint Rewrite add_nil_r. - - Lemma add_first_terms : forall us vs a b, - (a :: us) .+ (b :: vs) = (a + b) :: (us .+ vs). - Proof using Type. - - auto. - Qed. - Hint Rewrite add_first_terms. - - Lemma mul_bi'_cons : forall n x us, - mul_bi' base n (x :: us) = x * crosscoef base n (length us) :: mul_bi' base n us. - Proof using Type. - unfold mul_bi'; auto. - Qed. - - Lemma add_same_length : forall us vs l, (length us = l) -> (length vs = l) -> - length (us .+ vs) = l. - Proof using Type. - induction us, vs; boring. - erewrite (IHus vs (pred l)); boring. - Qed. - - Hint Rewrite app_nil_l. - Hint Rewrite app_nil_r. - - Lemma add_snoc_same_length : forall l us vs a b, - (length us = l) -> (length vs = l) -> - (us ++ a :: nil) .+ (vs ++ b :: nil) = (us .+ vs) ++ (a + b) :: nil. - Proof using Type. - induction l, us, vs; boring; discriminate. - Qed. - - Lemma mul_bi'_add : forall us n vs l - (Hlus: length us = l) - (Hlvs: length vs = l), - mul_bi' base n (rev (us .+ vs)) = - mul_bi' base n (rev us) .+ mul_bi' base n (rev vs). - Proof using Type. - (* TODO(adamc): please help prettify this *) - induction us using rev_ind; - try solve [destruct vs; boring; congruence]. - destruct vs using rev_ind; boring; clear IHvs; simpl_list. - erewrite (add_snoc_same_length (pred l) us vs _ _); simpl_list. - repeat rewrite mul_bi'_cons; rewrite add_first_terms; simpl_list. - rewrite (IHus n vs (pred l)). - replace (length us) with (pred l). - replace (length vs) with (pred l). - rewrite (add_same_length us vs (pred l)). - f_equal; ring. - - erewrite length_snoc; eauto. - erewrite length_snoc; eauto. - erewrite length_snoc; eauto. - erewrite length_snoc; eauto. - erewrite length_snoc; eauto. - erewrite length_snoc; eauto. - erewrite length_snoc; eauto. - erewrite length_snoc; eauto. - Qed. - - Lemma zeros_cons0 : forall n, 0 :: zeros n = zeros (S n). - Proof using Type. - - auto. - Qed. - - Lemma add_leading_zeros : forall n us vs, - (zeros n ++ us) .+ (zeros n ++ vs) = zeros n ++ (us .+ vs). - Proof using Type. - induction n; boring. - Qed. - - Lemma rev_add_rev : forall us vs l, (length us = l) -> (length vs = l) -> - (rev us) .+ (rev vs) = rev (us .+ vs). - Proof using Type. - induction us, vs; boring; try solve [subst; discriminate]. - rewrite (add_snoc_same_length (pred l) _ _ _ _) by (subst; simpl_list; omega). - rewrite (IHus vs (pred l)) by omega; auto. - Qed. - Hint Rewrite rev_add_rev. - - Lemma mul_bi'_length : forall us n, length (mul_bi' base n us) = length us. - Proof using Type. - induction us, n; boring. - Qed. - Hint Rewrite mul_bi'_length. - - Lemma add_comm : forall us vs, us .+ vs = vs .+ us. - Proof using Type. - induction us, vs; boring; f_equal; auto. - Qed. - - Hint Rewrite rev_length. - - Lemma mul_bi_add_same_length : forall n us vs l, - (length us = l) -> (length vs = l) -> - mul_bi base n (us .+ vs) = mul_bi base n us .+ mul_bi base n vs. - Proof using Type. - unfold mul_bi; boring. - rewrite add_leading_zeros. - erewrite mul_bi'_add; boring. - erewrite rev_add_rev; boring. - Qed. - - Lemma add_zeros_same_length : forall us, us .+ (zeros (length us)) = us. - Proof using Type. - induction us; boring; f_equal; omega. - Qed. - - Hint Rewrite add_zeros_same_length. - Hint Rewrite minus_diag. - - Lemma add_trailing_zeros : forall us vs, (length us >= length vs)%nat -> - us .+ vs = us .+ (vs ++ (zeros (length us - length vs)%nat)). - Proof using Type. - induction us, vs; boring; f_equal; boring. - Qed. - - Lemma length_add_ge : forall us vs, (length us >= length vs)%nat -> - (length (us .+ vs) <= length us)%nat. - Proof using Type. - intros. - rewrite add_trailing_zeros by trivial. - erewrite add_same_length by (pose proof app_length; boring); omega. - Qed. - - Lemma add_length_le_max : forall us vs, - (length (us .+ vs) <= max (length us) (length vs))%nat. - Proof using Type. - intros; case_max; (rewrite add_comm; apply length_add_ge; omega) || - (apply length_add_ge; omega) . - Qed. - - Lemma sub_nil_length: forall us : digits, length (sub nil us) = length us. - Proof using Type. - induction us; boring. - Qed. - - Lemma sub_length : forall us vs, - (length (sub us vs) = max (length us) (length vs))%nat. - Proof using Type. - induction us, vs; boring. - rewrite sub_nil_length; auto. - Qed. - - Lemma mul_bi_length : forall us n, length (mul_bi base n us) = (length us + n)%nat. - Proof using Type. - pose proof mul_bi'_length; unfold mul_bi. - destruct us; repeat progress (simpl_list; boring). - Qed. - Hint Rewrite mul_bi_length. - - Lemma mul_bi_trailing_zeros : forall m n us, - mul_bi base n us ++ zeros m = mul_bi base n (us ++ zeros m). - Proof using Type. - unfold mul_bi. - induction m; intros; try solve [boring]. - rewrite <- zeros_app0. - rewrite app_assoc. - repeat progress (boring; rewrite rev_app_distr). - Qed. - - Lemma mul_bi_add_longer : forall n us vs, - (length us >= length vs)%nat -> - mul_bi base n (us .+ vs) = mul_bi base n us .+ mul_bi base n vs. - Proof using Type. - boring. - rewrite add_trailing_zeros by auto. - rewrite (add_trailing_zeros (mul_bi base n us) (mul_bi base n vs)) - by (repeat (rewrite mul_bi_length); omega). - erewrite mul_bi_add_same_length by - (eauto; simpl_list; rewrite length_zeros; omega). - rewrite mul_bi_trailing_zeros. - repeat (f_equal; boring). - Qed. - - Lemma mul_bi_add : forall n us vs, - mul_bi base n (us .+ vs) = (mul_bi base n us) .+ (mul_bi base n vs). - Proof using Type. - intros; pose proof mul_bi_add_longer. - destruct (le_ge_dec (length us) (length vs)). { - rewrite add_comm. - rewrite (add_comm (mul_bi base n us)). - boring. - } { - boring. - } - Qed. - - Lemma mul_bi_rep : forall i vs, - (i + length vs < length base)%nat -> - decode base (mul_bi base i vs) = decode base vs * nth_default 0 base i. - Proof using Type*. - unfold decode. - induction vs using rev_ind; intros; try solve [unfold mul_bi; boring]. - assert (i + length vs < length base)%nat by - (rewrite app_length in *; boring). - - rewrite set_higher. - ring_simplify. - rewrite <- IHvs by auto; clear IHvs. - rewrite <- mul_bi_single by auto. - rewrite <- add_rep. - rewrite <- mul_bi_add. - rewrite set_higher'. - auto. - Qed. - - Local Notation mul' := (mul' base). - Local Notation mul := (mul base). - - Lemma mul'_rep : forall us vs, - (length us + length vs <= length base)%nat -> - decode base (mul' (rev us) vs) = decode base us * decode base vs. - Proof using Type*. - unfold decode. - induction us using rev_ind; boring. - - assert (length us + length vs < length base)%nat by - (rewrite app_length in *; boring). - - ssimpl_list. - rewrite add_rep. - boring. - rewrite set_higher. - rewrite mul_each_rep. - rewrite mul_bi_rep by auto. - unfold decode; ring. - Qed. - - Lemma mul_rep : forall us vs, - (length us + length vs <= length base)%nat -> - decode base (mul us vs) = decode base us * decode base vs. - Proof using Type*. - exact mul'_rep. - Qed. - - Lemma mul'_length: forall us vs, - (length (mul' us vs) <= length us + length vs)%nat. - Proof using Type. - pose proof add_length_le_max. - induction us; boring. - unfold mul_each. - simpl_list; case_max; boring; omega. - Qed. - - Lemma mul_length: forall us vs, - (length (mul us vs) <= length us + length vs)%nat. - Proof using Type. - intros; unfold BaseSystem.mul. - rewrite mul'_length. - rewrite rev_length; omega. - Qed. - - Lemma add_length_exact : forall us vs, - length (us .+ vs) = max (length us) (length vs). - Proof using Type. - induction us; destruct vs; boring. - Qed. - - Hint Rewrite add_length_exact : distr_length. - - Lemma mul'_length_exact_full: forall us vs, - (length (mul' us vs) = match length us with - | 0 => 0%nat - | _ => pred (length us + length vs) - end)%nat. - Proof using Type. - induction us; intros; try solve [boring]. - unfold BaseSystem.mul'; fold mul'. - unfold mul_each. - rewrite add_length_exact, map_length, mul_bi_length, length_cons. - destruct us. - + rewrite Max.max_0_r. simpl; omega. - + rewrite Max.max_l; [ omega | ]. - rewrite IHus by ( congruence || simpl in *; omega). - simpl; omega. - Qed. - - Hint Rewrite mul'_length_exact_full : distr_length. - - (* TODO(@jadephilipoom, from jgross): one of these conditions isn't - needed. Should it be dropped, or was there a reason to keep it? *) - Lemma mul'_length_exact: forall us vs, - (length us <= length vs)%nat -> us <> nil -> - (length (mul' us vs) = pred (length us + length vs))%nat. - Proof using Type. - intros; rewrite mul'_length_exact_full; destruct us; simpl; congruence. - Qed. - - Lemma mul_length_exact_full: forall us vs, - (length (mul us vs) = match length us with - | 0 => 0 - | _ => pred (length us + length vs) - end)%nat. - Proof using Type. - intros; unfold BaseSystem.mul; autorewrite with distr_length; reflexivity. - Qed. - - Hint Rewrite mul_length_exact_full : distr_length. - - (* TODO(@jadephilipoom, from jgross): one of these conditions isn't - needed. Should it be dropped, or was there a reason to keep it? *) - Lemma mul_length_exact: forall us vs, - (length us <= length vs)%nat -> us <> nil -> - (length (mul us vs) = pred (length us + length vs))%nat. - Proof using Type. - intros; unfold BaseSystem.mul. - rewrite mul'_length_exact; rewrite ?rev_length; try omega. - intro rev_nil. - match goal with H : us <> nil |- _ => apply H end. - apply length0_nil; rewrite <-rev_length, rev_nil. - reflexivity. - Qed. - Definition encode'_zero z max : encode' base z max 0%nat = nil := eq_refl. - Definition encode'_succ z max i : encode' base z max (S i) = - encode' base z max i ++ ((z mod (nth_default max base (S i))) / (nth_default max base i)) :: nil := eq_refl. - Opaque encode'. - Hint Resolve encode'_zero encode'_succ. - - Lemma encode'_length : forall z max i, length (encode' base z max i) = i. - Proof using Type. - induction i; auto. - rewrite encode'_succ, app_length, IHi. - cbv [length]. - omega. - Qed. - - (* States that each element of the base is a positive integer multiple of the previous - element, and that max is a positive integer multiple of the last element. Ideally this - would have a better name. *) - Definition base_max_succ_divide max := forall i, (S i <= length base)%nat -> - Z.divide (nth_default max base i) (nth_default max base (S i)). - - Lemma encode'_spec : forall z max, 0 < max -> - base_max_succ_divide max -> forall i, (i <= length base)%nat -> - decode' base (encode' base z max i) = z mod (nth_default max base i). - Proof using Type*. - induction i; intros. - + rewrite encode'_zero, b0_1, Z.mod_1_r. - apply decode_nil. - + rewrite encode'_succ, set_higher. - rewrite IHi by omega. - rewrite encode'_length, (Z.add_comm (z mod nth_default max base i)). - replace (nth_default 0 base i) with (nth_default max base i) by - (rewrite !nth_default_eq; apply nth_indep; omega). - match goal with H1 : base_max_succ_divide _, H2 : (S i <= length base)%nat, H3 : 0 < max |- _ => - specialize (H1 i H2); - rewrite (Znumtheory.Zmod_div_mod _ _ _ (nth_default_base_pos _ H _) - (nth_default_base_pos _ H _) H0) end. - rewrite <-Z.div_mod by (apply Z.positive_is_nonzero, Z.lt_gt; auto using nth_default_base_pos). - reflexivity. - Qed. - - Lemma encode_rep : forall z max, 0 <= z < max -> - base_max_succ_divide max -> decode base (encode base z max) = z. - Proof using Type*. - unfold encode; intros. - rewrite encode'_spec, nth_default_out_of_bounds by (omega || auto). - apply Z.mod_small; omega. - Qed. - -End BaseSystemProofs. - -Hint Rewrite @add_length_exact @mul'_length_exact_full @mul_length_exact_full @encode'_length @sub_length : distr_length. - -Section MultiBaseSystemProofs. - Context base0 (base_vector0 : @BaseVector base0) base1 (base_vector1 : @BaseVector base1). - - Lemma decode_short_initial : forall (us : digits), - (firstn (length us) base0 = firstn (length us) base1) - -> decode base0 us = decode base1 us. - Proof using Type. - intros us H. - unfold decode, decode'. - rewrite (combine_truncate_r us base0), (combine_truncate_r us base1), H. - reflexivity. - Qed. - - Lemma mul_rep_two_base : forall (us vs : digits), - (length us + length vs <= length base1)%nat - -> firstn (length us) base0 = firstn (length us) base1 - -> firstn (length vs) base0 = firstn (length vs) base1 - -> (decode base0 us) * (decode base0 vs) = decode base1 (mul base1 us vs). - Proof using base_vector1. - intros. - rewrite mul_rep by trivial. - apply f_equal2; apply decode_short_initial; assumption. - Qed. - -End MultiBaseSystemProofs. + rewrite !decode'_splice. + cbv [decode' nth_default]; break_match; ring_simplify; + match goal with + | [H:_ |- _] => unique pose proof (nth_error_error_length _ _ _ H) + | [H:_ |- _] => unique pose proof (nth_error_value_length _ _ _ _ H) + end; + repeat match goal with + | _ => solve [simpl;ring_simplify; trivial] + | _ => progress ring_simplify + | _ => progress rewrite skipn_all by trivial + | _ => progress rewrite combine_nil_r + | _ => progress rewrite firstn_all2 by trivial + end. + rewrite (combine_truncate_r vs bs); apply (f_equal2 Z.add); trivial; []. + unfold combine; break_match. + { apply (f_equal (@length _)) in Heql; simpl length in Heql; rewrite skipn_length in Heql; omega. } + { cbv -[Z.add Z.mul]; ring_simplify; f_equal. + assert (HH: nth_error (z0 :: l) 0 = Some z) by + ( + pose proof @nth_error_skipn _ (length vs) bs 0; + rewrite plus_0_r in *; + congruence); simpl in HH; congruence. } + Qed. +End BaseSystemProofs.
\ No newline at end of file diff --git a/src/BoundedArithmetic/Double/Core.v b/src/BoundedArithmetic/Double/Core.v index 6b6726f77..bf4de044d 100644 --- a/src/BoundedArithmetic/Double/Core.v +++ b/src/BoundedArithmetic/Double/Core.v @@ -2,13 +2,15 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.BoundedArithmetic.Interface. Require Import Crypto.BoundedArithmetic.InterfaceProofs. -Require Import Crypto.BoundedArithmetic.Pow2Base. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Notations. Require Import Crypto.Util.LetIn. Import Bug5107WorkAround. +Require Crypto.BoundedArithmetic.BaseSystem. +Require Crypto.BoundedArithmetic.Pow2Base. + Local Open Scope nat_scope. Local Open Scope Z_scope. Local Open Scope type_scope. @@ -18,7 +20,7 @@ Local Notation eta x := (fst x, snd x). (** The list is low to high; the tuple is low to high *) Definition tuple_decoder {n W} {decode : decoder n W} {k : nat} : decoder (k * n) (tuple W k) - := {| decode w := BaseSystem.decode (base_from_limb_widths (repeat n k)) + := {| decode w := BaseSystem.decode (Pow2Base.base_from_limb_widths (repeat n k)) (List.map decode (List.rev (Tuple.to_list _ w))) |}. Global Arguments tuple_decoder : simpl never. Hint Extern 3 (decoder _ (tuple ?W ?k)) => let kv := (eval simpl in (Z.of_nat k)) in apply (fun n decode => (@tuple_decoder n W decode k : decoder (kv * n) (tuple W k))) : typeclass_instances. diff --git a/src/BoundedArithmetic/Double/Proofs/Decode.v b/src/BoundedArithmetic/Double/Proofs/Decode.v index a84e84acf..04c90e835 100644 --- a/src/BoundedArithmetic/Double/Proofs/Decode.v +++ b/src/BoundedArithmetic/Double/Proofs/Decode.v @@ -1,15 +1,15 @@ Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.micromega.Psatz. Require Import Crypto.BoundedArithmetic.Interface. Require Import Crypto.BoundedArithmetic.InterfaceProofs. -Require Import Crypto.BaseSystem. -Require Import Crypto.BoundedArithmetic.Pow2Base. -Require Import Crypto.BoundedArithmetic.Pow2BaseProofs. Require Import Crypto.BoundedArithmetic.Double.Core. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Notations. +Require Crypto.BoundedArithmetic.Pow2Base. +Require Crypto.BoundedArithmetic.Pow2BaseProofs. + Local Open Scope nat_scope. Local Open Scope type_scope. @@ -25,10 +25,10 @@ Section decode. Local Notation limb_widths := (repeat n k). Lemma decode_bounded {isdecode : is_decode decode} w - : 0 <= n -> bounded limb_widths (List.map decode (rev (to_list k w))). + : 0 <= n -> Pow2Base.bounded limb_widths (List.map decode (rev (to_list k w))). Proof using Type. intro. - eapply bounded_uniform; try solve [ eauto using repeat_spec ]. + eapply Pow2BaseProofs.bounded_uniform; try solve [ eauto using repeat_spec ]. { distr_length. } { intros z H'. apply in_map_iff in H'. @@ -42,20 +42,20 @@ Section decode. unfold tuple_decoder; hnf; simpl. intro w. destruct (zerop k); [ subst | ]. - { unfold BaseSystem.decode, BaseSystem.decode'; simpl; omega. } + { cbv; intuition congruence. } assert (0 <= n) by (destruct k as [ | [|] ]; [ omega | | destruct w ]; eauto using decode_exponent_nonnegative). - replace (2^(k * n)) with (upper_bound limb_widths) - by (erewrite upper_bound_uniform by eauto using repeat_spec; distr_length). - apply decode_upper_bound; auto using decode_bounded. + replace (2^(k * n)) with (Pow2Base.upper_bound limb_widths) + by (erewrite Pow2BaseProofs.upper_bound_uniform by eauto using repeat_spec; distr_length). + apply Pow2BaseProofs.decode_upper_bound; auto using decode_bounded. { intros ? H'. apply repeat_spec in H'; omega. } { distr_length. } Qed. End with_k. - Local Arguments base_from_limb_widths : simpl never. + Local Arguments Pow2Base.base_from_limb_widths : simpl never. Local Arguments repeat : simpl never. Local Arguments Z.mul !_ !_. Lemma tuple_decoder_S {k} w : 0 <= n -> (tuple_decoder (k := S (S k)) w = tuple_decoder (k := S k) (fst w) + (decode (snd w) << (S k * n)))%Z. @@ -64,16 +64,15 @@ Section decode. destruct w as [? w]; simpl. replace (decode w) with (decode w * 1 + 0)%Z by omega. rewrite map_app, map_cons, map_nil. - erewrite decode_shift_uniform_app by (eauto using repeat_spec; distr_length). + erewrite Pow2BaseProofs.decode_shift_uniform_app by (eauto using repeat_spec; distr_length). distr_length. autorewrite with push_skipn natsimplify push_firstn. reflexivity. Qed. Global Instance tuple_decoder_O w : tuple_decoder (k := 1) w =~> decode w. Proof using Type. - unfold tuple_decoder, BaseSystem.decode, BaseSystem.decode', accumulate, base_from_limb_widths, repeat. - simpl; hnf. - omega. + cbv [tuple_decoder BoundedArithmetic.BaseSystem.decode BoundedArithmetic.BaseSystem.decode' BoundedArithmetic.BaseSystem.accumulate Pow2Base.base_from_limb_widths repeat]. + simpl; hnf; lia. Qed. Global Instance tuple_decoder_m1 w : tuple_decoder (k := 0) w =~> 0. Proof using Type. reflexivity. Qed. @@ -92,7 +91,7 @@ Section decode. : (P _ (tuple_decoder (k := 1)) -> P _ decode) * (P _ decode -> P _ (tuple_decoder (k := 1))). Proof using Type. - unfold tuple_decoder, BaseSystem.decode, BaseSystem.decode', accumulate, base_from_limb_widths, repeat. + unfold tuple_decoder, BaseSystem.decode, BaseSystem.decode', BaseSystem.accumulate, Pow2Base.base_from_limb_widths, repeat. simpl; hnf. rewrite Z.mul_1_l. split; apply P_ext; simpl; intro; autorewrite with zsimplify_const; reflexivity. diff --git a/src/BoundedArithmetic/Pow2Base.v b/src/BoundedArithmetic/Pow2Base.v index 0175018f8..62f1f742d 100644 --- a/src/BoundedArithmetic/Pow2Base.v +++ b/src/BoundedArithmetic/Pow2Base.v @@ -1,7 +1,6 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.ZUtil. -Require Crypto.BaseSystem. Require Import Coq.Lists.List. Local Open Scope Z_scope. @@ -9,81 +8,12 @@ Local Open Scope Z_scope. Section Pow2Base. Context (limb_widths : list Z). Local Notation "w[ i ]" := (nth_default 0 limb_widths i). - Fixpoint base_from_limb_widths limb_widths := match limb_widths with | nil => nil | w :: lw => 1 :: map (Z.mul (two_p w)) (base_from_limb_widths lw) end. - Local Notation base := (base_from_limb_widths limb_widths). - - Definition bounded us := forall i, 0 <= nth_default 0 us i < 2 ^ w[i]. - Definition upper_bound := 2 ^ (sum_firstn limb_widths (length limb_widths)). - - Function decode_bitwise' us i acc := - match i with - | O => acc - | S i' => decode_bitwise' us i' (Z.lor (nth_default 0 us i') (Z.shiftl acc w[i'])) - end. - - Definition decode_bitwise us := decode_bitwise' us (length us) 0. - - (* i is current index, counts down *) - Fixpoint encode' z i := - match i with - | O => nil - | S i' => let lw := sum_firstn limb_widths in - encode' z i' ++ (Z.shiftr (Z.land z (Z.ones (lw i))) (lw i')) :: nil - end. - - Definition encodeZ x:= encode' x (length limb_widths). - - (** ** Carrying *) - Section carrying. - (** Here we implement addition and multiplication with simple - carrying. *) - Notation log_cap i := (nth_default 0 limb_widths i). - - Definition add_to_nth n (x:Z) xs := - update_nth n (fun y => x + y) xs. - Definition carry_single i := fun di => - (Z.pow2_mod di (log_cap i), - Z.shiftr di (log_cap i)). - - (* [fi] is fed [length us] and [S i] and produces the index of - the digit to which value should be added; - [fc] modifies the carried value before adding it to that digit *) - Definition carry_gen fc fi i := fun us => - let i := fi i in - let di := nth_default 0 us i in - let '(di', ci) := carry_single i di in - let us' := set_nth i di' us in - add_to_nth (fi (S i)) (fc ci) us'. - - (* carry_simple does not modify the carried value, and always adds it - to the digit with index [S i] *) - Definition carry_simple := carry_gen (fun ci => ci) (fun i => i). - - Definition carry_simple_sequence is us := fold_right carry_simple us is. - - Fixpoint make_chain i := - match i with - | O => nil - | S i' => i' :: make_chain i' - end. - - Definition full_carry_chain := make_chain (length limb_widths). - - Definition carry_simple_full := carry_simple_sequence full_carry_chain. - - Definition carry_simple_add us vs := carry_simple_full (BaseSystem.add us vs). - - Definition carry_simple_sub us vs := carry_simple_full (BaseSystem.sub us vs). - - Definition carry_simple_mul out_base us vs := carry_simple_full (BaseSystem.mul out_base us vs). - End carrying. - End Pow2Base. diff --git a/src/BoundedArithmetic/Pow2BaseProofs.v b/src/BoundedArithmetic/Pow2BaseProofs.v index fd92db37d..fcb453ea6 100644 --- a/src/BoundedArithmetic/Pow2BaseProofs.v +++ b/src/BoundedArithmetic/Pow2BaseProofs.v @@ -9,12 +9,13 @@ Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.RewriteHyp. Require Import Crypto.BoundedArithmetic.Pow2Base. -Require Import Crypto.BoundedArithmetic.BaseSystemProofs. Require Import Crypto.Util.Notations. Require Export Crypto.Util.Bool. Require Export Crypto.Util.FixCoqMistakes. Local Open Scope Z_scope. +Require Crypto.BoundedArithmetic.BaseSystemProofs. + Create HintDb simpl_add_to_nth discriminated. Create HintDb push_upper_bound discriminated. Create HintDb pull_upper_bound discriminated. @@ -66,12 +67,6 @@ Section Pow2BaseProofs. eauto using Z.add_nonneg_nonneg, limb_widths_nonneg, In_firstn. Qed. Hint Resolve sum_firstn_limb_widths_nonneg. - Lemma two_sum_firstn_limb_widths_pos n : 0 < 2^sum_firstn limb_widths n. - Proof using Type*. auto with zarith. Qed. - - Lemma two_sum_firstn_limb_widths_nonzero n : 2^sum_firstn limb_widths n <> 0. - Proof using Type*. pose proof (two_sum_firstn_limb_widths_pos n); omega. Qed. - Lemma base_from_limb_widths_step : forall i b w, (S i < length limb_widths)%nat -> nth_error base i = Some b -> nth_error limb_widths i = Some w -> @@ -133,50 +128,6 @@ Section Pow2BaseProofs. reflexivity. Qed. - Lemma base_succ : forall i, ((S i) < length limb_widths)%nat -> - nth_default 0 base (S i) mod nth_default 0 base i = 0. - Proof using Type*. - intros. - repeat rewrite nth_default_base by omega. - apply Z.mod_same_pow. - split; [apply sum_firstn_limb_widths_nonneg | ]. - destruct (NPeano.Nat.eq_dec i 0); subst. - + case_eq limb_widths; intro; unfold sum_firstn; simpl; try omega; intros l' lw_eq. - apply Z.add_nonneg_nonneg; try omega. - apply limb_widths_nonneg. - rewrite lw_eq. - apply in_eq. - + assert (i < length limb_widths)%nat as i_lt_length by omega. - apply nth_error_length_exists_value in i_lt_length. - destruct i_lt_length as [x nth_err_x]. - erewrite sum_firstn_succ; eauto. - apply nth_error_value_In in nth_err_x. - apply limb_widths_nonneg in nth_err_x. - omega. - Qed. - - Lemma nth_error_subst : forall i b, nth_error base i = Some b -> - b = 2 ^ (sum_firstn limb_widths i). - Proof using Type*. - intros i b nth_err_b. - pose proof (nth_error_value_length _ _ _ _ nth_err_b). - rewrite base_from_limb_widths_length in *. - rewrite nth_error_base in nth_err_b by assumption. - rewrite two_p_correct in nth_err_b. - congruence. - Qed. - - Lemma base_positive : forall b : Z, In b base -> b > 0. - Proof using Type*. - intros b In_b_base. - apply In_nth_error_value in In_b_base. - destruct In_b_base as [i nth_err_b]. - apply nth_error_subst in nth_err_b. - rewrite nth_err_b. - apply Z.gt_lt_iff. - apply Z.pow_pos_nonneg; omega || auto using sum_firstn_limb_widths_nonneg. - Qed. - Lemma b0_1 : forall x : Z, limb_widths <> nil -> nth_default x base 0 = 1. Proof using Type. case_eq limb_widths; intros; [congruence | reflexivity]. @@ -229,27 +180,6 @@ Section Pow2BaseProofs. apply nth_default_preserves_properties; auto; omega. Qed. - Lemma pow2_mod_bounded_iff :forall lw us, (forall w, In w lw -> 0 <= w) -> (bounded lw us <-> - (forall i, Z.pow2_mod (nth_default 0 us i) (nth_default 0 lw i) = nth_default 0 us i)). - Proof using Type. - clear. - split; intros; auto using pow2_mod_bounded. - cbv [bounded]; intros. - assert (0 <= nth_default 0 lw i) by (apply nth_default_preserves_properties; auto; omega). - split. - + specialize (H0 i). - rewrite Z.pow2_mod_spec in H0 by assumption. - apply Z.mod_small_iff in H0; [ | apply Z.pow_nonzero; (assumption || omega)]. - destruct H0; try omega. - pose proof (Z.pow_nonneg 2 (nth_default 0 lw i)). - specialize_by omega; omega. - + apply Z.testbit_false_bound; auto. - intros. - rewrite <-H0. - rewrite Z.testbit_pow2_mod by assumption. - break_if; reflexivity || omega. - Qed. - Lemma bounded_nil_iff : forall us, bounded nil us <-> (forall u, In u us -> u = 0). Proof using Type. clear. @@ -277,7 +207,7 @@ Section Pow2BaseProofs. nth_default 0 us i = Z.pow2_mod (BaseSystem.decode base us >> sum_firstn limb_widths i) (nth_default 0 limb_widths i). Proof using Type*. intro; revert limb_widths limb_widths_nonneg; induction us; intros. - + rewrite nth_default_nil, decode_nil, Z.shiftr_0_l, Z.pow2_mod_spec, Z.mod_0_l by + + rewrite nth_default_nil, BaseSystemProofs.decode_nil, Z.shiftr_0_l, Z.pow2_mod_spec, Z.mod_0_l by (try (apply Z.pow_nonzero; try omega); apply nth_default_preserves_properties; auto; omega). reflexivity. + destruct i. @@ -286,11 +216,11 @@ Section Pow2BaseProofs. * cbv [base_from_limb_widths]. rewrite <-pow2_mod_bounded with (lw := nil); rewrite bounded_nil_iff in *; auto using in_cons; try solve [intros; exfalso; eauto using in_nil]. - rewrite !nth_default_nil, decode_base_nil; auto. + rewrite !nth_default_nil, BaseSystemProofs.decode_base_nil; auto. cbv. auto using in_eq. - * rewrite nth_default_cons, base_from_limb_widths_cons, peel_decode. + * rewrite nth_default_cons, base_from_limb_widths_cons, BaseSystemProofs.peel_decode. fold (BaseSystem.mul_each (two_p w)). - rewrite <-mul_each_base, mul_each_rep. + rewrite <-BaseSystemProofs.mul_each_base, BaseSystemProofs.mul_each_rep. rewrite two_p_correct, (Z.mul_comm (2 ^ w)). rewrite <-Z.shiftl_mul_pow2 by auto using in_eq. rewrite bounded_iff in *. @@ -311,12 +241,12 @@ Section Pow2BaseProofs. destruct limb_widths as [|w lw]. * cbv [base_from_limb_widths]. rewrite <-pow2_mod_bounded with (lw := nil); rewrite bounded_nil_iff in *; auto using in_cons. - rewrite sum_firstn_nil, !nth_default_nil, decode_base_nil, Z.shiftr_0_r. + rewrite sum_firstn_nil, !nth_default_nil, BaseSystemProofs.decode_base_nil, Z.shiftr_0_r. apply nth_default_preserves_properties; intros; auto using in_cons. f_equal; auto using in_cons. - * rewrite sum_firstn_succ_cons, nth_default_cons_S, base_from_limb_widths_cons, peel_decode. + * rewrite sum_firstn_succ_cons, nth_default_cons_S, base_from_limb_widths_cons, BaseSystemProofs.peel_decode. fold (BaseSystem.mul_each (two_p w)). - rewrite <-mul_each_base, mul_each_rep. + rewrite <-BaseSystemProofs.mul_each_base, BaseSystemProofs.mul_each_rep. rewrite two_p_correct, (Z.mul_comm (2 ^ w)). rewrite <-Z.shiftl_mul_pow2 by auto using in_eq. rewrite bounded_iff in *. @@ -334,22 +264,6 @@ Section Pow2BaseProofs. intros; apply nth_default_preserves_properties; auto; omega. Qed. Hint Resolve nth_default_limb_widths_nonneg. - Lemma parity_decode : forall x, - (0 < nth_default 0 limb_widths 0) -> - length x = length limb_widths -> - Z.odd (BaseSystem.decode base x) = Z.odd (nth_default 0 x 0). - Proof using Type*. - intros. - destruct limb_widths, x; simpl in *; try discriminate; try reflexivity. - rewrite peel_decode, nth_default_cons. - fold (BaseSystem.mul_each (two_p z)). - rewrite <-mul_each_base, mul_each_rep. - rewrite Z.odd_add_mul_even; [ f_equal; ring | ]. - rewrite <-Z.even_spec, two_p_correct. - apply Z.even_pow. - rewrite @nth_default_cons in *; auto. - Qed. - Lemma decode_firstn_pow2_mod : forall us i, (i <= length us)%nat -> length us = length limb_widths -> @@ -358,11 +272,11 @@ Section Pow2BaseProofs. Proof using Type*. intros; induction i; repeat match goal with - | |- _ => rewrite sum_firstn_0, decode_nil, Z.pow2_mod_0_r; reflexivity + | |- _ => rewrite sum_firstn_0, BaseSystemProofs.decode_nil, Z.pow2_mod_0_r; reflexivity | |- _ => progress distr_length | |- _ => progress autorewrite with simpl_firstn | |- _ => rewrite firstn_succ with (d := 0) - | |- _ => rewrite set_higher + | |- _ => rewrite BaseSystemProofs.set_higher | |- _ => rewrite nth_default_base | |- _ => rewrite IHi | |- _ => rewrite <-Z.lor_shiftl by (rewrite ?Z.pow2_mod_spec; try apply Z.mod_pos_bound; zero_bounds) @@ -459,82 +373,15 @@ Section Pow2BaseProofs. replace (length us) with (length limb_widths); try omega. } Qed. - Lemma decode_firstn_succ : forall us i, - (S i <= length us)%nat -> - bounded limb_widths us -> - length us = length limb_widths -> - BaseSystem.decode base (firstn (S i) us) = - Z.lor (BaseSystem.decode base (firstn i us)) (nth_default 0 us i << sum_firstn limb_widths i). - Proof using Type*. - repeat match goal with - | |- _ => progress intros - | |- _ => progress autorewrite with Ztestbit - | |- _ => 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)] => - destruct (Z_le_dec (sum_firstn l i) a); - [ rewrite (testbit_decode_firstn_high _ i a) - | rewrite (Z.testbit_neg_r _ (a - sum_firstn l i))] - | |- appcontext [Z.testbit (BaseSystem.decode' _ (firstn ?i _)) _] => - rewrite (decode_firstn_pow2_mod _ i) - | |- _ => rewrite digit_select by auto - | |- _ => rewrite Z.testbit_pow2_mod - | |- _ => assumption - | |- _ => reflexivity - | |- _ => omega - | |- _ => f_equal; ring - | |- _ => solve [auto] - | |- _ => solve [zero_bounds] - | H : appcontext [nth_default 0 limb_widths ?i] |- _ => - pose proof (nth_default_limb_widths_nonneg i); omega - | |- appcontext [nth_default 0 limb_widths ?i] => - pose proof (nth_default_limb_widths_nonneg i); omega - end. - Qed. - - Lemma testbit_decode_digit_select : forall us n i, - bounded limb_widths us -> - sum_firstn limb_widths i <= n < sum_firstn limb_widths (S i) -> - Z.testbit (BaseSystem.decode base us) n = Z.testbit (nth_default 0 us i) (n - sum_firstn limb_widths i). - Proof using Type*. - repeat match goal with - | |- _ => progress intros - | |- _ => erewrite digit_select by eauto - | |- _ => progress rewrite sum_firstn_succ_default in * - | |- _ => progress autorewrite with Ztestbit - | |- _ => break_if - | |- _ => omega - | |- _ => solve [f_equal;ring] - end. - Qed. - - Lemma testbit_bounded_high : forall i n us, bounded limb_widths us -> - nth_default 0 limb_widths i <= n -> - Z.testbit (nth_default 0 us i) n = false. - Proof using Type*. - repeat match goal with - | |- _ => progress intros - | |- _ => break_if - | |- _ => omega - | |- _ => reflexivity - | |- _ => assumption - | |- _ => apply nth_default_limb_widths_nonneg; auto - | H : nth_default 0 limb_widths ?i <= ?n |- 0 <= ?n => etransitivity; [ | eapply H] - | |- _ => erewrite <-pow2_mod_bounded by eauto; rewrite Z.testbit_pow2_mod - end. - Qed. - Lemma decode_shift_app : forall us0 us1, (length (us0 ++ us1) <= length limb_widths)%nat -> BaseSystem.decode base (us0 ++ us1) = (BaseSystem.decode (base_from_limb_widths (firstn (length us0) limb_widths)) us0) + ((BaseSystem.decode (base_from_limb_widths (skipn (length us0) limb_widths)) us1) << sum_firstn limb_widths (length us0)). Proof using Type*. unfold BaseSystem.decode; intros us0 us1 ?. assert (0 <= sum_firstn limb_widths (length us0)) by auto using sum_firstn_nonnegative. - rewrite decode'_splice; autorewrite with push_firstn. + rewrite BaseSystemProofs.decode'_splice; autorewrite with push_firstn. apply Z.add_cancel_l. autorewrite with pull_base_from_limb_widths Zshift_to_pow zsimplify. - rewrite decode'_map_mul, two_p_correct; nia. + rewrite BaseSystemProofs.decode'_map_mul, two_p_correct; nia. Qed. Lemma decode_shift : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> @@ -564,72 +411,6 @@ Section Pow2BaseProofs. reflexivity. Qed. - Lemma bounded_nil_r : forall l, (forall x, In x l -> 0 <= x) -> bounded l nil. - Proof using Type. - cbv [bounded]; intros. - rewrite nth_default_nil. - apply nth_default_preserves_properties; intros; split; zero_bounds. - Qed. - - Section make_base_vector. - Local Notation k := (sum_firstn limb_widths (length limb_widths)). - Context (limb_widths_match_modulus : forall i j, - (i < length base)%nat -> - (j < length base)%nat -> - (i + j >= length base)%nat -> - let w_sum := sum_firstn limb_widths in - k + w_sum (i + j - length base)%nat <= w_sum i + w_sum j) - (limb_widths_good : forall i j, (i + j < length limb_widths)%nat -> - sum_firstn limb_widths (i + j) <= - sum_firstn limb_widths i + sum_firstn limb_widths j). - - Lemma base_matches_modulus: forall i j, - (i < length base)%nat -> - (j < length base)%nat -> - (i+j >= length base)%nat-> - let b := nth_default 0 base in - let r := (b i * b j) / (2^k * b (i+j-length base)%nat) in - b i * b j = r * (2^k * b (i+j-length base)%nat). - Proof using limb_widths_match_modulus limb_widths_nonneg. - intros. - rewrite (Z.mul_comm r). - subst r. - rewrite base_from_limb_widths_length in *; - assert (i + j - length limb_widths < length limb_widths)%nat by omega. - rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; subst b; rewrite ?nth_default_base; zero_bounds; - assumption). - rewrite (Zminus_0_l_reverse (b i * b j)) at 1. - f_equal. - subst b. - repeat rewrite nth_default_base by auto. - do 2 rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. - symmetry. - apply Z.mod_same_pow. - split. - + apply Z.add_nonneg_nonneg; auto using sum_firstn_limb_widths_nonneg. - + auto using limb_widths_match_modulus. - Qed. - - Lemma base_good : forall i j : nat, - (i + j < length base)%nat -> - let b := nth_default 0 base in - let r := b i * b j / b (i + j)%nat in - b i * b j = r * b (i + j)%nat. - Proof using limb_widths_good limb_widths_nonneg. - intros; subst b r. - clear limb_widths_match_modulus. - rewrite base_from_limb_widths_length in *. - repeat rewrite nth_default_base by omega. - rewrite (Z.mul_comm _ (2 ^ (sum_firstn limb_widths (i+j)))). - rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; zero_bounds; - auto using sum_firstn_limb_widths_nonneg). - rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. - rewrite Z.mod_same_pow; try ring. - split; [ auto using sum_firstn_limb_widths_nonneg | ]. - apply limb_widths_good. - assumption. - Qed. - End make_base_vector. 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. @@ -647,184 +428,6 @@ 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. Hint Rewrite <- @upper_bound_cons @upper_bound_app using solve [ eauto with znonzero ] : pull_upper_bound. -Section BitwiseDecodeEncode. - Context {limb_widths} (limb_widths_nonnil : limb_widths <> nil) - (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w) - (limb_widths_good : forall i j, (i + j < length limb_widths)%nat -> - sum_firstn limb_widths (i + j) <= - sum_firstn limb_widths i + sum_firstn limb_widths j). - Local Hint Resolve limb_widths_nonneg. - Local Hint Resolve nth_default_limb_widths_nonneg. - Local Hint Resolve sum_firstn_limb_widths_nonneg. - Local Notation "w[ i ]" := (nth_default 0 limb_widths i). - Local Notation base := (base_from_limb_widths limb_widths). - Local Notation upper_bound := (upper_bound limb_widths). - - Lemma encode'_spec : forall x i, (i <= length limb_widths)%nat -> - encode' limb_widths x i = BaseSystem.encode' base x upper_bound i. - Proof using limb_widths_nonneg. - induction i; intros. - + rewrite encode'_zero. reflexivity. - + rewrite encode'_succ, <-IHi by omega. - simpl; do 2 f_equal. - rewrite Z.land_ones, Z.shiftr_div_pow2 by auto. - match goal with H : (S _ <= length limb_widths)%nat |- _ => - apply le_lt_or_eq in H; destruct H end. - - repeat f_equal; rewrite nth_default_base by (omega || auto); reflexivity. - - repeat f_equal; try solve [rewrite nth_default_base by (omega || auto); reflexivity]. - rewrite nth_default_out_of_bounds by (distr_length; omega). - unfold Pow2Base.upper_bound. - congruence. - Qed. - - Lemma length_encode' : forall lw z i, length (encode' lw z i) = i. - Proof using Type. - induction i; intros; simpl encode'; distr_length. - Qed. - Hint Rewrite length_encode' : distr_length. - - Lemma bounded_encode' : forall z i, (0 <= z) -> - bounded (firstn i limb_widths) (encode' limb_widths z i). - Proof using limb_widths_nonneg. - intros; induction i; simpl encode'; - repeat match goal with - | |- _ => progress intros - | |- _ => progress autorewrite with push_nth_default in * - | |- _ => progress autorewrite with Ztestbit - | |- _ => progress rewrite ?firstn_O, ?Nat.sub_diag in * - | |- _ => rewrite Z.testbit_pow2_mod by auto - | |- _ => rewrite Z.ones_spec by zero_bounds - | |- _ => rewrite sum_firstn_succ_default - | |- _ => rewrite nth_default_out_of_bounds by distr_length - | |- _ => break_if; distr_length - | |- _ => apply bounded_nil_r - | |- appcontext[nth_default _ (_ :: nil) ?i] => case_eq i; intros; autorewrite with push_nth_default - | |- Z.pow2_mod (?a >> ?b) _ = (?a >> ?b) => apply Z.bits_inj' - | IH : forall i, _ = nth_default 0 (encode' _ _ _) i - |- appcontext[nth_default 0 limb_widths ?i] => specialize (IH i) - | H : In _ (firstn _ _) |- _ => apply In_firstn in H - | H1 : ~ (?a < ?b)%nat, H2 : (?a < S ?b)%nat |- _ => - progress replace a with b in * by omega - | H : bounded _ _ |- bounded _ _ => - apply pow2_mod_bounded_iff; rewrite pow2_mod_bounded_iff in H - | |- _ => solve [auto] - | |- _ => contradiction - | |- _ => reflexivity - end. - Qed. - - Lemma bounded_encodeZ : forall z, (0 <= z) -> - bounded limb_widths (encodeZ limb_widths z). - Proof using limb_widths_nonneg. - cbv [encodeZ]; intros. - pose proof (bounded_encode' z (length limb_widths)) as Hencode'. - rewrite firstn_all in Hencode'; auto. - Qed. - - Lemma base_upper_bound_compatible : @base_max_succ_divide base upper_bound. - Proof using limb_widths_nonneg. - unfold base_max_succ_divide; intros i lt_Si_length. - rewrite base_from_limb_widths_length in lt_Si_length. - rewrite Nat.lt_eq_cases in lt_Si_length; destruct lt_Si_length; - rewrite !nth_default_base by (omega || auto). - + erewrite sum_firstn_succ by (eapply nth_error_Some_nth_default with (x := 0); omega). - rewrite Z.pow_add_r; eauto. - apply Z.divide_factor_r. - + rewrite nth_default_out_of_bounds by (distr_length; omega). - unfold Pow2Base.upper_bound. - replace (length limb_widths) with (S (pred (length limb_widths))) by omega. - replace i with (pred (length limb_widths)) by omega. - erewrite sum_firstn_succ by (eapply nth_error_Some_nth_default with (x := 0); omega). - rewrite Z.pow_add_r; eauto. - apply Z.divide_factor_r. - Qed. - Hint Resolve base_upper_bound_compatible. - - Lemma encodeZ_spec : forall x, - BaseSystem.decode base (encodeZ limb_widths x) = x mod upper_bound. - Proof. - intros. - assert (length base = length limb_widths) by distr_length. - unfold encodeZ; rewrite encode'_spec by omega. - erewrite BaseSystemProofs.encode'_spec; unfold Pow2Base.upper_bound; - zero_bounds; intros; eauto using base_positive, b0_1. { - rewrite nth_default_out_of_bounds by omega. - reflexivity. - } { - econstructor; try apply base_good; - eauto using base_positive, b0_1. - } - Qed. - - Lemma encodeZ_length : forall x, length (encodeZ limb_widths x) = length limb_widths. - Proof using limb_widths_nonneg. - cbv [encodeZ]; intros. - rewrite encode'_spec by omega. - apply encode'_length. - Qed. - - Definition decode_bitwise'_invariant us i acc := - forall n, 0 <= n -> Z.testbit acc n = Z.testbit (BaseSystem.decode base us) (n + sum_firstn limb_widths i). - - Lemma decode_bitwise'_invariant_step : forall us, - length us = length limb_widths -> - bounded limb_widths us -> - forall i acc, decode_bitwise'_invariant us (S i) acc -> - decode_bitwise'_invariant us i (Z.lor (nth_default 0 us i) (acc << nth_default 0 limb_widths i)). - Proof using limb_widths_nonneg. - repeat match goal with - | |- _ => progress cbv [decode_bitwise'_invariant]; intros - | |- _ => erewrite testbit_bounded_high by (omega || eauto) - | |- _ => progress autorewrite with Ztestbit - | |- _ => progress rewrite sum_firstn_succ_default - | |- appcontext[Z.testbit _ ?n] => rewrite (Z.testbit_neg_r _ n) by omega - | H : forall n, 0 <= n -> Z.testbit _ n = _ |- _ => rewrite H by omega - | |- _ => solve [f_equal; ring] - | |- appcontext[Z.testbit _ (?x + sum_firstn limb_widths ?i)] => - erewrite testbit_decode_digit_select with (i0 := i) by - (eauto; rewrite sum_firstn_succ_default; omega) - | |- appcontext[Z.testbit _ (?a - ?b)] => destruct (Z_lt_dec a b) - | _ => progress break_if - end. - Qed. - - Lemma decode_bitwise'_invariant_holds : forall i us acc, - length us = length limb_widths -> - bounded limb_widths us -> - decode_bitwise'_invariant us i acc -> - decode_bitwise'_invariant us 0 (decode_bitwise' limb_widths us i acc). - Proof using limb_widths_nonneg. - repeat match goal with - | |- _ => progress intros - | |- _ => solve [auto using decode_bitwise'_invariant_step] - | |- appcontext[decode_bitwise' ?a ?b ?c ?d] => - functional induction (decode_bitwise' a b c d) - end. - Qed. - - Lemma decode_bitwise_spec : forall us, bounded limb_widths us -> - length us = length limb_widths -> - decode_bitwise limb_widths us = BaseSystem.decode base us. - Proof using limb_widths_nonneg. - repeat match goal with - | |- _ => progress cbv [decode_bitwise decode_bitwise'_invariant] in * - | |- _ => progress intros - | |- _ => rewrite sum_firstn_0 - | |- _ => erewrite testbit_decode_high by (assumption || omega) - | H0 : ?P ?x , H1 : ?P ?x -> _ |- _ => specialize (H1 H0) - | H : _ -> forall n, 0 <= n -> Z.testbit _ n = _ |- _ => rewrite H - | |- decode_bitwise' ?a ?b ?c ?d = _ => - let H := fresh "H" in - pose proof (decode_bitwise'_invariant_holds c b d) as H; - apply Z.bits_inj' - | |- _ => apply Z.testbit_0_l - | |- _ => assumption - | |- _ => solve [f_equal; ring] - end. - Qed. - -End BitwiseDecodeEncode. - Section UniformBase. Context {width : Z} (limb_width_nonneg : 0 <= width). Context (limb_widths : list Z) @@ -900,11 +503,11 @@ Section UniformBase. Proof using Type. clear. induction us; intros. - + rewrite !decode_nil; reflexivity. + + rewrite !BaseSystemProofs.decode_nil; reflexivity. + distr_length. destruct bs. - - rewrite firstn_nil, !decode_base_nil; reflexivity. - - rewrite firstn_cons, !peel_decode. + - rewrite firstn_nil, !BaseSystemProofs.decode_base_nil; reflexivity. + - rewrite firstn_cons, !BaseSystemProofs.peel_decode. f_equal. apply IHus. Qed. @@ -949,609 +552,4 @@ Section UniformBase. rewrite decode_shift_app by auto using uniform_limb_widths_nonneg. reflexivity. Qed. - - Lemma decode_shift_uniform : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> - BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode base us) << width). - Proof using Type*. - intros. - rewrite decode_tl_base with (us := us) by distr_length. - apply decode_shift_uniform_tl; assumption. - Qed. - -End UniformBase. - -Hint Rewrite @upper_bound_uniform using solve [ auto with datatypes ] : push_upper_bound. - -Section SplitIndex. - (* This section defines [split_index], which for a list of bounded digits - splits a bit index in the decoded value into a digit index and a bit - index within the digit. Examples: - limb_widths [4;4] : split_index 6 = (1,2) - limb_widths [26,25,26] : split_index 30 = (1,4) - limb_widths [26,25,26] : split_index 51 = (2,0) - *) - Local Notation "u # i" := (nth_default 0 u i). - - Function split_index' i index lw := - match lw with - | nil => (index, i) - | w :: lw' => if Z_lt_dec i w then (index, i) - else split_index' (i - w) (S index) lw' - end. - - Lemma split_index'_ge_index : forall i index lw, (index <= fst (split_index' i index lw))%nat. - Proof. - intros; functional induction (split_index' i index lw); - repeat match goal with - | |- _ => omega - | |- _ => progress (simpl fst; simpl snd) - end. - Qed. - - Lemma split_index'_done_case : forall i index lw, 0 <= i -> - (forall x, In x lw -> 0 <= x) -> - if Z_lt_dec i (sum_firstn lw (length lw)) - then (fst (split_index' i index lw) - index < length lw)%nat - else (fst (split_index' i index lw) - index = length lw)%nat. - Proof. - intros; functional induction (split_index' i index lw); - repeat match goal with - | |- _ => break_if - | |- _ => rewrite sum_firstn_nil in * - | |- _ => rewrite sum_firstn_succ_cons in * - | |- _ => progress distr_length - | |- _ => progress (simpl fst; simpl snd) - | H : appcontext [split_index' ?a ?b ?c] |- _ => - unique pose proof (split_index'_ge_index a b c) - | H : appcontext [sum_firstn ?l ?i] |- _ => - let H0 := fresh "H" in - assert (forall x, In x l -> 0 <= x) by auto using in_cons; - unique pose proof (sum_firstn_limb_widths_nonneg H0 i) - | |- _ => progress specialize_by assumption - | |- _ => progress specialize_by omega - | |- _ => omega - end. - Qed. - - Lemma snd_split_index'_nonneg : forall index lw i, (0 <= i) -> - (0 <= snd (split_index' i index lw)). - Proof. - intros; functional induction (split_index' i index lw); - repeat match goal with - | |- _ => omega - | H : ?P -> ?G |- ?G => apply H - | |- _ => progress (simpl fst; simpl snd) - end. - Qed. - - Lemma snd_split_index'_small : forall i index lw, 0 <= i < sum_firstn lw (length lw) -> - (snd (split_index' i index lw) < lw # (fst (split_index' i index lw) - index)). - Proof. - intros; functional induction (split_index' i index lw); - try match goal with |- appcontext [split_index' ?a ?b ?c] => - pose proof (split_index'_ge_index a b c) end; - repeat match goal with - | |- _ => progress autorewrite with push_nth_default distr_length in * - | |- _ => rewrite Nat.sub_diag - | |- _ => rewrite sum_firstn_nil 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) => - replace (a - b)%nat with (S (a - S b))%nat - | |- _ => omega - end. - Qed. - - Lemma split_index'_correct : forall i index lw, - sum_firstn lw (fst (split_index' i index lw) - index) + (snd (split_index' i index lw)) = i. - Proof. - intros; functional induction (split_index' i index lw); - repeat match goal with - | |- _ => omega - | |- _ => rewrite Nat.sub_diag - | |- _ => progress rewrite ?sum_firstn_nil, ?sum_firstn_0, ?sum_firstn_succ_cons - | |- _ => 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 - (S (fst (split_index' i (S idx) lw) - S idx))%nat - end. - Qed. - - Context limb_widths - (limb_widths_pos : forall w, In w limb_widths -> 0 <= w). - Local Hint Resolve limb_widths_pos. - Local Notation base := (base_from_limb_widths limb_widths). - Local Notation bitsIn lw := (sum_firstn lw (length lw)). - - Definition split_index i := split_index' i 0 limb_widths. - Definition digit_index i := fst (split_index i). - Definition bit_index i := snd (split_index i). - - Lemma testbit_decode : forall us n, - 0 <= n < bitsIn limb_widths -> - length us = length limb_widths -> - bounded limb_widths us -> - Z.testbit (BaseSystem.decode base us) n = Z.testbit (us # digit_index n) (bit_index n). - Proof using Type*. - cbv [digit_index bit_index split_index]; intros. - pose proof (split_index'_correct n 0 limb_widths). - pose proof (snd_split_index'_nonneg 0 limb_widths n). - specialize_by assumption. - repeat match goal with - | |- _ => progress autorewrite with Ztestbit natsimplify in * - | |- _ => erewrite digit_select by eauto - | |- _ => break_if - | |- _ => rewrite Z.testbit_pow2_mod by auto using nth_default_limb_widths_nonneg - | |- _ => omega - | |- _ => f_equal; omega - end. - destruct (Z_lt_dec n (bitsIn limb_widths)). { - pose proof (snd_split_index'_small n 0 limb_widths). - specialize_by omega. - rewrite Nat.sub_0_r in *. - omega. - } { - apply testbit_decode_high; auto. - replace (length us) with (length limb_widths) in *. - omega. - } - Qed. - - Lemma testbit_decode_full : forall us n, - length us = length limb_widths -> - bounded limb_widths us -> - Z.testbit (BaseSystem.decode base us) n = - if Z_le_dec 0 n - then (if Z_lt_dec n (bitsIn limb_widths) - then Z.testbit (us # digit_index n) (bit_index n) - else false) - else false. - Proof using Type*. - repeat match goal with - | |- _ => progress intros - | |- _ => break_if - | |- _ => apply Z.testbit_neg_r; lia - | |- _ => apply testbit_decode_high; auto; - try match goal with H : length _ = length limb_widths |- _ => rewrite H end; lia - | |- _ => auto using testbit_decode - end. - Qed. - - Lemma bit_index_nonneg : forall i, 0 <= i -> 0 <= bit_index i. - Proof using Type. - apply snd_split_index'_nonneg. - Qed. - - Lemma digit_index_lt_length : forall i, 0 <= i < bitsIn limb_widths -> - (digit_index i < length limb_widths)%nat. - Proof using Type*. - cbv [bit_index digit_index split_index]; intros. - pose proof (split_index'_done_case i 0 limb_widths). - specialize_by lia. specialize_by eauto. - break_if; lia. - Qed. - - Lemma bit_index_not_done : forall i, 0 <= i < bitsIn limb_widths -> - (bit_index i < limb_widths # digit_index i). - Proof using Type. - - cbv [bit_index digit_index split_index]; intros. - eapply Z.lt_le_trans; try apply (snd_split_index'_small i 0 limb_widths); try assumption. - rewrite Nat.sub_0_r; lia. - Qed. - - Lemma split_index_eqn : forall i, 0 <= i < bitsIn limb_widths -> - sum_firstn limb_widths (digit_index i) + bit_index i = i. - Proof using Type. - cbv [bit_index digit_index split_index]; intros. - etransitivity;[ | apply (split_index'_correct i 0 limb_widths) ]. - repeat f_equal; omega. - Qed. - - Lemma rem_bits_in_digit_pos : forall i, 0 <= i < bitsIn limb_widths -> - 0 < (limb_widths # digit_index i) - bit_index i. - Proof using Type. - repeat match goal with - | |- _ => progress intros - | |- 0 < ?a - ?b => destruct (Z_lt_dec b a); [ lia | exfalso ] - | H : ~ (bit_index ?i < limb_widths # digit_index ?i) |- _ => - pose proof (bit_index_not_done i); specialize_by omega; omega - end. - Qed. - - - Lemma rem_bits_in_digit_le_rem_bits : forall i, 0 <= i < bitsIn limb_widths -> - i + ((limb_widths # digit_index i) - bit_index i) <= bitsIn limb_widths. - Proof using Type*. - intros. - rewrite <-(split_index_eqn i) at 1 by lia. - match goal with - | |- ?a + ?b + (?c - ?b) <= _ => replace (a + b + (c - b)) with (c + a) by ring - end. - rewrite <-sum_firstn_succ_default. - apply sum_firstn_prefix_le; auto. - pose proof (digit_index_lt_length i H); lia. - Qed. - - - Lemma same_digit : forall i j, 0 <= i <= j -> - j < bitsIn limb_widths -> - j < i + ((limb_widths # (digit_index i)) - bit_index i) -> - (digit_index i = digit_index j)%nat. - Proof using Type*. - intros. - pose proof (split_index_eqn i). - pose proof (split_index_eqn j). - specialize_by lia. - apply le_antisym. { - eapply sum_firstn_pos_lt_succ; eauto; try (apply digit_index_lt_length; auto; lia). - rewrite sum_firstn_succ_default. - eapply Z.le_lt_trans; [ | apply Z.add_lt_mono_r; apply bit_index_not_done; lia ]. - pose proof (bit_index_nonneg i). - specialize_by lia. - lia. - } { - eapply sum_firstn_pos_lt_succ; eauto; try (apply digit_index_lt_length; auto; lia). - rewrite <-H2 in H1 at 1. - match goal with - | H : _ < ?a + ?b + (?c - ?b) |- _ => replace (a + b + (c - b)) with (c + a) in H by ring; - rewrite <-sum_firstn_succ_default in H - end. - rewrite <-H3 in H1. - pose proof (bit_index_nonneg j). specialize_by lia. - lia. - } - Qed. - - Lemma same_digit_bit_index_sub : forall i j, 0 <= i <= j -> j < bitsIn limb_widths -> - digit_index i = digit_index j -> - bit_index j - bit_index i = j - i. - Proof using Type. - intros. - pose proof (split_index_eqn i). - pose proof (split_index_eqn j). - specialize_by lia. - rewrite H1 in *. - lia. - Qed. - -End SplitIndex. - -Section carrying_helper. - Context {limb_widths} (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w). - Local Notation base := (base_from_limb_widths limb_widths). - Local Notation log_cap i := (nth_default 0 limb_widths i). - - Lemma update_nth_sum : forall n f us, (n < length us \/ n >= length limb_widths)%nat -> - BaseSystem.decode base (update_nth n f us) = - (let v := nth_default 0 us n in f v - v) * nth_default 0 base n + BaseSystem.decode base us. - Proof using Type. - intros. - unfold BaseSystem.decode. - destruct H as [H|H]. - { nth_inbounds; auto. (* TODO(andreser): nth_inbounds should do this auto*) - erewrite nth_error_value_eq_nth_default by eassumption. - unfold splice_nth. - rewrite <- (firstn_skipn n us) at 3. - do 2 rewrite decode'_splice. - remember (length (firstn n us)) as n0. - ring_simplify. - remember (BaseSystem.decode' (firstn n0 base) (firstn n us)). - rewrite (skipn_nth_default n us 0) by omega. - erewrite (nth_error_value_eq_nth_default _ _ us) by eassumption. - rewrite firstn_length in Heqn0. - rewrite Min.min_l in Heqn0 by omega; subst n0. - destruct (le_lt_dec (length limb_widths) n). { - rewrite (@nth_default_out_of_bounds _ _ base) by (distr_length; auto). - rewrite skipn_all by (rewrite base_from_limb_widths_length; omega). - do 2 rewrite decode_base_nil. - ring_simplify; auto. - } { - rewrite (skipn_nth_default n base 0) by (distr_length; omega). - do 2 rewrite decode'_cons. - ring_simplify; ring. - } } - { rewrite (nth_default_out_of_bounds _ base) by (distr_length; omega); ring_simplify. - etransitivity; rewrite BaseSystem.decode'_truncate; [ reflexivity | ]. - apply f_equal. - autorewrite with push_firstn simpl_update_nth. - rewrite update_nth_out_of_bounds by (distr_length; omega * ). - reflexivity. } - Qed. - - Lemma unfold_add_to_nth n x - : forall xs, - add_to_nth n x xs - = match n with - | O => match xs with - | nil => nil - | x'::xs' => x + x'::xs' - end - | S n' => match xs with - | nil => nil - | x'::xs' => x'::add_to_nth n' x xs' - end - end. - Proof using Type. - induction n; destruct xs; reflexivity. - Qed. - - Lemma simpl_add_to_nth_0 x - : forall xs, - add_to_nth 0 x xs - = match xs with - | nil => nil - | x'::xs' => x + x'::xs' - end. - Proof using Type. intro; rewrite unfold_add_to_nth; reflexivity. Qed. - - Lemma simpl_add_to_nth_S x n - : forall xs, - add_to_nth (S n) x xs - = match xs with - | nil => nil - | x'::xs' => x'::add_to_nth n x xs' - end. - Proof using Type. intro; rewrite unfold_add_to_nth; reflexivity. Qed. - - Hint Rewrite @simpl_set_nth_S @simpl_set_nth_0 : simpl_add_to_nth. - - Lemma add_to_nth_cons : forall x u0 us, add_to_nth 0 x (u0 :: us) = x + u0 :: us. - Proof using Type. reflexivity. Qed. - - Hint Rewrite @add_to_nth_cons : simpl_add_to_nth. - - Lemma cons_add_to_nth : forall n f y us, - y :: add_to_nth n f us = add_to_nth (S n) f (y :: us). - Proof using Type. - induction n; boring. - Qed. - - Hint Rewrite <- @cons_add_to_nth : simpl_add_to_nth. - - Lemma add_to_nth_nil : forall n f, add_to_nth n f nil = nil. - Proof using Type. - induction n; boring. - Qed. - - Hint Rewrite @add_to_nth_nil : simpl_add_to_nth. - - Lemma add_to_nth_set_nth n x xs - : add_to_nth n x xs - = set_nth n (x + nth_default 0 xs n) xs. - Proof using Type. - revert xs; induction n; destruct xs; - autorewrite with simpl_set_nth simpl_add_to_nth; - try rewrite IHn; - reflexivity. - Qed. - Lemma add_to_nth_update_nth n x xs - : add_to_nth n x xs - = update_nth n (fun y => x + y) xs. - Proof using Type. - revert xs; induction n; destruct xs; - autorewrite with simpl_update_nth simpl_add_to_nth; - try rewrite IHn; - reflexivity. - Qed. - - Lemma length_add_to_nth i x xs : length (add_to_nth i x xs) = length xs. - Proof using Type. unfold add_to_nth; distr_length; reflexivity. Qed. - - Hint Rewrite @length_add_to_nth : distr_length. - - Lemma set_nth_sum : forall n x us, (n < length us \/ n >= length limb_widths)%nat -> - BaseSystem.decode base (set_nth n x us) = - (x - nth_default 0 us n) * nth_default 0 base n + BaseSystem.decode base us. - Proof using Type. intros; unfold set_nth; rewrite update_nth_sum by assumption; reflexivity. Qed. - - Lemma add_to_nth_sum : forall n x us, (n < length us \/ n >= length limb_widths)%nat -> - BaseSystem.decode base (add_to_nth n x us) = - x * nth_default 0 base n + BaseSystem.decode base us. - Proof using Type. intros; rewrite add_to_nth_set_nth, set_nth_sum; try ring_simplify; auto. Qed. - - Lemma add_to_nth_nth_default_full : forall n x l i d, - nth_default d (add_to_nth n x l) i = - if lt_dec i (length l) then - if (eq_nat_dec i n) then x + nth_default d l i - else nth_default d l i - else d. - Proof using Type. intros; rewrite add_to_nth_update_nth; apply update_nth_nth_default_full; assumption. Qed. - Hint Rewrite @add_to_nth_nth_default_full : push_nth_default. - - Lemma add_to_nth_nth_default : forall n x l i, (0 <= i < length l)%nat -> - nth_default 0 (add_to_nth n x l) i = - if (eq_nat_dec i n) then x + nth_default 0 l i else nth_default 0 l i. - Proof using Type. intros; rewrite add_to_nth_update_nth; apply update_nth_nth_default; assumption. Qed. - Hint Rewrite @add_to_nth_nth_default using omega : push_nth_default. - - Lemma log_cap_nonneg : forall i, 0 <= log_cap i. - Proof using Type*. - unfold nth_default; intros. - case_eq (nth_error limb_widths i); intros; try omega. - apply limb_widths_nonneg. - eapply nth_error_value_In; eauto. - Qed. Local Hint Resolve log_cap_nonneg. -End carrying_helper. - -Hint Rewrite @simpl_set_nth_S @simpl_set_nth_0 : simpl_add_to_nth. -Hint Rewrite @add_to_nth_cons : simpl_add_to_nth. -Hint Rewrite <- @cons_add_to_nth : simpl_add_to_nth. -Hint Rewrite @add_to_nth_nil : simpl_add_to_nth. -Hint Rewrite @length_add_to_nth : distr_length. -Hint Rewrite @add_to_nth_nth_default_full : push_nth_default. -Hint Rewrite @add_to_nth_nth_default using (omega || distr_length; omega) : push_nth_default. - -Section carrying. - Context {limb_widths} (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w). - Local Notation base := (base_from_limb_widths limb_widths). - Local Notation log_cap i := (nth_default 0 limb_widths i). - Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg. - - Lemma length_carry_gen : forall fc fi i us, length (carry_gen limb_widths fc fi i us) = length us. - Proof using Type. intros; unfold carry_gen, carry_single; distr_length; reflexivity. Qed. - - Hint Rewrite @length_carry_gen : distr_length. - - Lemma length_carry_simple : forall i us, length (carry_simple limb_widths i us) = length us. - Proof using Type. intros; unfold carry_simple; distr_length; reflexivity. Qed. - Hint Rewrite @length_carry_simple : distr_length. - - Lemma nth_default_base_succ : forall i, (S i < length limb_widths)%nat -> - nth_default 0 base (S i) = 2 ^ log_cap i * nth_default 0 base i. - Proof using Type*. - intros. - rewrite !nth_default_base, <- Z.pow_add_r by (omega || eauto using log_cap_nonneg). - autorewrite with simpl_sum_firstn; reflexivity. - Qed. - - Lemma carry_gen_decode_eq : forall fc fi i' us - (i := fi i') - (Si := fi (S i)), - (length us = length limb_widths) -> - BaseSystem.decode base (carry_gen limb_widths fc fi i' us) - = (fc (nth_default 0 us i / 2 ^ log_cap i) * - (if eq_nat_dec Si (S i) - then if lt_dec (S i) (length limb_widths) - then 2 ^ log_cap i * nth_default 0 base i - else 0 - else nth_default 0 base Si) - - 2 ^ log_cap i * (nth_default 0 us i / 2 ^ log_cap i) * nth_default 0 base i) - + BaseSystem.decode base us. - Proof using Type*. - intros fc fi i' us i Si H; intros. - destruct (eq_nat_dec 0 (length limb_widths)); - [ destruct limb_widths, us, i; simpl in *; try congruence; - break_match; - unfold carry_gen, carry_single, add_to_nth; - autorewrite with zsimplify simpl_nth_default simpl_set_nth simpl_update_nth distr_length; - reflexivity - | ]. - (*assert (0 <= i < length limb_widths)%nat by (subst i; auto with arith).*) - assert (0 <= log_cap i) by auto using log_cap_nonneg. - assert (2 ^ log_cap i <> 0) by (apply Z.pow_nonzero; lia). - unfold carry_gen, carry_single. - change (i' mod length limb_widths)%nat with i. - rewrite add_to_nth_sum by (rewrite length_set_nth; omega). - rewrite set_nth_sum by omega. - unfold Z.pow2_mod. - rewrite Z.land_ones by auto using log_cap_nonneg. - rewrite Z.shiftr_div_pow2 by auto using log_cap_nonneg. - change (fi i') with i. - subst Si. - repeat first [ ring - | match goal with H : _ = _ |- _ => rewrite !H in * end - | rewrite nth_default_base_succ by omega - | rewrite !(nth_default_out_of_bounds _ base) by (distr_length; omega) - | rewrite !(nth_default_out_of_bounds _ us) by omega - | rewrite Z.mod_eq by assumption - | progress distr_length - | progress autorewrite with natsimplify zsimplify in * - | progress break_match ]. - Qed. - - Lemma carry_simple_decode_eq : forall i us, - (length us = length limb_widths) -> - (i < (pred (length limb_widths)))%nat -> - BaseSystem.decode base (carry_simple limb_widths i us) = BaseSystem.decode base us. - Proof using Type*. - unfold carry_simple; intros; rewrite carry_gen_decode_eq by assumption. - autorewrite with natsimplify. - break_match; try lia; autorewrite with zsimplify; lia. - Qed. - - - Lemma length_carry_simple_sequence : forall is us, length (carry_simple_sequence limb_widths is us) = length us. - Proof using Type. - unfold carry_simple_sequence. - induction is; [ reflexivity | simpl; intros ]. - distr_length. - congruence. - Qed. - Hint Rewrite @length_carry_simple_sequence : distr_length. - - Lemma length_make_chain : forall i, length (make_chain i) = i. - Proof using Type. induction i; simpl; congruence. Qed. - Hint Rewrite @length_make_chain : distr_length. - - Lemma length_full_carry_chain : length (full_carry_chain limb_widths) = length limb_widths. - Proof using Type. unfold full_carry_chain; distr_length; reflexivity. Qed. - Hint Rewrite @length_full_carry_chain : distr_length. - - Lemma length_carry_simple_full us : length (carry_simple_full limb_widths us) = length us. - Proof using Type. unfold carry_simple_full; distr_length; reflexivity. Qed. - Hint Rewrite @length_carry_simple_full : distr_length. - - (* TODO : move? *) - Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat. - Proof using Type. - induction x; simpl; intuition auto with arith lia. - Qed. - - Lemma nth_default_carry_gen_full fc fi d i n us - : nth_default d (carry_gen limb_widths fc fi i us) n - = if lt_dec n (length us) - then (if eq_nat_dec n (fi i) - then Z.pow2_mod (nth_default 0 us n) (log_cap n) - else nth_default 0 us n) + - if eq_nat_dec n (fi (S (fi i))) - then fc (nth_default 0 us (fi i) >> log_cap (fi i)) - else 0 - else d. - Proof using Type. - unfold carry_gen, carry_single. - intros; autorewrite with push_nth_default natsimplify distr_length. - edestruct (lt_dec n (length us)) as [H|H]; [ | reflexivity ]. - rewrite !(@nth_default_in_bounds Z 0 d) by assumption. - repeat break_match; subst; try omega; try rewrite_hyp *; omega. - Qed. - - Hint Rewrite @nth_default_carry_gen_full : push_nth_default. - - Lemma nth_default_carry_simple_full : forall d i n us, - nth_default d (carry_simple limb_widths i us) n - = if lt_dec n (length us) - then if eq_nat_dec n i - then Z.pow2_mod (nth_default 0 us n) (log_cap n) - else nth_default 0 us n + - if eq_nat_dec n (S i) then nth_default 0 us i >> log_cap i else 0 - else d. - Proof using Type. - intros; unfold carry_simple; autorewrite with push_nth_default. - repeat break_match; try omega; try reflexivity. - Qed. - - Hint Rewrite @nth_default_carry_simple_full : push_nth_default. - - Lemma nth_default_carry_gen - : forall fc fi i us, - (0 <= i < length us)%nat - -> nth_default 0 (carry_gen limb_widths fc fi i us) i - = (if eq_nat_dec i (fi i) - then Z.pow2_mod (nth_default 0 us i) (log_cap i) - else nth_default 0 us i) + - if eq_nat_dec i (fi (S (fi i))) - then fc (nth_default 0 us (fi i) >> log_cap (fi i)) - else 0. - Proof using Type. - intros; autorewrite with push_nth_default natsimplify; break_match; omega. - Qed. - Hint Rewrite @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. - - Lemma nth_default_carry_simple - : forall i us, - (0 <= i < length us)%nat - -> nth_default 0 (carry_simple limb_widths i us) i - = Z.pow2_mod (nth_default 0 us i) (log_cap i). - Proof using Type. - intros; autorewrite with push_nth_default natsimplify; break_match; omega. - Qed. - Hint Rewrite @nth_default_carry_simple using (omega || distr_length; omega) : push_nth_default. -End carrying. - -Hint Rewrite @length_carry_gen : distr_length. -Hint Rewrite @length_carry_simple @length_carry_simple_sequence @length_make_chain @length_full_carry_chain @length_carry_simple_full : distr_length. -Hint Rewrite @nth_default_carry_simple_full @nth_default_carry_gen_full : push_nth_default. -Hint Rewrite @nth_default_carry_simple @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. +End UniformBase.
\ No newline at end of file |