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 (**************************************************************************)
16 include "cprop_connectives.ma".
18 notation "\rationals" non associative with precedence 99 for @{'q}.
19 interpretation "Q" 'q = Q.
25 interpretation "Q plus" 'plus x y = (qp x y).
26 interpretation "Q minus" 'minus x y = (qm x y).
28 axiom q_plus_OQ: ∀x:ℚ.x + OQ = x.
29 axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x.
30 axiom q_plus_minus: ∀x.Qpos x + Qneg x = OQ.
31 axiom q_minus: ∀x,y. y - Qpos x = y + Qneg x.
32 axiom q_minus_r: ∀x,y. y + Qpos x = y - Qneg x.
33 axiom q_plus_assoc: ∀x,y,z.x + (y + z) = x + y + z.
36 axiom qlt : ℚ → ℚ → CProp.
37 axiom qle : ℚ → ℚ → CProp.
38 interpretation "Q less than" 'lt x y = (qlt x y).
39 interpretation "Q less or equal than" 'leq x y = (qle x y).
41 inductive q_comparison (a,b:ℚ) : CProp ≝
42 | q_eq : a = b → q_comparison a b
43 | q_lt : a < b → q_comparison a b
44 | q_gt : b < a → q_comparison a b.
46 axiom q_cmp:∀a,b:ℚ.q_comparison a b.
48 axiom q_le_minus: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
49 axiom q_le_minus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b.
50 axiom q_lt_plus: ∀a,b,c:ℚ. a - b < c → a < c + b.
51 axiom q_lt_minus: ∀a,b,c:ℚ. a + b < c → a < c - b.
53 axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b.
54 axiom q_le_to_diff_ge_OQ : ∀a,b.a ≤ b → OQ ≤ b-a.
55 axiom q_lt_corefl: ∀x:Q.x < x → False.
56 axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False.
57 axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False.
58 axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z.
59 axiom q_le_trans: ∀x,y,z:Q. x ≤ y → y ≤ z → x ≤ z.
60 axiom q_pos_OQ: ∀x.Qpos x ≤ OQ → False.
61 axiom q_lt_plus_trans: ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y.
62 axiom q_pos_lt_OQ: ∀x.OQ < Qpos x.
63 axiom q_le_plus_trans: ∀x,y:Q. OQ ≤ x → OQ ≤ y → OQ ≤ x + y.
64 axiom q_le_S: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z.
65 axiom q_eq_to_le: ∀x,y. x = y → x ≤ y.
67 inductive q_le_elimination (a,b:ℚ) : CProp ≝
68 | q_le_from_eq : a = b → q_le_elimination a b
69 | q_le_from_lt : a < b → q_le_elimination a b.
71 axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y.
74 axiom q_dist : ℚ → ℚ → ℚ.
76 notation "hbox(\dd [term 19 x, break term 19 y])" with precedence 90
77 for @{'distance $x $y}.
78 interpretation "ℚ distance" 'distance x y = (q_dist x y).
80 axiom q_dist_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y].
81 axiom q_d_x_x: ∀x:Q.ⅆ[x,x] = OQ.
82 axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[x,y] = y - x.
83 axiom q_d_sym: ∀x,y. ⅆ[x,y] = ⅆ[y,x].
86 axiom nat_of_q: ℚ → nat.