(** Some simplification properties of rationals, not proven in the Standard Library **) Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs. Require Import Daisy.Infra.Abbrevs. Definition Qleb :=Qle_bool. Definition Qeqb := Qeq_bool. Definition machineEpsilon := (1#(2^53)). Definition maxAbs (iv:intv) := Qmax (Qabs (fst iv)) (Qabs (snd iv)). Lemma maxAbs_pointIntv a: maxAbs (a,a) == Qabs a. Proof. unfold maxAbs; simpl. apply Qabs_case; intros; eapply Q.max_id. Qed. Lemma Qsub_eq_Qopp_Qplus (a:Q) (b:Q) : (a - b = a + (- b))%Q. Proof. field_simplify; reflexivity. Qed. (* Based on stdlib proof of reals *) Lemma Qmult_le_compat_neg_l (r r1 r2:Q) : r <= 0 -> r1 <= r2 -> r * r2 <= r * r1. Proof. intros. rewrite <- (Qopp_involutive r). apply Qopp_le_compat in H. assert (-0 == 0) by field. rewrite H1 in H. assert (forall a b, - a*b == - (a * b)) by (intros; field). setoid_rewrite H2 at 1 2. apply Qopp_le_compat. setoid_rewrite Qmult_comm at 1 2. apply Qmult_le_compat_r; auto. Qed. Lemma le_neq_bool_to_lt_prop a b: (Qleb a 0 && negb (Qeq_bool a 0) || Qleb 0 b && negb (Qeq_bool b 0)) = true -> a < 0 \/ 0 < b. Proof. intros le_neq_bool. apply Is_true_eq_left in le_neq_bool. apply orb_prop_elim in le_neq_bool. destruct le_neq_bool as [lt_0 | lt_0]; apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0]; apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0; apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0; rewrite Qle_bool_iff in le_0; rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0]; [ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto. Qed.