diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-09-21 10:27:12 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-09-21 10:27:12 +0200 |
| commit | 993a19e07ebf6e178e23fe6c02a2f25736835c1d (patch) | |
| tree | d50145fd7b66aaa00df9ad6cf224777cacbc7e80 /lib/Integers.v | |
| parent | d51a87f29fffbe6416799d23da7af98d0b9f0d25 (diff) | |
| download | compcert-kvx-993a19e07ebf6e178e23fe6c02a2f25736835c1d.tar.gz compcert-kvx-993a19e07ebf6e178e23fe6c02a2f25736835c1d.zip | |
Some lemmas.
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 |