RationalSimps.v 1.69 KB
Newer Older
1
2
3
(**
  Some simplification properties of rationals, not proven in the Standard Library
**)
Heiko Becker's avatar
Heiko Becker committed
4
5
6
7
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs.
Require Import Daisy.Infra.Abbrevs.

Definition Qleb :=Qle_bool.
8
Definition Qeqb := Qeq_bool.
9
10
11

Definition machineEpsilon := (1#(2^53)).

12
13
Definition maxAbs (iv:intv) :=
  Qmax (Qabs (fst iv)) (Qabs (snd iv)).
Heiko Becker's avatar
Heiko Becker committed
14

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.
21

22
Lemma Qsub_eq_Qopp_Qplus (a:Q) (b:Q) :
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.
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.