helm/software/matita/contribs/dama/dama/models/q_support.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "Q/q/q.ma".
  16 include "cprop_connectives.ma".
  17
  18 notation "\rationals" non associative with precedence 99 for @{'q}.
  19 interpretation "Q" 'q = Q.
  20
  21 (* group over Q *)
  22 axiom qp : ℚ → ℚ → ℚ.
  23 axiom qm : ℚ → ℚ → ℚ.
  24
  25 interpretation "Q plus" 'plus x y = (qp x y).
  26 interpretation "Q minus" 'minus x y = (qm x y).
  27
  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.x - 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.
  34 axiom q_elim_minus: ∀x,y.x - y = x + Qopp y.
  35 axiom q_elim_opp: ∀x,y.x - Qopp y = x + y.
  36 axiom q_minus_distrib:∀x,y,z:Q.x - (y + z) = x - y - z.
  37
  38 (* order over Q *)
  39 axiom qlt : ℚ → ℚ → CProp.
  40 axiom qle : ℚ → ℚ → CProp.
  41 interpretation "Q less than" 'lt x y = (qlt x y).
  42 interpretation "Q less or equal than" 'leq x y = (qle x y).
  43
  44 inductive q_comparison (a,b:ℚ) : CProp ≝
  45  | q_eq : a = b → q_comparison a b
  46  | q_lt : a < b → q_comparison a b
  47  | q_gt : b < a → q_comparison a b.
  48
  49 axiom q_cmp:∀a,b:ℚ.q_comparison a b.
  50
  51 axiom q_le_minus: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
  52 axiom q_le_minus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b.
  53 axiom q_lt_plus: ∀a,b,c:ℚ. a - b < c → a < c + b.
  54 axiom q_lt_minus: ∀a,b,c:ℚ. a + b < c → a < c - b.
  55 axiom q_le_plus: ∀a,b,c:ℚ. a ≤ c + b → a - b ≤ c.
  56 axiom q_le_plus_r: ∀a,b,c:ℚ. a + b ≤ c → a ≤ c - b.
  57 axiom q_lt_plus_r: ∀a,b,c:ℚ. a + b < c → a < c - b.
  58 axiom q_lt_minus_r: ∀a,b,c:ℚ. a - b < c → a < c + b.
  59 axiom q_lt_opp_opp: ∀a,b.b < a → Qopp a < Qopp b.
  60 axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b.
  61 axiom q_le_to_diff_ge_OQ : ∀a,b.a ≤ b → OQ ≤ b-a.
  62 axiom q_lt_corefl: ∀x:Q.x < x → False.
  63 axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False.
  64 axiom q_lt_le_incompat: ∀x,y:Q.x < y → y ≤ x → False.
  65 axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False.
  66 axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z.
  67 axiom q_lt_le_trans: ∀x,y,z:Q. x < y → y ≤ z → x < z.
  68 axiom q_le_lt_trans: ∀x,y,z:Q. x ≤ y → y < z → x < z.
  69 axiom q_le_trans: ∀x,y,z:Q. x ≤ y → y ≤ z → x ≤ z.
  70 axiom q_pos_OQ: ∀x.Qpos x ≤ OQ → False.
  71 axiom q_lt_plus_trans: ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y.
  72 axiom q_pos_lt_OQ: ∀x.OQ < Qpos x.
  73 axiom q_le_plus_trans: ∀x,y:Q. OQ ≤ x → OQ ≤ y → OQ ≤ x + y.
  74 axiom q_le_S: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z.
  75 axiom q_eq_to_le: ∀x,y. x = y → x ≤ y.
  76 axiom q_le_OQ_Qpos: ∀x.OQ ≤ Qpos x.
  77
  78
  79 inductive q_le_elimination (a,b:ℚ) : CProp ≝
  80 | q_le_from_eq : a = b → q_le_elimination a b
  81 | q_le_from_lt : a < b → q_le_elimination a b.
  82
  83 axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y.
  84
  85 (* distance *)
  86 axiom q_dist : ℚ → ℚ → ℚ.
  87
  88 notation "hbox(\dd [term 19 x, break term 19 y])" with precedence 90
  89 for @{'distance $x $y}.
  90 interpretation "ℚ distance" 'distance x y = (q_dist x y).
  91
  92 axiom q_dist_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y].
  93 axiom q_d_x_x: ∀x:Q.ⅆ[x,x] = OQ.
  94 axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[x,y] = y - x.
  95 axiom q_d_sym:  ∀x,y. ⅆ[x,y] = ⅆ[y,x].
  96
  97 (* integral part *)
  98 axiom nat_of_q: ℚ → nat.
  99
 100 (* derived *)
 101 lemma q_lt_canc_plus_r:
 102   ∀x,y,z:Q.x + z < y + z → x < y.
 103 intros; rewrite < (q_plus_OQ y); rewrite < (q_plus_minus z);
 104 rewrite > q_elim_minus; rewrite > q_plus_assoc;
 105 apply q_lt_plus; rewrite > q_elim_opp; assumption;
 106 qed.
 107
 108 lemma q_lt_inj_plus_r:
 109   ∀x,y,z:Q.x < y → x + z < y + z.
 110 intros; apply (q_lt_canc_plus_r ?? (Qopp z));
 111 do 2 (rewrite < q_plus_assoc;rewrite < q_elim_minus);
 112 rewrite > q_plus_minus;
 113 do 2 rewrite > q_plus_OQ; assumption;
 114 qed.
 115
 116 lemma q_le_inj_plus_r:
 117   ∀x,y,z:Q.x ≤ y → x + z ≤ y + z.
 118 intros;cases (q_le_cases ?? H);
 119 [1: rewrite > H1; apply q_eq_to_le; reflexivity;
 120 |2: apply q_lt_to_le; apply q_lt_inj_plus_r; assumption;]
 121 qed.
 122
 123 lemma q_le_canc_plus_r:
 124   ∀x,y,z:Q.x + z ≤ y + z → x ≤ y.
 125 intros; lapply (q_le_inj_plus_r ?? (Qopp z) H) as H1;
 126 do 2 rewrite < q_plus_assoc in H1;
 127 rewrite < q_elim_minus in H1; rewrite > q_plus_minus in H1;
 128 do 2 rewrite > q_plus_OQ in H1; assumption;
 129 qed.