From 7b4e6a522bcf1f247ef9b3517af328b5da670a98 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 4 Oct 2019 17:57:25 +0200 Subject: Ibuiltin proof --- lib/Floats.v | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++- lib/Integers.v | 38 +++++++++++++++++++++++++---------- 2 files changed, 89 insertions(+), 12 deletions(-) (limited to 'lib') 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 -- cgit