aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Arithmetic/Saturated.v16
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.