Ibuiltin proof

2 files changed, 89 insertions, 12 deletions

diff --git a/lib/Floats.v b/lib/Floats.v
index 13350dd0..272efa52 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -16,7 +16,7 @@
 
 (** Formalization of floating-point numbers, using the Flocq library. *)
 
-Require Import Coqlib Zbits Integers.
+Require Import Coqlib Zbits Integers Axioms.
 (*From Flocq*)
 Require Import Binary Bits Core.
 Require Import IEEE754_extra.
@@ -27,8 +27,69 @@ Close Scope R_scope.
 Open Scope Z_scope.
 
 Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *)
+
+Definition float_eq: forall (i1 i2: float), {i1=i2} + {i1<>i2}.
+Proof.
+  intros. destruct i1.
+(* B754_zero *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + apply eqb_prop in BEQ. subst. left. reflexivity.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_infinity *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + apply eqb_prop in BEQ. subst. left. reflexivity.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_nan *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + generalize (Pos.eq_dec pl pl0). intro. inv H.
+      ++ left. apply eqb_prop in BEQ. subst.
+         assert (e = e0) by (apply proof_irr). congruence.
+      ++ right. intro. inv H. contradiction.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_finite *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ; [apply eqb_prop in BEQ | apply eqb_false_iff in BEQ].
+    generalize (Pos.eq_dec m m0). intro. inv H.
+    generalize (Z.eq_dec e e1). intro. inv H.
+    1: { left. assert (e0 = e2) by (apply proof_irr). congruence. }
+    all: right; intro; inv H; contradiction.
+Qed.
+
 Definition float32 := binary32. (**r the type of IEE754 single-precision FP numbers *)
 
+Definition float32_eq: forall (i1 i2: float32), {i1=i2} + {i1<>i2}.
+Proof.
+  intros. destruct i1.
+(* B754_zero *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + apply eqb_prop in BEQ. subst. left. reflexivity.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_infinity *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + apply eqb_prop in BEQ. subst. left. reflexivity.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_nan *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ.
+    + generalize (Pos.eq_dec pl pl0). intro. inv H.
+      ++ left. apply eqb_prop in BEQ. subst.
+         assert (e = e0) by (apply proof_irr). congruence.
+      ++ right. intro. inv H. contradiction.
+    + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction.
+(* B754_finite *)
+  - destruct i2; try (right; discriminate).
+    destruct (eqb s s0) eqn:BEQ; [apply eqb_prop in BEQ | apply eqb_false_iff in BEQ].
+    generalize (Pos.eq_dec m m0). intro. inv H.
+    generalize (Z.eq_dec e e1). intro. inv H.
+    1: { left. assert (e0 = e2) by (apply proof_irr). congruence. }
+    all: right; intro; inv H; contradiction.
+Qed.
+
 (** Boolean-valued comparisons *)
 
 Definition cmp_of_comparison (c: comparison) (x: option Datatypes.comparison) : bool :=
diff --git a/lib/Integers.v b/lib/Integers.v
index fca44b1e..9c6fcf1d 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -101,17 +101,6 @@ 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 :=
@@ -4167,8 +4156,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 *)
@@ -4445,6 +4452,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