From 655c6a861b426db3e5da942faaef7f5caed224e3 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@univ-grenoble-alpes.fr>
Date: Fri, 4 Oct 2019 11:38:12 +0200
Subject: Adding decidable equality for int

---
 lib/Integers.v | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'lib/Integers.v')

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