diff options
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 1eb59c5..c54b6fe 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -657,6 +657,13 @@ Proof. apply eqm_samerepr. unfold z'; red. exists 1. omega. Qed. +Theorem signed_eq_unsigned: + forall x, unsigned x <= max_signed -> signed x = unsigned x. +Proof. + intros. unfold signed. destruct (zlt (unsigned x) half_modulus). + auto. unfold max_signed in H. omegaContradiction. +Qed. + (** ** Properties of addition *) Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y). @@ -786,6 +793,13 @@ Proof. symmetry. apply sub_add_opp. Qed. +Theorem sub_signed: + forall x y, sub x y = repr (signed x - signed y). +Proof. + intros. unfold sub. apply eqm_samerepr. + apply eqm_sub; apply eqm_sym; apply eqm_signed_unsigned. +Qed. + (** ** Properties of multiplication *) Theorem mul_commut: forall x y, mul x y = mul y x. @@ -2565,4 +2579,15 @@ Proof. omega. Qed. +Theorem ltu_range_test: + forall x y, + ltu x y = true -> unsigned y <= max_signed -> + 0 <= signed x < unsigned y. +Proof. + intros. + unfold Int.ltu in H. destruct (zlt (unsigned x) (unsigned y)); try discriminate. + rewrite signed_eq_unsigned. + generalize (unsigned_range x). omega. omega. +Qed. + End Int. |