From 993a19e07ebf6e178e23fe6c02a2f25736835c1d Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 21 Sep 2017 10:27:12 +0200
Subject: Some lemmas.

---
 lib/Integers.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'lib')

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
-- 
cgit