diff options
Diffstat (limited to 'src/LegacyArithmetic/Pow2BaseProofs.v')
| -rw-r--r-- | src/LegacyArithmetic/Pow2BaseProofs.v | 555 |
1 files changed, 555 insertions, 0 deletions
diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v new file mode 100644 index 000000000..8a38275dd --- /dev/null +++ b/src/LegacyArithmetic/Pow2BaseProofs.v @@ -0,0 +1,555 @@ +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.micromega.Psatz. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Coq.Lists.List. +Require Import Coq.funind.Recdef. +Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil. +Require Import Crypto.LegacyArithmetic.VerdiTactics. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.UniquePose. +Require Import Crypto.Util.Tactics.RewriteHyp. +Require Import Crypto.LegacyArithmetic.Pow2Base. +Require Import Crypto.Util.Notations. +Require Export Crypto.Util.Bool. +Require Export Crypto.Util.FixCoqMistakes. +Local Open Scope Z_scope. + +Require Crypto.LegacyArithmetic.BaseSystemProofs. + +Create HintDb simpl_add_to_nth discriminated. +Create HintDb push_upper_bound discriminated. +Create HintDb pull_upper_bound discriminated. +Create HintDb push_base_from_limb_widths discriminated. +Create HintDb pull_base_from_limb_widths discriminated. + +Hint Extern 1 => progress autorewrite with push_upper_bound in * : push_upper_bound. +Hint Extern 1 => progress autorewrite with pull_upper_bound in * : pull_upper_bound. +Hint Extern 1 => progress autorewrite with push_base_from_limb_widths in * : push_base_from_limb_widths. +Hint Extern 1 => progress autorewrite with pull_base_from_limb_widths in * : pull_base_from_limb_widths. + +Section Pow2BaseProofs. + Context {limb_widths} (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w). + Local Notation base := (base_from_limb_widths limb_widths). + + Lemma base_from_limb_widths_length ls : length (base_from_limb_widths ls) = length ls. + Proof using Type. + clear limb_widths limb_widths_nonneg. + induction ls; [ reflexivity | simpl in * ]. + autorewrite with distr_length; auto. + Qed. + Hint Rewrite base_from_limb_widths_length : distr_length. + + Lemma base_from_limb_widths_cons : forall l0 l, + base_from_limb_widths (l0 :: l) = 1 :: map (Z.mul (two_p l0)) (base_from_limb_widths l). + Proof using Type. reflexivity. Qed. + Hint Rewrite base_from_limb_widths_cons : push_base_from_limb_widths. + Hint Rewrite <- base_from_limb_widths_cons : pull_base_from_limb_widths. + + Lemma base_from_limb_widths_nil : base_from_limb_widths nil = nil. + Proof using Type. reflexivity. Qed. + Hint Rewrite base_from_limb_widths_nil : push_base_from_limb_widths. + + Lemma firstn_base_from_limb_widths : forall n, firstn n (base_from_limb_widths limb_widths) = base_from_limb_widths (firstn n limb_widths). + Proof using Type. + clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *) + 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. + 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 using Type*. + unfold sum_firstn; intros. + apply fold_right_invariant; try omega. + eauto using Z.add_nonneg_nonneg, limb_widths_nonneg, In_firstn. + Qed. Hint Resolve sum_firstn_limb_widths_nonneg. + + 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 -> + nth_error base (S i) = Some (two_p w * b). + Proof using Type. + clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *) + induction limb_widths; intros ? ? ? ? nth_err_w nth_err_b; + unfold base_from_limb_widths in *; fold base_from_limb_widths in *; + [rewrite (@nil_length0 Z) in *; omega | ]. + simpl in *. + case_eq i; intros; subst. + + subst; apply nth_error_first in nth_err_w. + apply nth_error_first in nth_err_b; subst. + apply map_nth_error. + case_eq l; intros; subst; [simpl in *; omega | ]. + unfold base_from_limb_widths; fold base_from_limb_widths. + reflexivity. + + simpl in nth_err_w. + apply nth_error_map in nth_err_w. + destruct nth_err_w as [x [A B] ]. + subst. + replace (two_p w * (two_p a * x)) with (two_p a * (two_p w * x)) by ring. + apply map_nth_error. + apply IHl; auto. omega. + Qed. + + + Lemma nth_error_base : forall i, (i < length limb_widths)%nat -> + nth_error base i = Some (two_p (sum_firstn limb_widths i)). + Proof using Type*. + induction i; intros. + + unfold sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity. + intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega. + + assert (i < length limb_widths)%nat as lt_i_length by omega. + specialize (IHi lt_i_length). + destruct (nth_error_length_exists_value _ _ lt_i_length) as [w nth_err_w]. + erewrite base_from_limb_widths_step; eauto. + f_equal. + simpl. + destruct (NPeano.Nat.eq_dec i 0). + - subst; unfold sum_firstn; simpl. + apply nth_error_exists_first in nth_err_w. + destruct nth_err_w as [l' lw_destruct]; subst. + simpl; ring_simplify. + f_equal; ring. + - erewrite sum_firstn_succ; eauto. + symmetry. + apply two_p_is_exp; auto using sum_firstn_limb_widths_nonneg. + apply limb_widths_nonneg. + eapply nth_error_value_In; eauto. + Qed. + + Lemma nth_default_base : forall d i, (i < length limb_widths)%nat -> + nth_default d base i = 2 ^ (sum_firstn limb_widths i). + Proof using Type*. + intros ? ? i_lt_length. + apply nth_error_value_eq_nth_default. + rewrite nth_error_base, two_p_correct by assumption. + reflexivity. + 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]. + Qed. + + Lemma base_from_limb_widths_app : forall l0 l + (l0_nonneg : forall x, In x l0 -> 0 <= x) + (l_nonneg : forall x, In x l -> 0 <= x), + base_from_limb_widths (l0 ++ l) + = base_from_limb_widths l0 ++ map (Z.mul (two_p (sum_firstn l0 (length l0)))) (base_from_limb_widths l). + Proof using Type. + induction l0 as [|?? IHl0]. + { simpl; intros; rewrite <- map_id at 1; apply map_ext; intros; omega. } + { simpl; intros; rewrite !IHl0, !map_app, map_map, sum_firstn_succ_cons, two_p_is_exp by auto with znonzero. + do 2 f_equal; apply map_ext; intros; lia. } + Qed. + + Lemma skipn_base_from_limb_widths : forall n, skipn n (base_from_limb_widths limb_widths) = map (Z.mul (two_p (sum_firstn limb_widths n))) (base_from_limb_widths (skipn n limb_widths)). + Proof using Type*. + intro n; pose proof (base_from_limb_widths_app (firstn n limb_widths) (skipn n limb_widths)) as H. + specialize_by eauto using In_firstn, In_skipn. + autorewrite with simpl_firstn simpl_skipn in *. + rewrite H, skipn_app, skipn_all by auto with arith distr_length; clear H. + simpl; distr_length. + apply Min.min_case_strong; intro; + unfold sum_firstn; autorewrite with natsimplify simpl_skipn simpl_firstn; + reflexivity. + Qed. + 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. + Proof using Type. + clear. + repeat match goal with + | |- _ => progress (cbv [bounded]; intros) + | |- _ => break_if + | |- _ => apply Z.bits_inj' + | |- _ => rewrite Z.testbit_pow2_mod by (apply nth_default_preserves_properties; auto; omega) + | |- _ => reflexivity + end. + specialize (H0 i). + symmetry. + rewrite <- (Z.mod_pow2_bits_high (nth_default 0 us i) (nth_default 0 lw i) n); + [ rewrite Z.mod_small by omega; reflexivity | ]. + split; try omega. + apply nth_default_preserves_properties; auto; omega. + Qed. + + Lemma bounded_nil_iff : forall us, bounded nil us <-> (forall u, In u us -> u = 0). + Proof using Type. + clear. + split; cbv [bounded]; intros. + + edestruct (In_nth_error_value us u); try assumption. + specialize (H x). + replace u with (nth_default 0 us x) by (auto using nth_error_value_eq_nth_default). + rewrite nth_default_nil, Z.pow_0_r in H. + omega. + + rewrite nth_default_nil, Z.pow_0_r. + apply nth_default_preserves_properties; try omega. + intros. + apply H in H0. + omega. + Qed. + + Lemma bounded_iff : forall lw us, bounded lw us <-> forall i, 0 <= nth_default 0 us i < 2 ^ nth_default 0 lw i. + Proof using Type. + clear. + cbv [bounded]; intros. + reflexivity. + Qed. + + Lemma digit_select : forall us i, bounded limb_widths us -> + 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, 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. + - rewrite nth_default_cons, sum_firstn_0, Z.shiftr_0_r. + 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; + try solve [intros; exfalso; eauto using in_nil]. + rewrite !nth_default_nil, BaseSystemProofs.decode_base_nil; auto. + cbv. auto using in_eq. + * rewrite nth_default_cons, base_from_limb_widths_cons, BaseSystemProofs.peel_decode. + fold (BaseSystem.mul_each (two_p w)). + 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 *. + specialize (H 0%nat); rewrite !nth_default_cons in H. + rewrite <-Z.lor_shiftl by (auto using in_eq; omega). + apply Z.bits_inj'; intros. + rewrite Z.testbit_pow2_mod by auto using in_eq. + break_if. { + autorewrite with Ztestbit; break_match; + try rewrite Z.testbit_neg_r with (n := n - w) by omega; + autorewrite with bool_congr; + f_equal; ring. + } { + replace a with (a mod 2 ^ w) by (auto using Z.mod_small). + apply Z.mod_pow2_bits_high. split; auto using in_eq; omega. + } + - rewrite nth_default_cons_S. + 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, 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, BaseSystemProofs.peel_decode. + fold (BaseSystem.mul_each (two_p w)). + 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 *. + rewrite Z.shiftr_add_shiftl_high by first + [ 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)); + rewrite !nth_default_cons_S in H; assumption). + repeat f_equal; try ring. + Qed. + + Lemma nth_default_limb_widths_nonneg : forall i, 0 <= nth_default 0 limb_widths i. + Proof using Type*. + intros; apply nth_default_preserves_properties; auto; omega. + Qed. Hint Resolve nth_default_limb_widths_nonneg. + + Lemma decode_firstn_pow2_mod : forall us i, + (i <= length us)%nat -> + length us = length limb_widths -> + bounded limb_widths us -> + BaseSystem.decode' base (firstn i us) = Z.pow2_mod (BaseSystem.decode' base us) (sum_firstn limb_widths i). + Proof using Type*. + intros; induction i; + repeat match goal with + | |- _ => 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 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) + | |- appcontext[min ?x ?y] => (rewrite Nat.min_l by omega || rewrite Nat.min_r by omega) + | |- appcontext[2 ^ ?a * _] => rewrite (Z.mul_comm (2 ^ a)); rewrite <-Z.shiftl_mul_pow2 + | |- _ => solve [auto] + | |- _ => lia + end. + rewrite digit_select by assumption; apply Z.bits_inj'. + repeat match goal with + | |- _ => progress intros + | |- _ => progress autorewrite with Ztestbit + | |- _ => rewrite Z.testbit_pow2_mod by (omega || trivial) + | |- _ => break_if; try omega + | H : ?a < ?b |- appcontext[Z.testbit _ (?a - ?b)] => + rewrite (Z.testbit_neg_r _ (a-b)) by omega + | |- _ => reflexivity + | |- _ => solve [f_equal; ring] + | |- _ => 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, + (i <= length us)%nat -> + length us = length limb_widths -> + bounded limb_widths us -> + sum_firstn limb_widths i <= n -> + Z.testbit (BaseSystem.decode base (firstn i us)) n = false. + Proof using Type*. + repeat match goal with + | |- _ => progress intros + | |- _ => progress autorewrite with Ztestbit + | |- _ => rewrite decode_firstn_pow2_mod + | |- _ => rewrite Z.testbit_pow2_mod + | |- _ => break_if + | |- _ => assumption + | |- _ => solve [auto] + | H : ?a <= ?b |- 0 <= ?b => assert (0 <= a) by (omega || auto); omega + end. + Qed. + + Lemma testbit_decode_high : forall us n, + length us = length limb_widths -> + bounded limb_widths us -> + sum_firstn limb_widths (length us) <= n -> + Z.testbit (BaseSystem.decode base us) n = false. + Proof using Type*. + intros. + erewrite <-(firstn_all _ us) by reflexivity. + auto using testbit_decode_firstn_high. + Qed. + + (** TODO: Figure out how to automate and clean up this proof *) + Lemma decode_nonneg : forall us, + length us = length limb_widths -> + bounded limb_widths us -> + 0 <= BaseSystem.decode base us. + Proof using Type*. + intros. + unfold bounded, BaseSystem.decode, BaseSystem.decode' in *; simpl in *. + pose 0 as zero. + assert (0 <= zero) by reflexivity. + replace base with (map (Z.mul (two_p zero)) base) + by (etransitivity; [ | apply map_id ]; apply map_ext; auto with zarith). + clearbody zero. + revert dependent zero. + generalize dependent limb_widths. + induction us as [|u us IHus]; intros [|w limb_widths'] ?? Hbounded ??; simpl in *; + try (reflexivity || congruence). + pose proof (Hbounded 0%nat) as Hbounded0. + pose proof (fun n => Hbounded (S n)) as HboundedS. + unfold nth_default, nth_error in Hbounded0. + unfold nth_default in HboundedS. + rewrite map_map. + unfold BaseSystem.accumulate at 1; simpl. + assert (0 < two_p zero) by (rewrite two_p_equiv; auto with zarith). + replace (map (fun x => two_p zero * (two_p w * x)) (base_from_limb_widths limb_widths')) with (map (Z.mul (two_p (zero + w))) (base_from_limb_widths limb_widths')) + by (apply map_ext; rewrite two_p_is_exp by auto with zarith omega; auto with zarith). + change 0 with (0 + 0) at 1. + apply Z.add_le_mono; simpl in *; auto with zarith. + Qed. + + Lemma decode_upper_bound : forall us, + length us = length limb_widths -> + bounded limb_widths us -> + 0 <= BaseSystem.decode base us < upper_bound limb_widths. + Proof using Type*. + cbv [upper_bound]; intros. + split. + { apply decode_nonneg; auto. } + { apply Z.testbit_false_bound; auto; intros. + rewrite testbit_decode_high; auto; + replace (length us) with (length limb_widths); try omega. } + 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 BaseSystemProofs.decode'_splice; autorewrite with push_firstn. + apply Z.add_cancel_l. + autorewrite with pull_base_from_limb_widths Zshift_to_pow zsimplify. + rewrite BaseSystemProofs.decode'_map_mul, two_p_correct; nia. + Qed. + + Lemma decode_shift : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> + BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0)). + Proof using Type*. + intros; etransitivity; [ apply (decode_shift_app (u0::nil)); assumption | ]. + transitivity (u0 * 1 + 0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0 + 0))); [ | autorewrite with zsimplify; reflexivity ]. + destruct limb_widths; distr_length; reflexivity. + Qed. + + Lemma upper_bound_nil : upper_bound nil = 1. + Proof using Type. reflexivity. Qed. + + Lemma upper_bound_cons x xs : 0 <= x -> 0 <= sum_firstn xs (length xs) -> upper_bound (x::xs) = 2^x * upper_bound xs. + Proof using Type. + intros Hx Hxs. + unfold upper_bound; simpl. + autorewrite with simpl_sum_firstn pull_Zpow. + reflexivity. + Qed. + + Lemma upper_bound_app xs ys : 0 <= sum_firstn xs (length xs) -> 0 <= sum_firstn ys (length ys) -> upper_bound (xs ++ ys) = upper_bound xs * upper_bound ys. + Proof using Type. + intros Hxs Hys. + unfold upper_bound; simpl. + autorewrite with distr_length simpl_sum_firstn pull_Zpow. + reflexivity. + Qed. + +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. +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. +Hint Rewrite <- @upper_bound_cons @upper_bound_app using solve [ eauto with znonzero ] : pull_upper_bound. + +Section UniformBase. + Context {width : Z} (limb_width_nonneg : 0 <= width). + Context (limb_widths : list Z) + (limb_widths_uniform : forall w, In w limb_widths -> w = width). + Local Notation base := (base_from_limb_widths limb_widths). + + Lemma bounded_uniform : forall us, (length us <= length limb_widths)%nat -> + (bounded limb_widths us <-> (forall u, In u us -> 0 <= u < 2 ^ width)). + Proof using Type*. + cbv [bounded]; split; intro A; intros. + + let G := fresh "G" in + match goal with H : In _ us |- _ => + eapply In_nth in H; destruct H as [? G]; destruct G as [? G]; + rewrite <-nth_default_eq in G; rewrite <-G end. + specialize (A x). + split; try eapply A. + eapply Z.lt_le_trans; try apply A. + apply nth_default_preserves_properties; [ | apply Z.pow_le_mono_r; omega ] . + intros; apply Z.eq_le_incl. + f_equal; auto. + + apply nth_default_preserves_properties_length_dep; + try solve [apply nth_default_preserves_properties; split; zero_bounds; rewrite limb_widths_uniform; auto || omega]. + intros; apply nth_default_preserves_properties_length_dep; try solve [intros; omega]. + let x := fresh "x" in intro x; intros; + replace x with width; try symmetry; auto. + Qed. + + Lemma uniform_limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. + Proof using Type*. + intros. + replace w with width by (symmetry; auto). + assumption. + Qed. + + Lemma nth_default_uniform_base_full : forall i, + nth_default 0 limb_widths i = if lt_dec i (length limb_widths) + then width else 0. + Admitted. + + Lemma nth_default_uniform_base : forall i, (i < length limb_widths)%nat -> + nth_default 0 limb_widths i = width. + Proof using Type*. + intros; rewrite nth_default_uniform_base_full. + edestruct lt_dec; omega. + Qed. + + Lemma sum_firstn_uniform_base : forall i, (i <= length limb_widths)%nat -> + sum_firstn limb_widths i = Z.of_nat i * width. + Proof using limb_widths_uniform. + clear limb_width_nonneg. (* clear this before induction so we don't depend on this *) + induction limb_widths as [|x xs IHxs]; (intros [|i] ?); + simpl @length in *; + autorewrite with simpl_sum_firstn push_Zof_nat zsimplify; + try reflexivity; + try omega. + assert (x = width) by auto with datatypes; subst. + rewrite IHxs by auto with datatypes omega; omega. + Qed. + + Lemma sum_firstn_uniform_base_strong : forall i, (length limb_widths <= i)%nat -> + sum_firstn limb_widths i = Z.of_nat (length limb_widths) * width. + Proof using limb_widths_uniform. + intros; rewrite sum_firstn_all, sum_firstn_uniform_base by omega; reflexivity. + Qed. + + Lemma upper_bound_uniform : upper_bound limb_widths = 2^(Z.of_nat (length limb_widths) * width). + Proof using limb_widths_uniform. + unfold upper_bound; rewrite sum_firstn_uniform_base_strong by omega; reflexivity. + Qed. + + (* TODO : move *) + Lemma decode_truncate_base : forall us bs, BaseSystem.decode bs us = BaseSystem.decode (firstn (length us) bs) us. + Proof using Type. + clear. + induction us; intros. + + rewrite !BaseSystemProofs.decode_nil; reflexivity. + + distr_length. + destruct bs. + - rewrite firstn_nil, !BaseSystemProofs.decode_base_nil; reflexivity. + - rewrite firstn_cons, !BaseSystemProofs.peel_decode. + f_equal. + apply IHus. + Qed. + + (* TODO : move *) + Lemma tl_repeat : forall {A} xs n (x : A), (forall y, In y xs -> y = x) -> + (n < length xs)%nat -> + firstn n xs = firstn n (tl xs). + Proof using Type. + intros. + erewrite (repeat_spec_eq xs) by first [ eassumption | reflexivity ]. + rewrite ListUtil.tl_repeat. + autorewrite with push_firstn. + apply f_equal; omega *. + 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 using limb_widths_uniform. + intros. + 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. + eauto using tl_repeat. + Qed. + + Lemma decode_shift_uniform_tl : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> + BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << width). + Proof using Type*. + intros. + rewrite <- (nth_default_uniform_base 0) by distr_length. + rewrite decode_shift by auto using uniform_limb_widths_nonneg. + reflexivity. + Qed. + + Lemma decode_shift_uniform_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) << (Z.of_nat (length us0) * width)). + Proof using Type*. + intros. + rewrite <- sum_firstn_uniform_base by (distr_length; omega). + rewrite decode_shift_app by auto using uniform_limb_widths_nonneg. + reflexivity. + Qed. +End UniformBase.
\ No newline at end of file |