diff options
Diffstat (limited to 'src/Util/ZBounded.v')
-rw-r--r-- | src/Util/ZBounded.v | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/src/Util/ZBounded.v b/src/Util/ZBounded.v index cce5d1d44..64cb57b0a 100644 --- a/src/Util/ZBounded.v +++ b/src/Util/ZBounded.v @@ -128,15 +128,27 @@ Defined. Definition modulo (z : Z) (r : zrange) : zbounded r. Proof. - refine {| value := lower r + Z.modulo (z - lower r) (upper r - lower r) |}. + refine {| value := if (upper r <? lower r) + then z + else lower r + Z.modulo (z - lower r) (upper r - lower r + 1) |}. abstract ( destruct (upper r <? lower r) eqn:H; [ reflexivity | ]; - pose proof (Z.mod_pos_bound (z - lower r) (upper r - lower r)) as Hmod; + pose proof (Z.mod_pos_bound (z - lower r) (upper r - lower r + 1)) as Hmod; destruct r as [l u]; simpl in *; apply Bool.andb_true_iff; split; destruct (l =? u) eqn:H'; Z.ltb_to_lt; subst; - rewrite ?Z.sub_diag, ?Zmod_0_r, ?Z.add_0_r; - try reflexivity; omega + repeat rewrite ?Z.sub_diag, ?Zmod_0_r, ?Z.add_0_r, ?Z.add_0_l, ?Z.mod_1_r; + try reflexivity; try omega ). Defined. + +Lemma modulo_value_id {r} (v : zbounded r) : modulo (value v) r = v. +Proof. + apply path_zbounded; simpl. + destruct v as [v H]; simpl. + destruct (upper r <? lower r) eqn:H'; [ reflexivity | ]. + simpl in *; unfold is_true in *; split_andb; Z.ltb_to_lt. + rewrite Z.mod_small by omega. + omega. +Qed. |