1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "Q/q/qtimes.ma".
16 include "Q/q/qplus.ma".
17 include "logic/cprop_connectives.ma".
19 interpretation "Q" 'Q = Q.
24 interpretation "Q plus" 'plus x y = (qp x y).
25 interpretation "Q minus" 'minus x y = (qp x (Qopp y)).
27 axiom q_plus_OQ: ∀x:ℚ.x + OQ = x.
28 axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x.
29 axiom q_plus_minus: ∀x.x - x = OQ.
30 axiom q_plus_assoc: ∀x,y,z.x + (y + z) = x + y + z.
31 axiom q_opp_plus: ∀x,y,z:Q. Qopp (y + z) = Qopp y + Qopp z.
34 axiom qlt : ℚ → ℚ → Prop.
35 axiom qle : ℚ → ℚ → Prop.
36 interpretation "Q less than" 'lt x y = (qlt x y).
37 interpretation "Q less or equal than" 'leq x y = (qle x y).
39 inductive q_comparison (a,b:ℚ) : CProp ≝
40 | q_leq : a ≤ b → q_comparison a b
41 | q_gt : b < a → q_comparison a b.
43 axiom q_cmp:∀a,b:ℚ.q_comparison a b.
45 inductive q_le_elimination (a,b:ℚ) : CProp ≝
46 | q_le_from_eq : a = b → q_le_elimination a b
47 | q_le_from_lt : a < b → q_le_elimination a b.
49 axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y.
51 axiom q_le_to_le_to_eq : ∀x,y. x ≤ y → y ≤ x → x = y.
53 axiom q_le_plus_l: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
54 axiom q_le_plus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b.
55 axiom q_lt_plus_l: ∀a,b,c:ℚ. a < c - b → a + b < c.
56 axiom q_lt_plus_r: ∀a,b,c:ℚ. a - b < c → a < c + b.
58 axiom q_lt_opp_opp: ∀a,b.b < a → Qopp a < Qopp b.
60 axiom q_le_n: ∀x. x ≤ x.
61 axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b.
63 axiom q_lt_corefl: ∀x:Q.x < x → False.
64 axiom q_lt_le_incompat: ∀x,y:Q.x < y → y ≤ x → False.
66 axiom q_neg_gt: ∀r:ratio.Qneg r < OQ.
67 axiom q_pos_OQ: ∀x.OQ < Qpos x.
69 axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z.
70 axiom q_lt_le_trans: ∀x,y,z:Q. x < y → y ≤ z → x < z.
71 axiom q_le_lt_trans: ∀x,y,z:Q. x ≤ y → y < z → x < z.
72 axiom q_le_trans: ∀x,y,z:Q. x ≤ y → y ≤ z → x ≤ z.
74 axiom q_le_lt_OQ_plus_trans: ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y.
75 axiom q_lt_le_OQ_plus_trans: ∀x,y:Q.OQ < x → OQ ≤ y → OQ < x + y.
76 axiom q_le_OQ_plus_trans: ∀x,y:Q.OQ ≤ x → OQ ≤ y → OQ ≤ x + y.
78 axiom q_leWl: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z.
79 axiom q_ltWl: ∀x,y,z.OQ ≤ x → x + y < z → y < z.
82 axiom q_dist : ℚ → ℚ → ℚ.
84 notation "hbox(\dd [term 19 x, break term 19 y])" with precedence 90
85 for @{'distance $x $y}.
86 interpretation "ℚ distance" 'distance x y = (q_dist x y).
88 axiom q_d_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y].
89 axiom q_d_OQ: ∀x:Q.ⅆ[x,x] = OQ.
90 axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[y,x] = y - x.
91 axiom q_d_sym: ∀x,y. ⅆ[x,y] = ⅆ[y,x].
93 lemma q_2opp: ∀x:ℚ.Qopp (Qopp x) = x.
94 intros; cases x; reflexivity; qed.
97 lemma q_lt_canc_plus_r:
98 ∀x,y,z:Q.x + z < y + z → x < y.
99 intros; rewrite < (q_plus_OQ y); rewrite < (q_plus_minus z);
100 rewrite > q_plus_assoc; apply q_lt_plus_r; rewrite > q_2opp; assumption;
103 lemma q_lt_inj_plus_r:
104 ∀x,y,z:Q.x < y → x + z < y + z.
105 intros; apply (q_lt_canc_plus_r ?? (Qopp z));
106 do 2 rewrite < q_plus_assoc; rewrite > q_plus_minus;
107 do 2 rewrite > q_plus_OQ; assumption;
110 lemma q_le_inj_plus_r:
111 ∀x,y,z:Q.x ≤ y → x + z ≤ y + z.
112 intros;cases (q_le_cases ?? H);
113 [1: rewrite > H1; apply q_le_n;
114 |2: apply q_lt_to_le; apply q_lt_inj_plus_r; assumption;]
117 lemma q_le_canc_plus_r:
118 ∀x,y,z:Q.x + z ≤ y + z → x ≤ y.
119 intros; lapply (q_le_inj_plus_r ?? (Qopp z) H) as H1;
120 do 2 rewrite < q_plus_assoc in H1;
121 rewrite > q_plus_minus in H1; do 2 rewrite > q_plus_OQ in H1; assumption;