From 989f6a49cb390b6279ee8ce0ed70eb993ff1b809 Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 18 Jun 2017 15:28:55 -0400 Subject: proved eval_scmul --- src/Arithmetic/Saturated.v | 36 +++++++++++++++++++++--------------- 1 file changed, 21 insertions(+), 15 deletions(-) (limited to 'src/Arithmetic/Saturated.v') diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index 747c34501..9c7670cb5 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -166,7 +166,7 @@ Module Associational. End Associational. Hint Opaque Associational.mul Associational.multerm : uncps. Hint Rewrite @Associational.mul_id @Associational.multerm_id : uncps. -Hint Rewrite @Associational.eval_mul @Associational.eval_map_multerm : push_basesystem_eval. +Hint Rewrite @Associational.eval_mul @Associational.eval_map_multerm using (omega || assumption) : push_basesystem_eval. Module Columns. Section Columns. @@ -826,14 +826,18 @@ Section API. pose proof (@uweight_divides bound H) end. + Local Ltac pose_all := + pose_uweight bound; + pose proof Z.add_get_carry_full_div; + pose proof Z.add_get_carry_full_mod; + pose proof Z.mul_split_div; pose proof Z.mul_split_mod; + pose proof div_correct; pose proof modulo_correct. + Lemma eval_add_nz n m pred_nm p q : pred_nm <> 0%nat -> eval (@add n m pred_nm p q) = eval p + eval q. Proof. - intros. pose_uweight bound. - pose proof Z.add_get_carry_full_div. - pose proof Z.add_get_carry_full_mod. - pose proof div_correct. pose proof modulo_correct. + intros. pose_all. repeat match goal with | _ => progress (cbv [add_cps add eval Let_In]; repeat autounfold) | _ => progress autorewrite with uncps push_id cancel_pair push_basesystem_eval @@ -879,10 +883,7 @@ Section API. Local Definition compact_digit := Columns.compact_digit (add_get_carry:=Z.add_get_carry_full) (div:=div) (modulo:=modulo) (uweight bound). Lemma small_compact {n} (p:(list Z)^n) : small (snd (compact p)). Proof. - pose_uweight bound. - pose proof Z.add_get_carry_full_div. - pose proof Z.add_get_carry_full_mod. - pose proof div_correct. pose proof modulo_correct. + pose_all. match goal with |- ?G => assert (G /\ fst (compact p) = fst (compact p)); [|tauto] end. (* assert a dummy second statement so that fst (compact x) is in context *) @@ -922,10 +923,7 @@ Section API. (uweight bound n + uweight bound m <= uweight bound pred_nm) -> small a -> small b -> small (@add n m pred_nm a b). Proof. - intros. pose_uweight bound. - pose proof Z.add_get_carry_full_div. - pose proof Z.add_get_carry_full_mod. - pose proof div_correct. pose proof modulo_correct. + intros. pose_all. cbv [small add_cps add Let_In]. repeat autounfold. autorewrite with uncps push_id. rewrite to_list_left_append. @@ -965,9 +963,17 @@ Section API. apply small_left_tl. Qed. - Lemma eval_scmul n a v: eval (@scmul n a v) = a * eval v. + Lemma eval_scmul n a v : small v -> 0 <= a < bound -> + eval (@scmul n a v) = a * eval v. Proof. - Admitted. + intro Hsmall. pose_all. apply eval_small in Hsmall. + intros. cbv [scmul scmul_cps eval] in *. repeat autounfold. + autorewrite with uncps push_id push_basesystem_eval. + rewrite uweight_0, Z.mul_1_l. apply Z.mod_small. + split; [solve[Z.zero_bounds]|]. cbv [uweight] in *. + rewrite !Nat2Z.inj_succ, Z.pow_succ_r by auto using Nat2Z.is_nonneg. + apply Z.mul_lt_mono_nonneg; omega. + Qed. (* TODO : move to tuple *) Lemma from_list_tl {A n} (ls : list A) H H': -- cgit v1.2.3