Commit a4496a7c authored by Raphaël Monat's avatar Raphaël Monat

Adding support of mixed-precision eval_exp and Downcasting operator.

parent bc72a362
......@@ -2,6 +2,7 @@
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith.
Require Import Daisy.Expressions.
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
(**
......@@ -10,8 +11,23 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
Final return statement
**)
Inductive cmd (V:Type) :Type :=
Let: nat -> exp V -> cmd V -> cmd V
Let: mType -> nat -> exp V -> cmd V -> cmd V
| Ret: exp V -> cmd V.
Fixpoint toRCmd (f:cmd Q) :=
match f with
|Let m x e g => Let m x (toRExp e) (toRCmd g)
|Ret e => Ret (toRExp e)
end.
Fixpoint toREvalCmd (f:cmd R) :=
match f with
|Let m x e g => Let m x (toREval e) (toREvalCmd g)
|Ret e => Ret (toREval e)
end.
(*| Nop: cmd V. *)
(*
......@@ -29,23 +45,24 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
(**
Analogously define Big Step semantics for the Daisy language
**)
Inductive bstep : cmd R -> env -> R -> R -> Prop :=
let_b x e s E v eps res:
eval_exp eps E e v ->
bstep s (updEnv x v E) eps res ->
bstep (Let x e s) E eps res
|ret_b e E v eps:
eval_exp eps E e v ->
bstep (Ret e) E eps v.
Inductive bstep : cmd R -> env -> R * mType -> Prop :=
let_b m m1 x e s E v res:
isMorePrecise m1 m = true ->
eval_exp E e (v,m) ->
bstep s (updEnv x m v E) (res,m) ->
bstep (Let m1 x e s) E (res,m)
|ret_b e E v:
eval_exp E e v ->
bstep (Ret e) E v.
Fixpoint freeVars (f:cmd Q) :NatSet.t :=
match f with
| Let x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g))
| Let _ x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g))
| Ret e => Expressions.freeVars e
end.
Fixpoint definedVars (f:cmd Q) :NatSet.t :=
match f with
| Let x _ g => NatSet.add x (definedVars g)
| Let _ x _ g => NatSet.add x (definedVars g)
| Ret _ => NatSet.empty
end.
\ No newline at end of file
......@@ -15,21 +15,21 @@ expression may yield different values for different machine epsilons
Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
|approxRefl A:
approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 A v1 v2 x fVars dVars:
|approxUpdFree E1 E2 A v1 v2 x fVars dVars m:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= v1 * Q2R machineEpsilon)%R ->
(Rabs (v1 - v2) <= v1 * Q2R (meps m))%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
|approxUpdBound E1 E2 A v1 v2 x fVars dVars:
|approxUpdBound E1 E2 A v1 v2 x fVars dVars m:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q m x))))%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
Inductive approxParams :env -> R -> env -> Prop :=
|approxParamRefl eps:
approxParams emptyEnv eps emptyEnv
|approxParamUpd E1 E2 eps x v1 v2 :
approxParams E1 eps E2 ->
(Rabs (v1 - v2) <= eps)%R ->
approxParams (updEnv x v1 E1) eps (updEnv x v2 E2).
Inductive approxParams :env -> env -> Prop :=
|approxParamRefl:
approxParams emptyEnv emptyEnv
|approxParamUpd E1 E2 m x v1 v2 :
approxParams E1 E2 ->
(Rabs (v1 - v2) <= Q2R (meps m))%R ->
approxParams (updEnv x v1 E1) (updEnv x v2 E2).
......@@ -3,7 +3,8 @@ Formalization of the base expression language for the daisy framework
Required in all files, since we will always reason about expressions.
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith.
Require Import Daisy.Infra.RealRationalProps.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
(**
Expressions will use binary operators.
......@@ -53,15 +54,18 @@ Definition evalUnop (o:unop) (v:R):=
|Inv => (/ v)%R
end .
(**
Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later.
**)
Inductive exp (V:Type): Type :=
Var: nat -> exp V
Var: mType -> nat -> exp V
| Const: V -> exp V
| Unop: unop -> exp V -> exp V
| Binop: binop -> exp V -> exp V -> exp V.
| Binop: binop -> exp V -> exp V -> exp V
| Downcast: mType -> exp V -> exp V.
(**
Boolean equality function on expressions.
......@@ -69,14 +73,14 @@ Inductive exp (V:Type): Type :=
**)
Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
match e1 with
|Var _ v1 =>
|Var _ m1 v1 =>
match e2 with
|Var _ v2 => v1 =? v2
|Var _ m2 v2 => andb (mTypeEqBool m1 m2) (v1 =? v2)
| _=> false
end
|Const n1 =>
match e2 with
|Const n2 => Qeq_bool n1 n2
|Const n2 => (Qeq_bool n1 n2)
| _=> false
end
|Unop o1 e11 =>
......@@ -89,8 +93,41 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
|Binop o2 e21 e22 => andb (binopEqBool o1 o2) (andb (expEqBool e11 e21) (expEqBool e12 e22))
|_ => false
end
|Downcast m1 f1 =>
match e2 with
|Downcast m2 f2 => andb (mTypeEqBool m1 m2) (expEqBool f1 f2)
|_ => false
end
end.
Fixpoint toRExp (e:exp Q) :=
match e with
|Var _ m v => Var R m v
|Const n => Const (Q2R n)
|Unop o e1 => Unop o (toRExp e1)
|Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2)
|Downcast m e1 => Downcast m (toRExp e1)
end.
Fixpoint toREval (e:exp R) :=
match e with
| Var _ _ v => Var R M0 v
| Const n => Const n
| Unop o e1 => Unop o (toREval e1)
| Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
| Downcast _ e1 => (toREval e1)
end.
Definition toREvalEnv (E:env) : env :=
fun (n:nat) =>
let s := (E n) in
match s with
| None => None
| Some (r, _) => Some (r, M0)
end.
(**
Define a perturbation function to ease writing of basic definitions
**)
......@@ -106,31 +143,41 @@ It is important that variables are not perturbed when loading from an environmen
This is the case, since loading a float value should not increase an additional error.
Unary negation is special! We do not have a new error here since IEE 754 gives us a sign bit
**)
Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
| Var_load x v:
E x = Some v ->
eval_exp eps E (Var R x) v
| Const_dist n delta:
Rle (Rabs delta) eps ->
eval_exp eps E (Const n) (perturb n delta)
| Unop_neg f1 v1:
eval_exp eps E f1 v1 ->
eval_exp eps E (Unop Neg f1) (evalUnop Neg v1)
| Unop_inv f1 v1 delta:
Rle (Rabs delta) eps ->
eval_exp eps E f1 v1 ->
eval_exp eps E (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
| Binop_dist op f1 f2 v1 v2 delta:
Rle (Rabs delta) eps ->
eval_exp eps E f1 v1 ->
eval_exp eps E f2 v2 ->
eval_exp eps E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
Inductive eval_exp (E:env) :(exp R) -> R -> mType -> Prop :=
| Var_load m m1 x v:
isMorePrecise m m1 = true ->
(**mTypeEqBool m m1 = true ->*)
E x = Some (v, m1) ->
eval_exp E (Var R m1 x) v m
| Const_dist m n delta:
Rle (Rabs delta) (Q2R (meps m)) ->
eval_exp E (Const n) (perturb n delta) m
| Unop_neg m f1 v1:
eval_exp E f1 v1 m ->
eval_exp E (Unop Neg f1) (evalUnop Neg v1) m
| Unop_inv m f1 v1 delta:
Rle (Rabs delta) (Q2R (meps m)) ->
eval_exp E f1 v1 m ->
eval_exp E (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m
| Binop_dist m m1 m2 op f1 f2 v1 v2 delta:
isJoinOf m m1 m2 = true ->
Rle (Rabs delta) (Q2R (meps m)) ->
eval_exp E f1 v1 m1 ->
eval_exp E f2 v2 m2 ->
eval_exp E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) m
| Downcast_dist m m1 f1 v1 delta:
(* Qle_bool (meps m1) (meps m) = true ->*)
isMorePrecise m1 m = true ->
Rle (Rabs delta) (Q2R (meps m)) ->
eval_exp E f1 v1 m1 ->
eval_exp E (Downcast m f1) (perturb v1 delta) m.
Fixpoint freeVars (V:Type) (e:exp V) :NatSet.t :=
match e with
| Var _ x => NatSet.singleton x
| Var _ _ x => NatSet.singleton x
| Unop u e1 => freeVars e1
| Binop b e1 e2 => NatSet.union (freeVars e1) (freeVars e2)
| Downcast _ e1 => freeVars e1
| _ => NatSet.empty
end.
......@@ -146,28 +193,126 @@ Proof.
lra.
Qed.
(* Lemma compat_eexp (E:env) (f f':exp R) (v:R): *)
(* forall m1, *)
(* mTypeEq m1 M0 -> *)
(* f' = toREval f -> *)
(* eval_exp E f' v m1 <-> *)
(* eval_exp E f' v M0. *)
(* Proof. *)
(* intros m1 meq. *)
(* induction f'; intros; split; intros; inversion H0; subst; auto. *)
(* - constructor; auto. *)
(* unfold isMorePrecise in *. *)
(* unfold mTypeEqBool in *. *)
(* case_eq (Qeq_bool (meps m) (meps M0)); intros; auto. *)
(* rewrite H1 in H3. *)
(* apply mTypeEquivs in meq; unfold mTypeEqBool in meq; rewrite meq in H3. *)
(* inversion H3. *)
(* - admit. *)
(* - constructor; auto. *)
(* unfold mTypeEq in meq. *)
(* apply Qeq_eqR in meq. *)
(* rewrite <- meq; auto. *)
(* - admit. *)
(* - constructor; auto. *)
(* - constructor. *)
(* unfold mTypeEq in meq. *)
(* apply Qeq_eqR in meq. *)
(* rewrite meq in H. *)
(* auto. *)
(* - constructor. *)
(* apply (IHeval_exp meq); auto. *)
(* - constructor. *)
(* unfold mTypeEq in meq; apply Qeq_eqR in meq; rewrite <- meq; auto. *)
(* apply IHeval_exp; auto. *)
(* - assert (isJoinOf M0 m1 m2 = true) as join012. *)
(* apply (eq_compat_join m M0 m1 m2); auto. *)
(* apply (Binop_dist M0 op delta join012); auto. *)
(* unfold mTypeEq in meq; apply Qeq_eqR in meq; rewrite <- meq; auto. *)
(* - apply (Downcast_dist m delta). *)
(* Qed. *)
(* Lemma bla (m:mType) E f v: *)
(* (meps m) == 0 -> *)
(* eval_exp E (toREval f) v m <-> eval_exp E (toREval f) v M0. *)
(* Proof. *)
(* intros. *)
(* assert (mTypeEq m M0). *)
(* unfold mTypeEq. *)
(* rewrite H. *)
(* simpl (meps M0). *)
(* lra. *)
(* rewrite H0. *)
(* split; trivial. *)
(* Qed. *)
Lemma general_meps_0_deterministic (f:exp R) (E:env):
forall v1 v2 m1 m2,
(meps m1) == 0 ->
(meps m2) == 0 ->
eval_exp E (toREval f) v1 m1 ->
eval_exp E (toREval f) v2 m2 ->
v1 = v2.
Proof.
induction f; intros v1 v2 m1 m2 meps1 meps2 eval_v1 eval_v2.
- inversion eval_v1; inversion eval_v2; subst; auto;
try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
rewrite H4 in H10; inversion H10; subst; auto.
- inversion eval_v1; inversion eval_v2; subst; auto;
try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
rewrite (Qeq_eqR (meps m1) 0 meps1) in H0.
rewrite (Qeq_eqR (meps m2) 0 meps2) in H4.
rewrite Q2R0_is_0 in *.
rewrite delta_0_deterministic; auto. symmetry. rewrite delta_0_deterministic; auto.
- inversion eval_v1; inversion eval_v2; subst; auto;
try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
+ apply Ropp_eq_compat. apply (IHf v0 v3 m1 m2); auto.
+ inversion H4.
+ inversion H5.
+ rewrite (Qeq_eqR (meps m1) 0 meps1) in H1.
rewrite (Qeq_eqR (meps m2) 0 meps2) in H7.
rewrite Q2R0_is_0 in *.
rewrite delta_0_deterministic; auto. symmetry. rewrite delta_0_deterministic; auto.
rewrite (IHf v0 v3 m1 m2); auto.
- inversion eval_v1; inversion eval_v2; subst; auto;
try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
rewrite (Qeq_eqR (meps m1) 0 meps1) in H3.
rewrite (Qeq_eqR (meps m2) 0 meps2) in H12.
rewrite Q2R0_is_0 in *.
rewrite delta_0_deterministic; auto. symmetry. rewrite delta_0_deterministic; auto.
rewrite (IHf1 v0 v4 m0 m5); auto.
rewrite (IHf2 v5 v3 m6 m3); auto.
apply (ifM0isJoin_r m2 m5 m6); auto.
apply (ifM0isJoin_r m1 m0 m3); auto.
apply (ifM0isJoin_l m1 m0 m3); auto.
apply (ifM0isJoin_l m2 m5 m6); auto.
- simpl toREval in eval_v1.
simpl toREval in eval_v2.
apply (IHf v1 v2 m1 m2); auto.
Qed.
(**
Evaluation with 0 as machine epsilon is deterministic
**)
Lemma meps_0_deterministic (f:exp R) (E:env):
forall v1 v2,
eval_exp 0 E f v1 ->
eval_exp 0 E f v2 ->
eval_exp E (toREval f) v1 M0 ->
eval_exp E (toREval f) v2 M0 ->
v1 = v2.
Proof.
induction f; intros v1 v2 eval_v1 eval_v2;
inversion eval_v1; inversion eval_v2;
repeat try rewrite delta_0_deterministic; subst; auto.
- rewrite H3 in H0; inversion H0;
subst; auto.
- rewrite (IHf v0 v3); auto.
- inversion H3.
- inversion H4.
- rewrite (IHf v0 v3); auto.
- rewrite (IHf1 v0 v4); auto.
rewrite (IHf2 v3 v5); auto.
intros v1 v2 ev1 ev2.
assert ((meps M0) == 0) by (simpl; lra).
apply (general_meps_0_deterministic f H H ev1 ev2).
Qed.
(**
Helping lemma. Needed in soundness proof.
For each evaluation of using an arbitrary epsilon, we can replace it by
......@@ -175,47 +320,54 @@ evaluating the subexpressions and then binding the result values to different
variables in the Eironment.
This relies on the property that variables are not perturbed as opposed to parameters
**)
Lemma binary_unfolding b f1 f2 eps E vF:
eval_exp eps E (Binop b f1 f2) vF ->
exists vF1 vF2,
eval_exp eps E f1 vF1 /\
eval_exp eps E f2 vF2 /\
eval_exp eps (updEnv 2 vF2 (updEnv 1 vF1 emptyEnv))
(Binop b (Var R 1) (Var R 2)) vF.
Lemma binary_unfolding b f1 f2 m E vF:
eval_exp E (Binop b f1 f2) vF m ->
exists vF1 vF2 m1 m2,
eval_exp E f1 vF1 m1 /\
eval_exp E f2 vF2 m2 /\
eval_exp (updEnv 2 m2 vF2 (updEnv 1 m1 vF1 emptyEnv))
(Binop b (Var R m1 1) (Var R m2 2)) vF m.
Proof.
intros eval_float.
inversion eval_float; subst.
exists v1 ; exists v2; repeat split; try auto.
constructor; try auto.
- constructor.
unfold updEnv; cbv; auto.
- constructor.
unfold updEnv; cbv; auto.
exists v1 ; exists v2; exists m1; exists m2; repeat split; try auto.
eapply Binop_dist; eauto.
pose proof (isMorePrecise_refl m1).
eapply Var_load; eauto.
pose proof (isMorePrecise_refl m2).
(* unfold mTypeEqBool; apply Qeq_bool_iff; apply Qeq_refl. *)
eapply Var_load; eauto.
(* unfold mTypeEqBool; apply Qeq_bool_iff; apply Qeq_refl. *)
Qed.
(**
Analogous lemma for unary expressions.
**)
Lemma unary_unfolding (e:exp R) (eps:R) (E:env) (v:R):
(eval_exp eps E (Unop Inv e) v <->
exists v1,
eval_exp eps E e v1 /\
eval_exp eps (updEnv 1 v1 E) (Unop Inv (Var R 1)) v).
(* (** *)
(* Analogous lemma for unary expressions. *)
(* **) *)
Lemma unary_unfolding (e:exp R) (m:mType) (E:env) (v:R):
(eval_exp E (Unop Inv e) v m ->
exists v1 m1,
eval_exp E e v1 m1 /\
eval_exp (updEnv 1 m1 v1 E) (Unop Inv (Var R m1 1)) v m).
Proof.
split.
- intros eval_un.
intros eval_un.
inversion eval_un; subst.
exists v1.
exists v1; exists m.
repeat split; try auto.
constructor; try auto.
constructor; auto.
- intros exists_val.
destruct exists_val as [v1 [eval_f1 eval_e_E]].
inversion eval_e_E; subst.
inversion H1; subst.
unfold updEnv in *; simpl in *.
constructor; auto.
inversion H2; subst; auto.
econstructor; try auto.
pose proof (isMorePrecise_refl m).
econstructor; eauto.
(* - intros exists_val. *)
(* destruct exists_val as [v1 [m1 [eval_f1 eval_e_E]]]. *)
(* inversion eval_e_E; subst. *)
(* inversion H1; subst. *)
(* econstructor; eauto. *)
(* unfold updEnv in H6. *)
(* simpl in H6. *)
(* inversion H6. *)
(* rewrite <- H2. *)
(* rewrite <- H1. *)
(* auto. *)
Qed.
......@@ -225,20 +377,21 @@ Qed.
Inductive bexp (V:Type) : Type :=
leq: exp V -> exp V -> bexp V
| less: exp V -> exp V -> bexp V.
(**
Define evaluation of booleans for reals
**)
Inductive bval (eps:R) (E:env): (bexp R) -> Prop -> Prop :=
leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):
eval_exp eps E f1 v1 ->
eval_exp eps E f2 v2 ->
bval eps E (leq f1 f2) (Rle v1 v2)
|less_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):
eval_exp eps E f1 v1 ->
eval_exp eps E f2 v2 ->
bval eps E (less f1 f2) (Rlt v1 v2).
(**
Simplify arithmetic later by making > >= only abbreviations
**)
Definition gr := fun (V:Type) (f1: exp V) (f2: exp V) => less f2 f1.
Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1.
\ No newline at end of file
(* Inductive bval (E:env): (bexp R) -> Prop -> Prop := *)
(* leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): *)
(* eval_exp E f1 v1 -> *)
(* eval_exp E f2 v2 -> *)
(* bval E (leq f1 f2) (Rle v1 v2) *)
(* |less_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): *)
(* eval_exp E f1 v1 -> *)
(* eval_exp E f2 v2 -> *)
(* bval E (less f1 f2) (Rlt v1 v2). *)
(* (** *)
(* Simplify arithmetic later by making > >= only abbreviations *)
(* **) *)
(* Definition gr := fun (V:Type) (f1: exp V) (f2: exp V) => less f2 f1. *)
(* Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. *)
\ No newline at end of file
......@@ -2,6 +2,7 @@
This file contains some type abbreviations, to ease writing.
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.MachineType.
Global Set Implicit Arguments.
(**
......@@ -40,21 +41,21 @@ Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
(**
Later we will argue about program preconditions.
Define a precondition to be a function mapping numbers (resp. variables) to intervals.
Later we will argue about program preconditions.
Define a precondition to be a function mapping numbers (resp. variables) to intervals.
**)
Definition precond :Type := nat -> intv.
(**
Abbreviation for the type of a variable environment, which should be a partial function
**)
Definition env := nat -> option R.
Definition env := nat -> option (R * mType).
Definition emptyEnv:env := fun _ => None.
(**
Define environment update function as abbreviation, for variable environments
**)
Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
if y =? x
then Some v
Definition updEnv (x:nat) (mx:mType) (v: R) (E:env) (y:nat) :=
if (y =? x)
then Some (v, mx)
else E y.
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
(**
Define machine types, and some tool functions. Needed for the
mixed-precision part, to be able to define a rounding operator.
**)
Record mType : Type := mkmType {meps : Q; meps_geq_zero: 0 <= meps}.
Arguments meps _ /.
Lemma M0_is_geq_zero: 0 <= 0.
Proof. apply Qle_refl. Qed.
Lemma M32_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 24)).
Proof. apply Qle_bool_iff; auto. Qed.
Lemma M64_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 53)).
Proof. apply Qle_bool_iff; auto. Qed.
Lemma M128_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 113)).
Proof. apply Qle_bool_iff; auto. Qed.
Lemma M256_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 237)).
Proof. apply Qle_bool_iff; auto. Qed.
Definition M0 := mkmType 0 (M0_is_geq_zero).
Definition M32 := mkmType (Qpower (2#1) (Zneg 24)) (M32_is_geq_zero).
Definition M64 := mkmType (Qpower (2#1) (Zneg 53)) (M64_is_geq_zero).
Definition M128 := mkmType (Qpower (2#1) (Zneg 113)) (M128_is_geq_zero).
Definition M256 := mkmType (Qpower (2#1) (Zneg 237)) (M256_is_geq_zero).
Definition mTypeEqBool (m1:mType) (m2:mType) :=
Qeq_bool (meps m1) (meps m2).