diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Arithmetic/Saturated.v | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index 7b42c31e7..23c80675c 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -934,10 +934,22 @@ Section API. destruct pred_nm; autorewrite with push_basesystem_eval; rewrite Z.div_small; omega. Qed. - + + Lemma small_left_tl n (v:T (S n)) : small v -> small (left_tl v). + Proof. cbv [small]. auto using In_to_list_left_tl. Qed. + Lemma eval_drop_high n v : small v -> eval (@drop_high n v) = eval v mod (uweight bound n). - Admitted. + Proof. + cbv [drop_high drop_high_cps eval]. + rewrite Tuple.left_tl_cps_correct, push_id. (* TODO : for some reason autorewrite with uncps doesn't work here *) + intro H. apply small_left_tl in H. + rewrite (subst_left_append v) at 2. + autorewrite with push_basesystem_eval. + apply eval_small in H. + rewrite Z.mod_add_l' by (pose_uweight bound; auto). + rewrite Z.mod_small; auto. + Qed. Lemma eval_scmul n a v: eval (@scmul n a v) = a * eval v. Proof. |