MachineType.v 9.58 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 135 136 137 138
(**
  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.

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
(* 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. *)
167
(* Proof. *)
168 169 170 171 172 173
(*   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. *)
174 175
(* Qed. *)

176 177
(* Lemma M0_is_bot (m:mType): *)
(*   isMorePrecise m M0 = true. *)
178
(* Proof. *)
179 180 181
(*   unfold isMorePrecise. *)
(*   destruct m. *)
(*   simpl; auto. *)
182 183
(* Qed. *)

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 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232
(* (* 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. *) *)

233

234 235 236 237 238 239 240 241 242 243 244 245
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.

246
Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) :
247
  m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0.
248 249 250
Proof.
  intros H0 H.
  unfold isJoinOf in H.
251 252
  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.
253
  - unfold isMorePrecise in Hyp.
254 255
    apply EquivEqBoolEq in H; symmetry in H; apply EquivEqBoolEq in H.
    rewrite H in Hyp; inversion Hyp.
256 257 258 259
Qed.


Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) :
260
  m = M0 -> isJoinOf m m1 m2 = true -> m2 = M0.
261 262 263
Proof.
  intros H0 H.
  unfold isJoinOf in H.
264 265 266 267 268 269 270 271 272
  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.
273
Qed.
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 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321

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