MachineType.v 9.31 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 57 58 59 60 61 62 63 64 65 66
  match m1, m2 with
  | M0, M0 => true
  | M32, M32 => true
  | M64, M64 => true
  | M128, M128 => true
  | M256, M256 => true
  | _, _ => false
  end.

(* 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.     *)
67

68 69
Lemma EquivEqBoolEq (m1:mType) (m2:mType):
  mTypeEqBool m1 m2 = true <-> m1 = m2.
70
Proof.
71
  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.
72
Qed.
73

74 75
(*   Definition mTypeEq: relation mType := *)
(*   fun m1 m2 => Qeq (meps m1) (meps m2). *)
76

77 78 79 80 81 82 83 84 85 86 87 88 89 90 91

(* 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. *)
92 93 94 95 96 97 98 99 100

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
101
    Qle_bool (meps m1) (meps m2).
102

103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
(**
  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.

Lemma ismoreprec_rw m1 m2:
  forall b, isMorePrecise m1 m2  = b <-> isMorePrecise' m1 m2 = b.
Admitted.

124 125 126 127 128 129 130
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.

131 132
(* Definition isMorePrecise_rel (m1:mType) (m2:mType) := *)
(*   Qle (meps m1) (meps m2). *)
133 134 135 136 137 138 139 140 141 142 143


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) :=
144
  if (isMorePrecise m1 m2) then m1 else m2.
145

146
    
147

148 149 150 151
(* Lemma eq_compat_join (m:mType) (m2:mType) (m1:mType) (m0:mType) : *)
(*   mTypeEq m m2 -> *)
(*   isJoinOf m m1 m0 = true -> *)
(*   isJoinOf m2 m1 m0 = true. *)
152
(* Proof. *)
153 154 155 156 157 158
(*   intros. *)
(*   unfold isJoinOf in *. *)
(*   case_eq (isMorePrecise m1 m0); intros; rewrite H1 in H0; auto; *)
(*     apply mTypeEquivs in H0; apply mTypeEquivs; *)
(*     [ apply (Equivalence_Transitive m2 m m1) | apply (Equivalence_Transitive m2 m m0) ]; *)
(*     auto; apply (Equivalence_Symmetric m m2); auto. *)
159 160
(* Qed. *)

161 162
(* Lemma M0_is_bot (m:mType): *)
(*   isMorePrecise m M0 = true. *)
163
(* Proof. *)
164 165 166
(*   unfold isMorePrecise. *)
(*   destruct m. *)
(*   simpl; auto. *)
167 168
(* Qed. *)

169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
(* (* Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) : *) *)
(* (*   (meps m) == 0 -> isJoinOf m m1 m2 = true -> mTypeEqBool M0 m1 = true.  *) *)
(* (* Proof. *) *)
(* (*   intros H0 H. *) *)
(* (*   unfold isJoinOf in H. *) *)
(* (*   case_eq (isMorePrecise m1 m2); intro Hyp; rewrite Hyp in H; simpl in H.  *) *)
(* (*   - auto. *) *)
(* (*     unfold mTypeEqBool. *) *)
(* (*     simpl (meps M0). *) *)
(* (*     unfold mTypeEqBool in H. *) *)
(* (*     rewrite H0 in H. *) *)
(* (*     auto. *) *)
(* (*   - unfold isMorePrecise in Hyp. *) *)
(* (*     unfold mTypeEqBool in *. *) *)
(* (*     apply Qeq_bool_iff in H. *) *)
(* (*     symmetry in H. *) *)
(* (*     apply Qeq_eq_bool in H. *) *)
(* (*     rewrite H0 in H. *) *)
(* (*     simpl (meps M0) in Hyp. *) *)
(* (*     rewrite H in Hyp. *) *)
(* (*     apply diff_true_false in Hyp. *) *)
(* (*     inversion Hyp. *) *)
(* (* Qed. *) *)


(* (* Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) : *) *)
(* (*   (meps m) == 0 -> isJoinOf m m1 m2 = true -> mTypeEqBool M0 m2 = true. *) *)
(* (* Proof. *) *)
(* (*   intros H0 H. *) *)
(* (*   unfold isJoinOf in H. *) *)
(* (*   case_eq (isMorePrecise m1 m2); intro Hyp; rewrite Hyp in H; simpl in H.  *) *)
(* (*   - unfold isMorePrecise in Hyp. *) *)
(* (*     case_eq (mTypeEqBool m2 M0); intro H2; rewrite H2 in Hyp.  *) *)
(* (*     + unfold mTypeEqBool in *. *) *)
(* (*       rewrite Qeq_bool_iff in *. *) *)
(* (*       symmetry; auto. *) *)
(* (*     + unfold mTypeEqBool in H; apply Qeq_bool_iff in H; symmetry in H; apply Qeq_eq_bool in H. *) *)
(* (*       unfold mTypeEqBool in Hyp. *) *)
(* (*       assert (Qeq_bool (meps m1) (meps M0) = true). *) *)
(* (*       apply Qeq_bool_iff. *) *)
(* (*       apply Qeq_bool_iff in H. *) *)
(* (*       rewrite H0 in H. *) *)
(* (*       rewrite H.  *) *)
(* (*       simpl meps. *) *)
(* (*       lra. *) *)
(* (*       rewrite H1 in Hyp; apply diff_false_true in Hyp; inversion Hyp. *) *)
(* (*   - unfold mTypeEqBool in *. simpl in *. rewrite H0 in H. auto. *) *)
(* (* Qed. *) *)

218

219 220 221 222 223 224 225 226 227 228 229 230
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.

231
Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) :
232
  m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0.
233 234 235
Proof.
  intros H0 H.
  unfold isJoinOf in H.
236 237
  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.
238
  - unfold isMorePrecise in Hyp.
239 240
    apply EquivEqBoolEq in H; symmetry in H; apply EquivEqBoolEq in H.
    rewrite H in Hyp; inversion Hyp.
241 242 243 244
Qed.


Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) :
245
  m = M0 -> isJoinOf m m1 m2 = true -> m2 = M0.
246 247 248
Proof.
  intros H0 H.
  unfold isJoinOf in H.
249 250 251 252 253 254 255 256 257
  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.
258
Qed.
259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306

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.
Qed. 
  (* Lemma joinIsMP (m1:mType) (m2:mType) : *)
(*   isMorePrecise (computeJoin m1 m2) m1 = true. *)
(* Proof. *)
(*   unfold computeJoin. *)
(*   case_eq (isMorePrecise m1 m2); intros. *)
(*   apply isMorePrecise_refl. *)

(*   unfold isMorePrecise in *. *)
(*   case_eq (mTypeEqBool m2 M0); intros; rewrite H0 in H; auto. *)
(*   inversion H. *)
(*   case_eq (mTypeEqBool m1 M0); intros; rewrite H1 in H; auto. *)
(*   rewrite Qle_bool_iff. *)
(*   apply Qnot_lt_le. *)

(*   intro. *)

(*   apply not_true_iff_false in H. *)

  
(*   Lemma Qnot_lt_le : forall x y, ~ x<y -> y<=x. *)

(* Lemma Qnot_le_lt : forall x y, ~ x<=y -> y<x. *)

(* Lemma Qlt_not_le : forall x y, x<y -> ~ y<=x. *)

(* Lemma Qle_not_lt : forall x y, x<=y -> ~ y<x. *)