diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-11-13 14:14:17 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-11-13 14:14:17 +0100 |
| commit | f2cf6d4e0600d4a58677a7531e8516a37fe1d0da (patch) | |
| tree | adf79d4780ffb2aa8733a70da461239270e5c21e /lib/Integers.v | |
| parent | 24406a351e9d64c2953b0b9fc7ef0b3d79db9b85 (diff) | |
| parent | 847554275608bafcbfad635684e588501e00ac31 (diff) | |
| download | compcert-kvx-f2cf6d4e0600d4a58677a7531e8516a37fe1d0da.tar.gz compcert-kvx-f2cf6d4e0600d4a58677a7531e8516a37fe1d0da.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 34 |
1 files changed, 33 insertions, 1 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 3b6c35eb..3e78ee60 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 *) @@ -29,6 +29,11 @@ Inductive comparison : Type := | Cgt : comparison (**r greater than *) | Cge : comparison. (**r greater than or equal *) +Definition comparison_eq: forall (x y: comparison), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + Definition negate_comparison (c: comparison): comparison := match c with | Ceq => Cne @@ -4535,8 +4540,26 @@ End Int64. Strategy 0 [Wordsize_64.wordsize]. +Definition int_eq: forall (i1 i2: int), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Notation int64 := Int64.int. +Definition int64_eq: forall (i1 i2: int64), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Global Opaque Int.repr Int64.repr Byte.repr. (** * Specialization to offsets in pointer values *) @@ -4813,6 +4836,15 @@ Strategy 0 [Wordsize_Ptrofs.wordsize]. Notation ptrofs := Ptrofs.int. +Definition ptrofs_eq: forall (i1 i2: ptrofs), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Global Opaque Ptrofs.repr. Hint Resolve Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans |