MachineType.v 7.51 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
(* Definition mTypeEqBool (m1:mType) (m2:mType) := *)
(*   Qeq_bool (meps m1) (meps m2). *)
30

31 32 33 34 35
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.
36 37

Definition mTypeEqBool (m1:mType) (m2:mType) :=
38 39 40 41 42 43 44 45 46 47 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.

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

58 59
Lemma EquivEqBoolEq (m1:mType) (m2:mType):
  mTypeEqBool m1 m2 = true <-> m1 = m2.
60
Proof.
61
  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.
62
Qed.
63

64 65
(*   Definition mTypeEq: relation mType := *)
(*   fun m1 m2 => Qeq (meps m1) (meps m2). *)
66

67 68 69 70 71 72 73 74 75 76 77 78 79 80 81

(* 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. *)
82 83 84 85 86 87 88 89 90

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
91
    Qle_bool (meps m1) (meps m2).
92

93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
(**
  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.

114 115 116 117 118 119 120
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.

121 122
(* Definition isMorePrecise_rel (m1:mType) (m2:mType) := *)
(*   Qle (meps m1) (meps m2). *)
123 124 125 126 127 128 129 130 131 132 133


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) :=
134
  if (isMorePrecise m1 m2) then m1 else m2.
135 136 137



138 139 140 141
(* 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. *)
142
(* Proof. *)
143 144 145 146 147 148
(*   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. *)
149 150
(* Qed. *)

151 152
(* Lemma M0_is_bot (m:mType): *)
(*   isMorePrecise m M0 = true. *)
153
(* Proof. *)
154 155 156
(*   unfold isMorePrecise. *)
(*   destruct m. *)
(*   simpl; auto. *)
157 158
(* Qed. *)

159 160 161 162 163 164 165 166 167 168 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
(* (* 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. *) *)

208 209

Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) :
210
  m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0.
211 212 213
Proof.
  intros H0 H.
  unfold isJoinOf in H.
214 215
  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.
216
  - unfold isMorePrecise in Hyp.
217 218
    apply EquivEqBoolEq in H; symmetry in H; apply EquivEqBoolEq in H.
    rewrite H in Hyp; inversion Hyp.
219 220 221 222
Qed.


Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) :
223
  m = M0 -> isJoinOf m m1 m2 = true -> m2 = M0.
224 225 226
Proof.
  intros H0 H.
  unfold isJoinOf in H.
227 228 229 230 231 232 233 234 235
  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.
236
Qed.