MachineType.v 6.29 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 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 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
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.
 **)
Record mType : Type := mkmType {meps : Q; meps_geq_zero: 0 <= meps}.
Arguments meps _ /.

Lemma M0_is_geq_zero: 0 <= 0.
Proof. apply Qle_refl. Qed.

Lemma M32_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 24)).
Proof. apply Qle_bool_iff; auto. Qed.

Lemma M64_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 53)).
Proof. apply Qle_bool_iff; auto. Qed.

Lemma M128_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 113)).
Proof. apply Qle_bool_iff; auto. Qed.

Lemma M256_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 237)).
Proof. apply Qle_bool_iff; auto. Qed.

Definition M0 := mkmType 0 (M0_is_geq_zero).
Definition M32 := mkmType (Qpower (2#1) (Zneg 24)) (M32_is_geq_zero). 
Definition M64 := mkmType (Qpower (2#1) (Zneg 53)) (M64_is_geq_zero).
Definition M128 := mkmType (Qpower (2#1) (Zneg 113)) (M128_is_geq_zero).
Definition M256 := mkmType (Qpower (2#1) (Zneg 237)) (M256_is_geq_zero).

Definition mTypeEqBool (m1:mType) (m2:mType) :=
  Qeq_bool (meps m1) (meps m2).

Definition mTypeEq: relation mType :=
  fun m1 m2 => Qeq (meps m1) (meps m2).

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.

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

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.

Definition isMorePrecise_rel (m1:mType) (m2:mType) :=
  Qle (meps m1) (meps m2).


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



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.
Proof.
  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.
Qed.    

Lemma M0_is_bot (m:mType):
  isMorePrecise m M0 = true.
Proof.
  unfold isMorePrecise.
  destruct m.
  simpl; auto.
Qed.

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


Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) :
  (meps m) == 0 -> isJoinOf m m1 m2 = true -> (meps m1) == 0.
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.
    apply Qeq_bool_iff in H.
    rewrite <- H.
    lra.
  - 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 -> (meps m2) == 0.
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 *.
      simpl meps in H2 at 2.
      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 *. rewrite H0 in H. apply Qeq_bool_iff in H. symmetry; auto.
Qed.