diff options
| author | Cyril SIX <cyril.six@univ-grenoble-alpes.fr> | 2019-10-04 11:38:12 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@univ-grenoble-alpes.fr> | 2019-10-04 11:38:12 +0200 |
| commit | 655c6a861b426db3e5da942faaef7f5caed224e3 (patch) | |
| tree | 9c3d9f7e3e48e6c722cd443229b410b496b21cb1 /lib/Integers.v | |
| parent | 79d48fa72a3ac0cd2b84dc8c70eb9170088e0353 (diff) | |
| download | compcert-kvx-655c6a861b426db3e5da942faaef7f5caed224e3.tar.gz compcert-kvx-655c6a861b426db3e5da942faaef7f5caed224e3.zip | |
Adding decidable equality for int
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index f4213332..fca44b1e 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -16,7 +16,7 @@ (** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *) Require Import Eqdep_dec Zquot Zwf. -Require Import Coqlib Zbits. +Require Import Coqlib Zbits Axioms. Require Archi. (** * Comparisons *) @@ -101,6 +101,17 @@ Hint Resolve modulus_pos: ints. Record int: Type := mkint { intval: Z; intrange: -1 < intval < modulus }. +Definition int_eq: forall (i1 i2: int), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval0 intval1). intro. + inversion H0. + - subst. left. assert (intrange0 = intrange1) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + +(* TODO - continue for the rest *) + (** Fast normalization modulo [2^wordsize] *) Definition Z_mod_modulus (x: Z) : Z := |