From d0c486b975064d30e6fe88baca1f4a9f26ba9fb5 Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 18 Jun 2017 15:08:55 -0400 Subject: proved eval_drop_high --- src/Arithmetic/Saturated.v | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'src/Arithmetic/Saturated.v') 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. -- cgit v1.2.3