X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_support.ma;h=6694a033fa6494902a7f499a95eff54063faf569;hb=2ddda3a0f1e22c9b5c9572896cdaf69b3c4d19d2;hp=2073c8a77afad47f5b6d6c64b56464a1db1ff0a0;hpb=88b32d4e8fe371d59e41cd272064c9d486ae7ec5;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/models/q_support.ma b/helm/software/matita/contribs/dama/dama/models/q_support.ma
index 2073c8a77..6694a033f 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma
@@ -12,7 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Q/q/q.ma".
+include "Q/q/qtimes.ma".
+include "Q/q/qplus.ma".
 include "cprop_connectives.ma".
 
 notation "\rationals" non associative with precedence 99 for @{'q}.
@@ -20,63 +21,61 @@ interpretation "Q" 'q = Q.
 
 (* group over Q *)
 axiom qp : ℚ → ℚ → ℚ.
-axiom qm : ℚ → ℚ → ℚ.
 
 interpretation "Q plus" 'plus x y = (qp x y).
-interpretation "Q minus" 'minus x y = (qm x y).
+interpretation "Q minus" 'minus x y = (qp x (Qopp y)).
 
 axiom q_plus_OQ: ∀x:ℚ.x + OQ = x.
 axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x.
 axiom q_plus_minus: ∀x.x - x = OQ.
-axiom q_minus: ∀x,y. y - Qpos x = y + Qneg x.
-axiom q_minus_r: ∀x,y. y + Qpos x = y - Qneg x.
 axiom q_plus_assoc: ∀x,y,z.x + (y + z) = x + y + z. 
-axiom q_elim_minus: ∀x,y.x - y = x + Qopp y.
-axiom q_elim_opp: ∀x,y.x - Qopp y = x + y.
-axiom q_minus_distrib:∀x,y,z:Q.x - (y + z) = x - y - z.
+axiom q_opp_plus: ∀x,y,z:Q. Qopp (y + z) = Qopp y + Qopp z.
 
 (* order over Q *)
-axiom qlt : ℚ → ℚ → CProp.
-axiom qle : ℚ → ℚ → CProp.
+axiom qlt : ℚ → ℚ → Prop.
+axiom qle : ℚ → ℚ → Prop.
 interpretation "Q less than" 'lt x y = (qlt x y).
 interpretation "Q less or equal than" 'leq x y = (qle x y).
 
 inductive q_comparison (a,b:ℚ) : CProp ≝
- | q_eq : a = b → q_comparison a b 
- | q_lt : a < b → q_comparison a b
+ | q_leq : a ≤ b → q_comparison a b 
  | q_gt : b < a → q_comparison a b.
 
 axiom q_cmp:∀a,b:ℚ.q_comparison a b.
 
-axiom q_le_minus: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
-axiom q_le_minus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b.
-axiom q_lt_plus: ∀a,b,c:ℚ. a - b < c → a < c + b.
-axiom q_lt_minus: ∀a,b,c:ℚ. a + b < c → a < c - b.
+inductive q_le_elimination (a,b:ℚ) : CProp ≝
+| q_le_from_eq : a = b → q_le_elimination a b
+| q_le_from_lt : a < b → q_le_elimination a b.
+
+axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y.
+
+axiom q_le_plus_l: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
+axiom q_le_plus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b.
+axiom q_lt_plus_l: ∀a,b,c:ℚ. a < c - b → a + b < c.
+axiom q_lt_plus_r: ∀a,b,c:ℚ. a - b < c → a < c + b.
+
 axiom q_lt_opp_opp: ∀a,b.b < a → Qopp a < Qopp b.
+
+axiom q_le_n: ∀x. x ≤ x.
 axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b.
-axiom q_le_to_diff_ge_OQ : ∀a,b.a ≤ b → OQ ≤ b-a.
+
 axiom q_lt_corefl: ∀x:Q.x < x → False.
-axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False.
 axiom q_lt_le_incompat: ∀x,y:Q.x < y → y ≤ x → False.
-axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False.
+
+axiom q_neg_gt: ∀r:ratio.Qneg r < OQ.
+axiom q_pos_OQ: ∀x.OQ < Qpos x.
+
 axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z.
 axiom q_lt_le_trans: ∀x,y,z:Q. x < y → y ≤ z → x < z.
 axiom q_le_lt_trans: ∀x,y,z:Q. x ≤ y → y < z → x < z.
 axiom q_le_trans: ∀x,y,z:Q. x ≤ y → y ≤ z → x ≤ z.
-axiom q_pos_OQ: ∀x.Qpos x ≤ OQ → False.
-axiom q_lt_plus_trans: ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y.
-axiom q_pos_lt_OQ: ∀x.OQ < Qpos x.
-axiom q_le_plus_trans: ∀x,y:Q. OQ ≤ x → OQ ≤ y → OQ ≤ x + y.
-axiom q_le_S: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z.
-axiom q_eq_to_le: ∀x,y. x = y → x ≤ y.
-axiom q_le_OQ_Qpos: ∀x.OQ ≤ Qpos x.
-       
 
-inductive q_le_elimination (a,b:ℚ) : CProp ≝
-| q_le_from_eq : a = b → q_le_elimination a b
-| q_le_from_lt : a < b → q_le_elimination a b.
+axiom q_le_lt_OQ_plus_trans: ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y.
+axiom q_lt_le_OQ_plus_trans: ∀x,y:Q.OQ < x → OQ ≤ y → OQ < x + y.
+axiom q_le_OQ_plus_trans: ∀x,y:Q.OQ ≤ x → OQ ≤ y → OQ ≤ x + y.
 
-axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y.
+axiom q_leWl: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z.
+axiom q_ltWl: ∀x,y,z.OQ ≤ x → x + y < z → y < z.
 
 (* distance *)
 axiom q_dist : ℚ → ℚ → ℚ.
@@ -85,27 +84,38 @@ notation "hbox(\dd [term 19 x, break term 19 y])" with precedence 90
 for @{'distance $x $y}.
 interpretation "ℚ distance" 'distance x y = (q_dist x y).
 
-axiom q_dist_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y].
-axiom q_d_x_x: ∀x:Q.ⅆ[x,x] = OQ.
-axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[x,y] = y - x.
-axiom q_d_sym:  ∀x,y. ⅆ[x,y] = ⅆ[y,x].
+axiom q_d_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y].
+axiom q_d_OQ: ∀x:Q.ⅆ[x,x] = OQ.
+axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[y,x] = y - x.
+axiom q_d_sym: ∀x,y. ⅆ[x,y] = ⅆ[y,x].
 
