Commit 2be203fb authored by Heiko Becker's avatar Heiko Becker

Reinitialize branch for fixed-point arithmetic checking, as the old branch somehow got

botched up by a merge.
parent 67d57ae8
This diff is collapsed.
......@@ -5,13 +5,15 @@
@maintainer: Heiko Becker
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qpower
Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Flover.Infra.RealRationalProps.
(**
Define machine precision as datatype
Define machine precision as datatype. We treat Fixed-point types as floats,
like Flocq, where f:positive specifies the fraction size
**)
Inductive mType: Type := M0 | M16 | M32 | M64. (*| M128 | M256*)
Inductive mType: Type := M0 | M16 | M32 | M64 | F (f:positive). (*| M128 | M256*)
(**
Injection of machine types into Q
......@@ -22,6 +24,7 @@ Definition mTypeToQ (e:mType) :Q :=
| M16 => (Qpower (2#1) (Zneg 11))
| M32 => (Qpower (2#1) (Zneg 24))
| M64 => (Qpower (2#1) (Zneg 53))
| F f => Qpower (2#1) (Zneg f)
(*
(* the epsilons below match what is used internally in flover,
although these value do not match the IEEE standard *)
......@@ -35,8 +38,9 @@ Lemma mTypeToQ_pos_Q:
forall e, 0 <= mTypeToQ e.
Proof.
intro e.
case_eq e; intro;
simpl mTypeToQ; apply Qle_bool_iff; auto.
case_eq e; intros;
unfold mTypeToQ; try (apply Qle_bool_iff; auto; fail).
apply Qpower_pos; lra.
Qed.
Lemma mTypeToQ_pos_R :
......@@ -54,25 +58,28 @@ Definition mTypeEq (m1:mType) (m2:mType) :=
| M16, M16 => true
| M32, M32 => true
| M64, M64 => true
| F f1, F f2 => (f1 =? f2)%positive
(* | M128, M128 => true *)
(* | M256, M256 => true *)
| _, _ => false
end.
Lemma mTypeEq_refl (m:mType):
mTypeEq m m = true.
Proof.
intros. destruct m; try auto; simpl. apply Pos.eqb_refl.
Qed.
Lemma mTypeEq_compat_eq(m1:mType) (m2:mType):
mTypeEq m1 m2 = true <-> m1 = m2.
Proof.
split; intros eq_case;
case_eq m1; intros m1_case;
case_eq m2; intros m2_case; subst;
case_eq m1; intros * m1_case;
case_eq m2; intros * m2_case; subst;
try congruence; try auto;
cbv in eq_case; inversion eq_case.
Qed.
Lemma mTypeEq_refl (m:mType):
mTypeEq m m = true.
Proof.
intros. rewrite mTypeEq_compat_eq; auto.
try simpl in eq_case; try inversion eq_case.
- f_equal. auto using Peqb_true_eq.
- inversion m2_case. apply mTypeEq_refl.
Qed.
Lemma mTypeEq_compat_eq_false (m1:mType) (m2:mType):
......@@ -81,7 +88,9 @@ Proof.
split; intros eq_case.
- hnf; intros; subst. rewrite mTypeEq_refl in eq_case.
congruence.
- case_eq m1; intros; case_eq m2; intros; subst; cbv; congruence.
- case_eq m1; intros; case_eq m2; intros; subst; simpl; try congruence.
assert (f <> f0) by (hnf; intros; subst; congruence).
rewrite Pos.eqb_neq; auto.
Qed.
Ltac type_conv :=
......@@ -95,7 +104,8 @@ Lemma mTypeEq_sym (m1:mType) (m2:mType):
mTypeEq m1 m2 = mTypeEq m2 m1.
Proof.
intros.
destruct m1, m2; compute; auto.
destruct m1, m2; simpl; auto.
apply Pos.eqb_sym.
Qed.
(**
......@@ -105,11 +115,20 @@ Qed.
mTypeToQ m1 <= mTypeToQ m2
**)
Definition isMorePrecise (m1:mType) (m2:mType) :=
Qle_bool (mTypeToQ m1) (mTypeToQ m2).
match m1, m2 with
|M0, _ => true
| F f1, F f2 => (f1 <=? f2)%positive
| F f, _ => false
| _ , F f => false
| _, _ => Qle_bool (mTypeToQ m1) (mTypeToQ m2)
end.
Definition morePrecise (m1:mType) (m2:mType) :=
match m1, m2 with
|M0, _ => true
|F f1, F f2 => (f1 <=? f2)%positive
| _ , F f => false
| F f, _ => false
|M16, M16 => true
|M32, M32 => true
|M32, M16 => true
......@@ -123,7 +142,10 @@ Lemma morePrecise_antisym m1 m2:
morePrecise m2 m1 = true ->
mTypeEq m1 m2 = true.
Proof.
destruct m1; destruct m2; cbv; auto.
destruct m1; destruct m2; simpl; auto.
intros le_m1m2 le_m2m1. apply Pos.eqb_eq.
apply Pos.leb_le in le_m1m2; apply Pos.leb_le in le_m2m1.
apply Pos.le_antisym; auto.
Qed.
Lemma morePrecise_trans m1 m2 m3:
......@@ -131,20 +153,24 @@ Lemma morePrecise_trans m1 m2 m3:
morePrecise m2 m3 = true ->
morePrecise m1 m3 = true.
Proof.
destruct m1; destruct m2; destruct m3; cbv; auto.
destruct m1; destruct m2; destruct m3; simpl; auto;
intros le1 le2; try congruence.
apply Pos.leb_le. apply Pos.leb_le in le1.
apply Pos.leb_le in le2.
eapply Pos.le_trans; eauto.
Qed.
Lemma isMorePrecise_morePrecise m1 m2:
isMorePrecise m1 m2 = morePrecise m1 m2.
Proof.
destruct m1 eqn:?, m2 eqn:?; compute; auto.
destruct m1 eqn:?, m2 eqn:?; simpl; auto.
Qed.
Lemma isMorePrecise_refl (m:mType) :
isMorePrecise m m = true.
Proof.
unfold isMorePrecise; simpl.
apply Qle_bool_iff; lra.
unfold isMorePrecise; destruct m; simpl; try auto.
apply Pos.leb_le. apply Pos.le_refl.
Qed.
Lemma M0_least_precision (m:mType) :
......@@ -186,6 +212,7 @@ Definition maxExponent (m:mType) :positive :=
| M16 => 15
| M32 => 127
| M64 => 1023
| F f => f
end.
Definition minExponentPos (m:mType) :positive :=
......@@ -194,6 +221,7 @@ Definition minExponentPos (m:mType) :positive :=
| M16 => 14
| M32 => 126
| M64 => 1022
| F f => f
end.
(**
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment