From 5475629802b34912b2d280b3a1ae54187a721124 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 21 Apr 2017 12:11:10 -0400 Subject: prove compact obeys div/mod rule --- src/Arithmetic/Saturated.v | 161 +++++++++++++++++++++++++++++---------------- 1 file changed, 105 insertions(+), 56 deletions(-) (limited to 'src/Arithmetic') diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index 884a59ef7..addfe08e5 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -127,6 +127,12 @@ Module Columns. Proof. reflexivity. Qed. Hint Rewrite eval_unit : push_basesystem_eval. + Lemma eval_single (x:list Z) : eval (n:=1) x = sum x. + Proof. + cbv [eval]. simpl map. cbv - [Z.mul Z.add sum]. + rewrite weight_0; ring. + Qed. Hint Rewrite eval_single : push_basesystem_eval. + Definition eval_from {n} (offset:nat) (x : (list Z)^n) : Z := B.Positional.eval (fun i => weight (i+offset)) (Tuple.map sum x). @@ -226,65 +232,103 @@ Module Columns. rewrite Z.div_add' by auto; nsatz. Qed. - Definition compact_invariant n i (starter rem:Z) (inp : tuple (list Z) n) (out : tuple Z n) := - B.Positional.eval_from weight i out + weight (i + n) * rem = eval_from i inp + weight i*starter. - - Lemma compact_invariant_holds n i starter rem inp out : - compact_invariant n (S i) (fst (compact_step_cps i starter (hd inp) id)) rem (tl inp) out -> - compact_invariant (S n) i starter rem inp (append (snd (compact_step_cps i starter (hd inp) id)) out). - Proof using Type*. - cbv [compact_invariant B.Positional.eval_from]; intros. - repeat match goal with - | _ => rewrite B.Positional.eval_step - | _ => rewrite eval_from_S - | _ => rewrite sum_cons - | _ => rewrite weight_multiples - | _ => rewrite Nat.add_succ_l in * - | _ => rewrite Nat.add_succ_r in * - | _ => (rewrite fst_fst_compact_step in * ) - | _ => progress ring_simplify - | _ => rewrite ZUtil.Z.mul_div_eq_full by apply weight_nonzero - | _ => cbv [compact_step_cps] in *; - autorewrite with uncps push_id in *; - rewrite !compact_digit_mod, !compact_digit_div in * - | _ => progress (autorewrite with natsimplify in * ) - end; - rewrite B.Positional.eval_wt_equiv with (wtb := fun i0 => weight (i0 + S i)) by (intros; f_equal; try omega). - { - rewrite Z.mod_eq by auto using Z.positive_is_nonzero. - rewrite sum_cons in H. - ring_simplify. - match type of H with - context [?y * (?a / (?y / ?x))] => - replace (y * (a / (y / x))) with (x * (y / x) * (a / (y / x))) in H - by (rewrite Z.mul_div_eq_full by auto using Z.positive_is_nonzero; - rewrite weight_multiples; ring) - end. - nsatz. - } + (* TODO : move to Core? *) + Lemma Pos_eval_unit : B.Positional.eval (n:=0) weight tt = 0. + Proof. reflexivity. Qed. + Hint Rewrite Pos_eval_unit B.Positional.eval_single + @B.Positional.eval_step : push_basesystem_eval. + (* TODO : move to Core? *) + Lemma Pos_eval_left_append {n} : forall wt x xs, + B.Positional.eval wt (left_append (n:=n) x xs) + = wt n * x + B.Positional.eval wt xs. + Proof. + induction n; intros; try destruct xs; + unfold left_append; fold @left_append; + autorewrite with push_basesystem_eval; [ring|]. + rewrite IHn. + rewrite (subst_append xs), hd_append, tl_append. + rewrite B.Positional.eval_step. + ring. + Qed. + Hint Rewrite @Pos_eval_left_append : push_basesystem_eval. + + Lemma small_mod_eq a b n: a mod n = b mod n -> 0 <= a < n -> a = b mod n. + Proof. intros; rewrite <-(Z.mod_small a n); auto. Qed. + + (* helper for some of the modular logic in compact *) + Lemma compact_mod_step a b c d: 0 < a -> 0 < b -> + a * ((c / a + d) mod b) + c mod a = (a * d + c) mod (a * b). + Proof. + intros Ha Hb. assert (a <= a * b) by (apply Z.le_mul_diag_r; omega). + pose proof (Z.mod_pos_bound c a Ha). + pose proof (Z.mod_pos_bound (c/a+d) b Hb). + apply small_mod_eq. + { rewrite <-(Z.mod_small (c mod a) (a * b)) by omega. + rewrite <-Z.mul_mod_distr_l with (c:=a) by omega. + rewrite Z.mul_add_distr_l, Z.mul_div_eq, <-Z.add_mod_full by omega. + f_equal; ring. } + { split; [zero_bounds|]. + apply Z.lt_le_trans with (m:=a*(b-1)+a); [|ring_simplify; omega]. + apply Z.add_le_lt_mono; try apply Z.mul_le_mono_nonneg_l; omega. } Qed. - - Lemma compact_invariant_base i rem : compact_invariant 0 i rem rem tt tt. - Proof using Type. cbv [compact_invariant]. simpl. repeat (f_equal; try omega). Qed. - - Lemma compact_invariant_end {n} start (input : (list Z)^n): - compact_invariant n 0%nat start (fst (mapi_with_cps compact_step_cps start input id)) input (snd (mapi_with_cps compact_step_cps start input id)). - Proof using Type*. - autorewrite with uncps push_id. - apply (mapi_with_invariant _ compact_invariant - compact_invariant_holds compact_invariant_base). + Lemma compact_div_step a b c d : 0 < a -> 0 < b -> + (c / a + d) / b = (a * d + c) / (a * b). + Proof. + intros Ha Hb. + rewrite <-Z.div_div by omega. + rewrite Z.div_add_l' by omega. + f_equal; ring. Qed. - Lemma eval_compact {n} (xs : tuple (list Z) n) : - B.Positional.eval weight (snd (compact xs)) = eval xs - (weight n * fst (compact xs)). - Proof using Type*. - pose proof (compact_invariant_end 0 xs) as Hinv. - cbv [compact_invariant] in Hinv. - simpl in Hinv. autorewrite with zsimplify natsimplify in Hinv. - rewrite eval_from_0, B.Positional.eval_from_0 in Hinv. nsatz. + Lemma compact_div_mod {n} inp : + (B.Positional.eval weight (snd (compact inp)) + = (eval inp) mod (weight n)) + /\ (fst (compact inp) = eval (n:=n) inp / weight n). + Proof. + cbv [compact compact_cps compact_step compact_step_cps]; + autorewrite with uncps push_id. + change (fun i s a => compact_digit_cps i (s :: a) id) + with (fun i s a => compact_digit i (s :: a)). + + apply mapi_with'_linvariant; [|tauto]. + + clear n inp. intros until 0. intros Hst Hys [Hmod Hdiv]. + pose proof (weight_positive n). pose proof (weight_divides n). + autorewrite with push_basesystem_eval. + destruct n; cbv [mapi_with] in *; simpl tuple in *; + [destruct xs, ys; subst; simpl| cbv [eval] in *]; + repeat match goal with + | _ => rewrite mapi_with'_left_step + | _ => rewrite compact_digit_div, sum_cons + | _ => rewrite compact_digit_mod, sum_cons + | _ => rewrite map_left_append + | _ => rewrite eval_left_append + | _ => rewrite weight_0, ?Z.div_1_r, ?Z.mod_1_r + | _ => rewrite Hdiv + | _ => rewrite Hmod + | _ => progress subst + | _ => progress autorewrite with natsimplify cancel_pair push_basesystem_eval + | _ => solve [split; ring_simplify; f_equal; ring] + end. + remember (weight (S (S n)) / weight (S n)) as bound. + replace (weight (S (S n))) with (weight (S n) * bound) + by (subst bound; rewrite Z.mul_div_eq by omega; + rewrite weight_multiples; ring). + split; [apply compact_mod_step | apply compact_div_step]; omega. Qed. + Lemma compact_mod {n} inp : + (B.Positional.eval weight (snd (compact inp)) + = (eval (n:=n) inp) mod (weight n)). + Proof. apply (proj1 (compact_div_mod inp)). Qed. + Hint Rewrite @compact_mod : push_basesystem_eval. + + Lemma compact_div {n} inp : + fst (compact inp) = eval (n:=n) inp / weight n. + Proof. apply (proj2 (compact_div_mod inp)). Qed. + Hint Rewrite @compact_div : push_basesystem_eval. + Definition cons_to_nth_cps {n} i (x:Z) (t:(list Z)^n) {T} (f:(list Z)^n->T) := @on_tuple_cps _ _ nil (update_nth_cps i (cons x)) n n t _ f. @@ -404,7 +448,8 @@ Hint Rewrite @Columns.from_associational_id : uncps. Hint Rewrite - @Columns.eval_compact + @Columns.compact_mod + @Columns.compact_div @Columns.eval_cons_to_nth @Columns.eval_from_associational @Columns.eval_nils @@ -526,9 +571,13 @@ Section Freeze. = B.Positional.eval weight p + (if (dec (cond = 0)) then 0 else B.Positional.eval weight q) - weight n * (fst (conditional_add mask cond p q)). Proof. cbv [conditional_add_cps conditional_add]; - repeat progress autounfold; rewrite ?Hmask, ?map_land_zero; + repeat progress autounfold in *; rewrite ?Hmask, ?map_land_zero; autorewrite with uncps push_id push_basesystem_eval; - break_match; ring. + break_match; + match goal with + |- context [weight ?n * (?x / weight ?n)] => + pose proof (Z.div_mod x (weight n) (weight_nonzero n)) + end; omega. Qed. Hint Rewrite @eval_conditional_add using (omega || assumption) : push_basesystem_eval. -- cgit v1.2.3