RationalSimps.v 1.94 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 ``````Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs. `````` Heiko Becker committed Oct 28, 2016 5 ``````Require Import Coq.micromega.Psatz. `````` Heiko Becker committed Nov 04, 2016 6 ``````Require Import Daisy.Infra.Abbrevs Daisy.Infra.Ltacs. `````` Heiko Becker committed Aug 20, 2016 7 8 `````` Definition Qleb :=Qle_bool. `````` Heiko Becker committed Aug 21, 2016 9 ``````Definition Qeqb := Qeq_bool. `````` Heiko Becker committed Sep 05, 2016 10 `````` `````` Raphaël Monat committed Mar 01, 2017 11 ``````(* Definition machineEpsilon := (1#(2^53)). *) `````` Heiko Becker committed Sep 05, 2016 12 `````` `````` Heiko Becker committed Oct 06, 2016 13 14 ``````Definition maxAbs (iv:intv) := Qmax (Qabs (fst iv)) (Qabs (snd iv)). `````` Heiko Becker committed Aug 20, 2016 15 `````` `````` Heiko Becker committed Oct 31, 2016 16 17 18 ``````Definition minAbs (iv:intv) := Qmin (Qabs (fst iv)) (Qabs (snd iv)). `````` Heiko Becker committed Oct 06, 2016 19 20 21 22 23 24 ``````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 25 `````` `````` Heiko Becker committed Oct 06, 2016 26 ``````Lemma Qsub_eq_Qopp_Qplus (a:Q) (b:Q) : `````` Heiko Becker committed Aug 21, 2016 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 `````` (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 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 `````` 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. `````` Heiko Becker committed Oct 28, 2016 61 62 63 64 65 66 67 ``````Qed. Lemma equal_naming a b c d: (a#b) + (c#d) = (a*Zpos d + c * Zpos b)#(b*d). Proof. unfold Qplus, Qeq; auto. Qed.``````