Commit 7679dff6 authored by Heiko Becker's avatar Heiko Becker

WIP start moving to mTypeToQ with value param

parent b01628ba
......@@ -323,9 +323,9 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
destruct m0; destruct m1; auto.
+ destruct (mTypeEq m m1) eqn:?; type_conv;
destruct m0; destruct m1; simpl in *; try congruence.
* destruct (f0 <=? f)%positive; congruence.
* destruct (w0 <=? w)%positive; congruence.
* destruct m; try congruence.
destruct (f1 <=? f)%positive; congruence.
destruct (w1 <=? w)%positive; congruence.
- destruct (unopEq u u0) eqn:?;
destruct (unopEq u0 u1) eqn:?;
try rewrite unopEq_compat_eq in *; subst;
......@@ -354,8 +354,8 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
+ destruct (mTypeEq m m1) eqn:?; type_conv; congruence.
+ destruct (mTypeEq m m1) eqn:?; type_conv; try congruence;
destruct m0, m1; simpl in *; try congruence;
destruct (f0 <=? f)%positive; try congruence;
destruct m; try congruence; destruct (f <=? f0)%positive; congruence.
destruct (w0 <=? w)%positive; try congruence;
destruct m; try congruence; destruct (w <=? w0)%positive; congruence.
Qed.
Lemma expCompare_antisym e1:
......@@ -380,7 +380,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
* destruct m, m0; simpl in *; try congruence.
rewrite Pos.leb_nle in Heqb0, Heqb1.
rewrite <- Pos.lt_nle in Heqb0, Heqb1.
assert (f < f)%positive by (eapply Pos.lt_trans; eauto).
assert (w < w)%positive by (eapply Pos.lt_trans; eauto).
pose proof (Pos.lt_irrefl _ H). inversion H0.
- rewrite unopEq_sym.
destruct (unopEq u0 u) eqn:?;
......@@ -417,7 +417,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
* destruct m, m0; simpl in *; try congruence.
rewrite Pos.leb_nle in Heqb0, Heqb1.
rewrite <- Pos.lt_nle in Heqb0, Heqb1.
assert (f < f)%positive by (eapply Pos.lt_trans; eauto).
assert (w < w)%positive by (eapply Pos.lt_trans; eauto).
pose proof (Pos.lt_irrefl _ H). inversion H0.
Qed.
......@@ -610,30 +610,30 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
- erewrite morePrecise_trans; eauto;
type_conv; subst;
destruct m, m0, m1; try congruence.
destruct (f <=? f0)%positive eqn:?; try congruence.
destruct (f0 <=? f1)%positive eqn:?; try congruence.
assert (f <=? f1 = true)%positive.
destruct (w <=? w0)%positive eqn:?; try congruence.
destruct (w0 <=? w1)%positive eqn:?; try congruence.
assert (w <=? w1 = true)%positive.
{ rewrite Pos.leb_le; eapply Pos.le_trans;
rewrite <- Pos.leb_le; eauto. }
rewrite H; auto.
- type_conv; subst; destruct m, m0, m1; try congruence.
destruct (f <=? f0)%positive eqn:?; try congruence.
destruct (f0 <=? f1)%positive eqn:?; try congruence.
assert (f <=? f1 = true)%positive.
destruct (w <=? w0)%positive eqn:?; try congruence.
destruct (w0 <=? w1)%positive eqn:?; try congruence.
assert (w <=? w1 = true)%positive.
{ rewrite Pos.leb_le; eapply Pos.le_trans;
rewrite <- Pos.leb_le; eauto. }
rewrite H; auto.
- type_conv; subst; destruct m, m0, m1; try congruence.
destruct (f <=? f0)%positive eqn:?; try congruence.
destruct (f0 <=? f1)%positive eqn:?; try congruence.
assert (f <=? f1 = true)%positive.
destruct (w <=? w0)%positive eqn:?; try congruence.
destruct (w0 <=? w1)%positive eqn:?; try congruence.
assert (w <=? w1 = true)%positive.
{ rewrite Pos.leb_le; eapply Pos.le_trans;
rewrite <- Pos.leb_le; eauto. }
rewrite H; auto.
- type_conv; subst; destruct m, m0, m1; try congruence.
destruct (f <=? f0)%positive eqn:?; try congruence.
destruct (f0 <=? f1)%positive eqn:?; try congruence.
assert (f <=? f1 = true)%positive.
destruct (w <=? w0)%positive eqn:?; try congruence.
destruct (w0 <=? w1)%positive eqn:?; try congruence.
assert (w <=? w1 = true)%positive.
{ rewrite Pos.leb_le; eapply Pos.le_trans;
rewrite <- Pos.leb_le; eauto. }
rewrite H; auto. }
......@@ -697,8 +697,8 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
destruct (morePrecise m0 m1) eqn:prec2;
destruct m, m0, m1; simpl in *; try congruence; try auto;
try rewrite prec1 in *; try rewrite prec2 in *; try congruence;
destruct (f <=? f0)%positive eqn:?; try congruence;
assert (f <=? f1 = true)%positive as tr
destruct (w <=? w0)%positive eqn:?; try congruence;
assert (w <=? w1 = true)%positive as tr
by (rewrite Pos.leb_le; eapply Pos.le_trans; rewrite <- Pos.leb_le; eauto);
rewrite tr; auto. }
Defined.
......@@ -987,13 +987,13 @@ Inductive eval_exp (E:env) (Gamma: nat -> option mType) :(exp R) -> R -> mType -
E x = Some v ->
eval_exp E Gamma (Var R x) v m
| Const_dist m n delta:
Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
eval_exp E Gamma (Const m n) (perturb n delta) m
Rle (Rabs delta) (Q2R (mTypeToQ m n)) ->
eval_exp E Gamma (Const m (Q2R n)) (perturb (Q2R n) delta) m
| Unop_neg m f1 v1:
eval_exp E Gamma f1 v1 m ->
eval_exp E Gamma (Unop Neg f1) (evalUnop Neg v1) m
| Unop_inv m f1 v1 delta:
Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
Rle (Rabs delta) (Q2R (mTypeToQ m (evalUnop Inv v1))) ->
eval_exp E Gamma f1 v1 m ->
(~ v1 = 0)%R ->
eval_exp E Gamma (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m
......
......@@ -7,24 +7,26 @@
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.
Require Import Flover.Infra.RealRationalProps Flover.Infra.PosSimps.
(**
Define machine precision as datatype. We treat Fixed-point types as floats,
like Flocq, where f:positive specifies the fraction size
**)
Define machine precision as datatype.
**)
Inductive mType: Type := M0 | M16 | M32 | M64 | F (f:positive). (*| M128 | M256*)
Inductive mType: Type := M0 | M16 | M32 | M64 | F (w:positive). (*| M128 | M256*)
(**
Injection of machine types into Q
To support fixed-point values, we add an additional paramer, v which is the
value represented, as the error depends on the fraction bits which in turn
depend on the value represented
**)
Definition mTypeToQ (e:mType) :Q :=
match e with
Definition mTypeToQ (m:mType) (v:Q):Q :=
match m with
| M0 => 0
| 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)
| F w => (Qpower (2#1) (Zneg (fractionBits w v)))
(*
(* the epsilons below match what is used internally in flover,
although these value do not match the IEEE standard *)
......@@ -35,18 +37,19 @@ Definition mTypeToQ (e:mType) :Q :=
Arguments mTypeToQ _/.
Lemma mTypeToQ_pos_Q:
forall e, 0 <= mTypeToQ e.
forall m v, 0 <= mTypeToQ m v.
Proof.
intro e.
case_eq e; intros;
unfold mTypeToQ; try (apply Qle_bool_iff; auto; fail).
apply Qpower_pos; lra.
intros *.
destruct m eqn:?; cbn; try lra.
pose proof (Qpower_pos (2#1) (Zneg (fractionBits w v))) as pos_pow.
cbn in *.
apply pos_pow; lra.
Qed.
Lemma mTypeToQ_pos_R :
forall e, (0 <= Q2R (mTypeToQ e))%R.
forall m v, (0 <= Q2R (mTypeToQ m v))%R.
Proof.
intro.
intros *.
rewrite <- Q2R0_is_0.
apply Qle_Rle.
apply mTypeToQ_pos_Q.
......@@ -58,7 +61,7 @@ Definition mTypeEq (m1:mType) (m2:mType) :=
| M16, M16 => true
| M32, M32 => true
| M64, M64 => true
| F f1, F f2 => (f1 =? f2)%positive
| F w1, F w2 => (w1 =? w2)%positive
(* | M128, M128 => true *)
(* | M256, M256 => true *)
| _, _ => false
......@@ -89,7 +92,7 @@ Proof.
- hnf; intros; subst. rewrite mTypeEq_refl in eq_case.
congruence.
- case_eq m1; intros; case_eq m2; intros; subst; simpl; try congruence.
assert (f <> f0) by (hnf; intros; subst; congruence).
assert (w <> w0) by (hnf; intros; subst; congruence).
rewrite Pos.eqb_neq; auto.
Qed.
......@@ -120,15 +123,15 @@ Definition isMorePrecise (m1:mType) (m2:mType) :=
| F f1, F f2 => (f1 <=? f2)%positive
| F f, _ => false
| _ , F f => false
| _, _ => Qle_bool (mTypeToQ m1) (mTypeToQ m2)
| _, _ => Qle_bool (mTypeToQ m1 0) (mTypeToQ m2 0)
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
|F w1, F w2 => (w1 <=? w2)%positive
| _ , F w => false
| F w, _ => false
|M16, M16 => true
|M32, M32 => true
|M32, M16 => true
......
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