MachineType.v 6.42 KB
Newer Older
1 2 3 4 5 6 7
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.
 **)
8
Inductive mType: Type := M0 | M32 | M64 | M128 | M256.
9

10 11 12 13 14 15 16 17
Definition inj_eps_Q (e:mType) : Q :=
  match e with
  | M0 => 0
  | M32 => (Qpower (2#1) (Zneg 24))
  | M64 => (Qpower (2#1) (Zneg 54))
  | M128 => (Qpower (2#1) (Zneg 113))
  | M256 => (Qpower (2#1) (Zneg 237))
  end.
18

19
Definition meps := inj_eps_Q.
20

21 22 23 24 25 26
Lemma inj_eps_pos :
  forall e, 0 <= inj_eps_Q e.
Proof.
  intro e.
  case_eq e; intro; simpl inj_eps_Q; apply Qle_bool_iff; auto.
Qed.
27

28 29 30 31 32 33 34 35 36 37
Lemma inj_eps_posR :
  forall e, (0 <= Q2R (meps e))%R.
Proof.
  intro.
  assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra).
  rewrite <- H.
  apply Qle_Rle.
  apply inj_eps_pos.
Qed.
  
38 39
(* Definition mTypeEqBool (m1:mType) (m2:mType) := *)
(*   Qeq_bool (meps m1) (meps m2). *)
40

41 42 43 44 45
Theorem eq_mType_dec: forall (m1 m2:mType), {m1 = m2} + {m1 <> m2}.
Proof.
  intros.
  case_eq m1; intros; case_eq m2; intros; auto; right; intro; inversion H1.
Qed.
46 47

Definition mTypeEqBool (m1:mType) (m2:mType) :=
48 49 50 51 52 53 54 55 56
  match m1, m2 with
  | M0, M0 => true
  | M32, M32 => true
  | M64, M64 => true
  | M128, M128 => true
  | M256, M256 => true
  | _, _ => false
  end.

57 58 59 60 61 62 63 64 65 66 67 68 69 70
Lemma mTypeEqBool_sym (m1:mType) (m2:mType):
  forall b, mTypeEqBool m1 m2 = b -> mTypeEqBool m2 m1 = b.
Proof.
  intros.
  destruct b, m1, m2; simpl; cbv; auto.
Qed.  

Lemma mTypeEqBool_refl (m:mType):
  mTypeEqBool m m = true.
Proof.
  intros. destruct m; cbv; auto.
Qed.


71 72 73 74 75 76 77 78 79 80
(* Definition mTypeEqComp (m1:mType) (m2:mType) := *)
(*   Qeq_bool (meps m1) (meps m2). *)

(* Lemma EquivBoolComp (m1:mType) (m2:mType): *)
(*   mTypeEqBool m1 m2 = true <-> mTypeEqComp m1 m2 = true. *)
(* Proof. *)
(*   split; intros. *)
(*   - case_eq m1; intros; case_eq m2; intros; auto; try rewrite H0 in H; rewrite H1 in H; cbv; auto. *)
(*   - case_eq m1; intros; case_eq m2; intros; auto; try rewrite H0 in H; rewrite H1 in H; unfold mTypeEqComp in H; cbv in H; inversion H. *)
(* Qed.     *)
81

82 83
Lemma EquivEqBoolEq (m1:mType) (m2:mType):
  mTypeEqBool m1 m2 = true <-> m1 = m2.
84
Proof.
85
  split; intros; case_eq m1; intros; case_eq m2; intros; auto; rewrite H0 in H; rewrite H1 in H; cbv in H; inversion H; auto.
86
Qed.
87

88

89 90
(*   Definition mTypeEq: relation mType := *)
(*   fun m1 m2 => Qeq (meps m1) (meps m2). *)
91

92 93 94 95 96 97 98 99 100 101 102 103 104 105 106

(* Instance mTypeEquivalence: Equivalence mTypeEq. *)
(* Proof. *)
(*   split; intros. *)
(*   - intro. apply Qeq_refl. *)
(*   - intros a b eq. apply Qeq_sym. auto. *)
(*   - intros a b c eq1 eq2. eapply Qeq_trans; eauto. *)
(* Qed. *)


(* Lemma mTypeEquivs (m1:mType) (m2:mType): *)
(*   mTypeEqBool m1 m2 = true <-> mTypeEq m1 m2. *)
(* Proof. *)
(*   split; unfold mTypeEqBool; unfold mTypeEq; apply Qeq_bool_iff. *)
(* Qed. *)
107 108 109 110 111 112 113 114 115

Definition isMorePrecise (m1:mType) (m2:mType) :=
  (* check if m1 is more precise than m2, i.e. if the epsilon of m1 is *)
  (*   smaller than the epsilon of m2 *)
  if (mTypeEqBool m2 M0) then
    true
  else if (mTypeEqBool m1 M0) then
    mTypeEqBool m2 M0
  else
116
    Qle_bool (meps m1) (meps m2).
117

118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
(**
  Check if m1 is a more precise floating point type, meaning that the corresponding machine epsilon is less.
  Special Case m0, which must be the bottom element.
**)
Definition isMorePrecise' (m1:mType) (m2:mType) :=
  match m2, m1 with
  |M0, _ => true
  |M32, M0 => false
  |M32, _ => true
  |M64, M0 | M64, M32 => false
  |M64, _ => true
  |M128, M128 => true
  |M128, M256 => true
  |M256, M256 => true
  |_, _ => false
  end.

Raphaël Monat's avatar
Raphaël Monat committed
135 136 137
(* Lemma ismoreprec_rw m1 m2: *)
(*   forall b, isMorePrecise m1 m2  = b <-> isMorePrecise' m1 m2 = b. *)
(* Admitted. *)
138

139 140 141 142 143 144 145
Lemma isMorePrecise_refl (m1:mType) :
  isMorePrecise m1 m1 = true.
Proof.
  unfold isMorePrecise; simpl.
  case_eq (mTypeEqBool m1 M0); intro hyp; [ auto |  apply Qle_bool_iff; apply Qle_refl ].
Qed.

146 147
(* Definition isMorePrecise_rel (m1:mType) (m2:mType) := *)
(*   Qle (meps m1) (meps m2). *)
148 149 150 151 152 153 154 155 156 157 158


Definition isJoinOf (m:mType) (m1:mType) (m2:mType) :=
  (* is m the join of m1 and m2 ?*)
  if (isMorePrecise m1 m2) then
    mTypeEqBool m m1
  else
    mTypeEqBool m m2.


Definition computeJoin (m1:mType) (m2:mType) :=
159
  if (isMorePrecise m1 m2) then m1 else m2.
160

161 162 163 164 165 166 167 168 169 170 171 172
Lemma ifisMorePreciseM0 (m:mType) :
  isMorePrecise M0 m = true -> m = M0.
Proof.
  intro.
  unfold isMorePrecise in H.
  case_eq (mTypeEqBool m M0); intros; rewrite H0 in H; auto.
  - apply EquivEqBoolEq in H0; auto.
  - assert (mTypeEqBool M0 M0 = true) by (apply EquivEqBoolEq; auto).
    rewrite H1 in H.
    inversion H.
Qed.

173
Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) :
174
  m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0.
175 176 177
Proof.
  intros H0 H.
  unfold isJoinOf in H.
178 179
  case_eq (isMorePrecise m1 m2); intro Hyp; rewrite Hyp in H; simpl in H; rewrite H0 in H; subst.
  - case_eq m1; intros; auto; unfold isMorePrecise in Hyp; rewrite H0 in H; compute in H; inversion H.
180
  - unfold isMorePrecise in Hyp.
181 182
    apply EquivEqBoolEq in H; symmetry in H; apply EquivEqBoolEq in H.
    rewrite H in Hyp; inversion Hyp.
183 184 185 186
Qed.


Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) :
187
  m = M0 -> isJoinOf m m1 m2 = true -> m2 = M0.
188 189 190
Proof.
  intros H0 H.
  unfold isJoinOf in H.
191 192 193 194 195 196 197 198 199
  case_eq (isMorePrecise m1 m2); intro Hyp; rewrite Hyp in H; simpl in H; rewrite H0 in H; subst.
  - apply EquivEqBoolEq in H. rewrite <- H in Hyp; subst.
    unfold isMorePrecise in Hyp.
    case_eq (mTypeEqBool m2 M0); intros; auto; rewrite H in Hyp.
    apply EquivEqBoolEq in H; auto.
    case_eq (mTypeEqBool M0 M0); intros; auto; rewrite H0 in Hyp.
    inversion Hyp.
    unfold mTypeEqBool in H0; inversion H0.
  - apply EquivEqBoolEq in H; auto.
200
Qed.
201

202 203 204 205 206 207 208 209 210
Lemma ifM0isJoin (m1:mType) (m2:mType):
  isJoinOf M0 m1 m2 = true -> m1 = M0 /\ m2 = M0.
Proof.
  assert (M0 = M0) by auto.
  intros; split.
  - apply (ifM0isJoin_l M0 m1 m2); auto.
  - apply (ifM0isJoin_r M0 m1 m2); auto.  
Qed.

211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230
Lemma computeJoinIsJoin (m1:mType) (m2:mType) :
  isJoinOf (computeJoin m1 m2) m1 m2 = true.
Proof.
  remember (computeJoin m1 m2) as m.
  unfold isJoinOf.
  unfold computeJoin in Heqm.
  case_eq (isMorePrecise m1 m2); intros; auto;
  rewrite H in Heqm;
  rewrite Heqm;
  apply EquivEqBoolEq; auto.
Qed.

Lemma isJoinComputeJoin (M:mType) (m1:mType) (m2:mType) :
  isJoinOf M m1 m2 = true ->
  M = computeJoin m1 m2.
Proof.
  intros.
  unfold computeJoin.
  unfold isJoinOf in H.
  case_eq (isMorePrecise m1 m2); intros; auto; rewrite H0 in H; apply EquivEqBoolEq; auto.
='s avatar
= committed
231
Qed.