MachineType.v 6.99 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 27 28 29
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.
  
(* 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

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.

100 101
(* Definition isMorePrecise_rel (m1:mType) (m2:mType) := *)
(*   Qle (meps m1) (meps m2). *)
102 103 104 105 106 107 108 109 110 111 112


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) :=
113
  if (isMorePrecise m1 m2) then m1 else m2.
114 115 116



117 118 119 120
(* 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. *)
121
(* Proof. *)
122 123 124 125 126 127
(*   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. *)
128 129
(* Qed. *)

130 131
(* Lemma M0_is_bot (m:mType): *)
(*   isMorePrecise m M0 = true. *)
132
(* Proof. *)
133 134 135
(*   unfold isMorePrecise. *)
(*   destruct m. *)
(*   simpl; auto. *)
136 137
(* Qed. *)

138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 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
(* (* 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. *) *)

187 188

Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) :
189
  m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0. 
190 191 192
Proof.
  intros H0 H.
  unfold isJoinOf in H.
193 194
  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.
195
  - unfold isMorePrecise in Hyp.
196 197
    apply EquivEqBoolEq in H; symmetry in H; apply EquivEqBoolEq in H.
    rewrite H in Hyp; inversion Hyp.
198 199 200 201
Qed.


Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) :
202
  m = M0 -> isJoinOf m m1 m2 = true -> m2 = M0.
203 204 205
Proof.
  intros H0 H.
  unfold isJoinOf in H.
206 207 208 209 210 211 212 213 214
  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.
215
Qed.