RationalSimps.v 1.94 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
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs.
5
Require Import Coq.micromega.Psatz.
6
Require Import Daisy.Infra.Abbrevs Daisy.Infra.Ltacs.
Heiko Becker's avatar
Heiko Becker committed
7
8

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

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

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

16
17
18
Definition minAbs (iv:intv) :=
  Qmin (Qabs (fst iv)) (Qabs (snd iv)).

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

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