RationalSimps.v 1.69 KB
 Heiko Becker committed Oct 06, 2016 1 2 3 ``````(** Some simplification properties of rationals, not proven in the Standard Library **) `````` Heiko Becker committed Aug 20, 2016 4 5 6 7 ``````Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs. Require Import Daisy.Infra.Abbrevs. Definition Qleb :=Qle_bool. `````` Heiko Becker committed Aug 21, 2016 8 ``````Definition Qeqb := Qeq_bool. `````` Heiko Becker committed Sep 05, 2016 9 10 11 `````` Definition machineEpsilon := (1#(2^53)). `````` Heiko Becker committed Oct 06, 2016 12 13 ``````Definition maxAbs (iv:intv) := Qmax (Qabs (fst iv)) (Qabs (snd iv)). `````` Heiko Becker committed Aug 20, 2016 14 `````` `````` Heiko Becker committed Oct 06, 2016 15 16 17 18 19 20 ``````Lemma maxAbs_pointIntv a: maxAbs (a,a) == Qabs a. Proof. unfold maxAbs; simpl. apply Qabs_case; intros; eapply Q.max_id. Qed. `````` Heiko Becker committed Aug 21, 2016 21 `````` `````` Heiko Becker committed Oct 06, 2016 22 ``````Lemma Qsub_eq_Qopp_Qplus (a:Q) (b:Q) : `````` Heiko Becker committed Aug 21, 2016 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 `````` (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. `````` Heiko Becker committed Oct 09, 2016 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 `````` 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.``````