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. **) Inductive mType: Type := M0 | M32 | M64 | M128 | M256. 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. Definition meps := inj_eps_Q. 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). *) 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. Definition mTypeEqBool (m1:mType) (m2:mType) := 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. *) Lemma EquivEqBoolEq (m1:mType) (m2:mType): mTypeEqBool m1 m2 = true <-> m1 = m2. Proof. 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. Qed. (* 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) : m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0. Proof. intros H0 H. unfold isJoinOf in H. 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. - unfold isMorePrecise in Hyp. apply EquivEqBoolEq in H; symmetry in H; apply EquivEqBoolEq in H. rewrite H in Hyp; inversion Hyp. Qed. Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) : m = M0 -> isJoinOf m m1 m2 = true -> m2 = M0. Proof. intros H0 H. unfold isJoinOf in H. 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. Qed.