-(* integral part *)
-axiom nat_of_q: ℚ → nat.
+lemma q_2opp: ∀x:ℚ.Qopp (Qopp x) = x.
+intros; cases x; reflexivity; qed.
 
 (* derived *)
 lemma q_lt_canc_plus_r:
   ∀x,y,z:Q.x + z < y + z → x < y.
 intros; rewrite < (q_plus_OQ y); rewrite < (q_plus_minus z);
-rewrite > q_elim_minus; rewrite > q_plus_assoc;
-apply q_lt_plus; rewrite > q_elim_opp; assumption;
+rewrite > q_plus_assoc; apply q_lt_plus_r; rewrite > q_2opp; assumption;
 qed.
 
 lemma q_lt_inj_plus_r:
   ∀x,y,z:Q.x < y → x + z < y + z.
 intros; apply (q_lt_canc_plus_r ?? (Qopp z));
-do 2 (rewrite < q_plus_assoc;rewrite < q_elim_minus);
-rewrite > q_plus_minus;
+do 2 rewrite < q_plus_assoc; rewrite > q_plus_minus; 
 do 2 rewrite > q_plus_OQ; assumption;
 qed.
 
+lemma q_le_inj_plus_r:
+  ∀x,y,z:Q.x ≤ y → x + z ≤ y + z.
+intros;cases (q_le_cases ?? H);
+[1: rewrite > H1; apply q_le_n;
+|2: apply q_lt_to_le; apply q_lt_inj_plus_r; assumption;]
+qed.
+
+lemma q_le_canc_plus_r:
+  ∀x,y,z:Q.x + z ≤ y + z → x ≤ y.
+intros; lapply (q_le_inj_plus_r ?? (Qopp z) H) as H1;
+do 2 rewrite < q_plus_assoc in H1;
+rewrite > q_plus_minus in H1; do 2 rewrite > q_plus_OQ in H1; assumption;
+qed.