diff options
Diffstat (limited to 'lib/Integers.v')
-rw-r--r-- | lib/Integers.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index c44fa55f..5fe8202d 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -5097,6 +5097,13 @@ Proof. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. Qed. +Lemma to_int_of_int: + forall n, to_int (of_int n) = n. +Proof. + intros; unfold of_int, to_int. rewrite unsigned_repr. apply Int.repr_unsigned. + unfold max_unsigned. rewrite modulus_eq32. destruct (Int.unsigned_range n); omega. +Qed. + End AGREE32. Section AGREE64. @@ -5200,6 +5207,13 @@ Proof. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr. Qed. +Lemma to_int64_of_int64: + forall n, to_int64 (of_int64 n) = n. +Proof. + intros; unfold of_int64, to_int64. rewrite unsigned_repr. apply Int64.repr_unsigned. + unfold max_unsigned. rewrite modulus_eq64. destruct (Int64.unsigned_range n); omega. +Qed. + End AGREE64. Hint Resolve |