helm/software/matita/contribs/dama/dama/models/q_bars.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 "nat_ordered_set.ma".
  16 include "models/q_support.ma".
  17 include "models/list_support.ma".
  18 include "cprop_connectives.ma".
  19
  20 definition bar ≝ ratio × ℚ. (* base (Qpos) , height *)
  21 record q_f : Type ≝ { start : ℚ; bars: list bar }.
  22
  23 notation < "\rationals \sup 2" non associative with precedence 90 for @{'q2}.
  24 interpretation "Q x Q" 'q2 = (Prod Q Q).
  25
  26 definition empty_bar : bar ≝ 〈one,OQ〉.
  27 notation "\rect" with precedence 90 for @{'empty_bar}.
  28 interpretation "q0" 'empty_bar = empty_bar.
  29
  30 notation < "\ldots\rect\square\EmptySmallSquare\ldots" with precedence 90 for @{'lq2}.
  31 interpretation "lq2" 'lq2 = (list bar).
  32
  33 let rec sum_bases (l:list bar) (i:nat) on i ≝
  34     match i with
  35     [ O ⇒ OQ
  36     | S m ⇒
  37          match l with
  38          [ nil ⇒ sum_bases [] m + Qpos one
  39          | cons x tl ⇒ sum_bases tl m + Qpos (\fst x)]].
  40
  41 axiom sum_bases_empty_nat_of_q_ge_OQ:
  42   ∀q:ℚ.OQ ≤ sum_bases [] (nat_of_q q).
  43 axiom sum_bases_empty_nat_of_q_le_q:
  44   ∀q:ℚ.sum_bases [] (nat_of_q q) ≤ q.
  45 axiom sum_bases_empty_nat_of_q_le_q_one:
  46   ∀q:ℚ.q < sum_bases [] (nat_of_q q) + Qpos one.
  47
  48 lemma sum_bases_ge_OQ:
  49   ∀l,n. OQ ≤ sum_bases l n.
  50 intro; elim l; simplify; intros;
  51 [1: elim n; [apply q_eq_to_le;reflexivity] simplify;
  52     apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ;
  53 |2: cases n; [apply q_eq_to_le;reflexivity] simplify;
  54     apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]]
  55 qed.
  56
  57 alias symbol "leq" = "Q less or equal than".
  58 lemma sum_bases_O:
  59   ∀l.∀x.sum_bases l x ≤ OQ → x = O.
  60 intros; cases x in H; [intros; reflexivity] intro; cases (?:False);
  61 cases (q_le_cases ?? H);
  62 [1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %);
  63 |2: apply (q_lt_antisym ??? H1);] clear H H1; cases l;
  64 simplify; apply q_lt_plus_trans;
  65 try apply q_pos_lt_OQ;
  66 try apply (sum_bases_ge_OQ []);
  67 apply (sum_bases_ge_OQ l1);
  68 qed.
  69
  70
  71 lemma sum_bases_increasing:
  72   ∀l.∀n1,n2:nat.n1<n2→sum_bases l n1 < sum_bases l n2.
  73 intro; elim l 0;
  74 [1: intros 2; apply (cic:/matita/dama/nat_ordered_set/nat_elim2.con ???? n1 n2);
  75     [1: intro; cases n;
  76         [1: intro X; cases (not_le_Sn_O ? X);
  77         |2: simplify; intros; apply q_lt_plus_trans;
  78             [1: apply sum_bases_ge_OQ;|2: apply (q_pos_lt_OQ one)]]
  79     |2: simplify; intros;  cases (not_le_Sn_O ? H);
  80     |3: simplify; intros; apply q_lt_inj_plus_r;
  81         apply H; apply le_S_S_to_le; apply H1;]
  82 |2:  intros 5; apply (cic:/matita/dama/nat_ordered_set/nat_elim2.con ???? n1 n2);
  83     [1: simplify; intros; cases n in H1; intros;
  84         [1: cases (not_le_Sn_O ? H1);
  85         |2: simplify; apply q_lt_plus_trans;
  86             [1: apply sum_bases_ge_OQ;|2: apply q_pos_lt_OQ]]
  87     |2: simplify; intros; cases (not_le_Sn_O ? H1);
  88     |3: simplify; intros; apply q_lt_inj_plus_r; apply H;
  89         apply le_S_S_to_le; apply H2;]]
  90 qed.
  91
  92
  93 definition eject1 ≝
  94   λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p].
  95 coercion eject1.
  96 definition inject1 ≝ λP.λp:nat × ℚ.λh:P p. ex_introT ? P p h.
  97 coercion inject1 with 0 1 nocomposites.
  98
  99 definition value :
 100   ∀f:q_f.∀i:ℚ.∃p:nat × ℚ.
 101    Or4
 102     (And3 (i < start f) (\fst p = O) (\snd p = OQ))
 103     (And3
 104      (start f + sum_bases (bars f) (len (bars f)) ≤ i)
 105      (\fst p = O) (\snd p = OQ))
 106     (And3 (bars f = []) (\fst p = O) (\snd p = OQ))
 107     (And4
 108      (And3 (bars f ≠ []) (start f ≤ i) (i < start f + sum_bases (bars f) (len (bars f))))
 109      (\fst p ≤ (len (bars f)))
 110      (\snd p = \snd (nth (bars f) ▭ (\fst p)))
 111      (sum_bases (bars f) (\fst p) ≤ ⅆ[i,start f] ∧
 112        (ⅆ[i, start f] < sum_bases (bars f) (S (\fst p))))).
 113 intros;
 114 letin value ≝ (
 115   let rec value (p: ℚ) (l : list bar) on l ≝
 116     match l with
 117     [ nil ⇒ 〈nat_of_q p,OQ〉
 118     | cons x tl ⇒
 119         match q_cmp p (Qpos (\fst x)) with
 120         [ q_lt _ ⇒ 〈O, \snd x〉
 121         | _ ⇒
 122            let rc ≝ value (p - Qpos (\fst x)) tl in
 123            〈S (\fst rc),\snd rc〉]]
 124   in value :
 125   ∀acc,l.∃p:nat × ℚ.OQ ≤ acc →
 126      Or
 127       (And3 (l = []) (\fst p = nat_of_q acc) (\snd p = OQ))
 128       (And3
 129        (sum_bases l (\fst p) ≤ acc)
 130        (acc < sum_bases l (S (\fst p)))
 131        (\snd p = \snd (nth l ▭ (\fst p)))));
 132 [5: clearbody value;
 133     cases (q_cmp i (start f));
 134     [2: exists [apply 〈O,OQ〉] simplify; constructor 1; split; try assumption;
 135         try reflexivity; apply q_lt_to_le; assumption;
 136     |1: cases (bars f); [exists [apply 〈O,OQ〉] simplify; constructor 3; split;try assumption;reflexivity;]
 137         cases (value ⅆ[i,start f] (b::l)) (p Hp);
 138         cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; [cases H1; destruct H2]
 139         cases H1; clear H1; lapply (sum_bases_O (b::l) (\fst p)) as H1;
 140         [2: apply (q_le_trans ??? H2); rewrite > H; apply q_eq_to_le;
 141             rewrite > q_d_x_x; reflexivity;
 142         |1: exists [apply p] simplify; constructor 4; rewrite > H1; split;
 143             try split; try rewrite > q_d_x_x; try autobatch depth=2;
 144             [1: rewrite > H; rewrite > q_plus_sym; apply q_lt_plus;
 145                 rewrite > q_plus_minus; apply q_lt_plus_trans; [apply sum_bases_ge_OQ]
 146                 apply q_pos_lt_OQ;
 147             |2: rewrite > H; rewrite > q_d_x_x; apply q_eq_to_le; reflexivity;
 148             |3: rewrite > H; rewrite > q_d_x_x; apply q_lt_plus_trans;
 149                 try apply sum_bases_ge_OQ; apply q_pos_lt_OQ;]]
 150     |3: cases (q_cmp i (start f+sum_bases (bars f) (len (bars f))));
 151         [1: exists [apply 〈O,OQ〉] simplify; constructor 2; split; try assumption;
 152             try reflexivity; rewrite > H1; apply q_eq_to_le; reflexivity;
 153         |3: exists [apply 〈O,OQ〉] simplify; constructor 2; split; try assumption;
 154             try reflexivity; apply q_lt_to_le; assumption;
 155         |2: generalize in match (refl_eq ? (bars f): bars f = bars f);
 156             generalize in match (bars f) in ⊢ (??? % → %); intro X; cases X; clear X;
 157             intros;
 158             [1: exists [apply 〈O,OQ〉] simplify; constructor 3; split; reflexivity;
 159             |2: cases (value ⅆ[i,start f] (b::l)) (p Hp);
 160                 cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; [cases H3;destruct H4]
 161                 cases H3; clear H3;
 162                 exists [apply p]; constructor 4; split; try split; try assumption;
 163                 [1: intro X; destruct X;
 164                 |2: apply q_lt_to_le; assumption;
 165                 |3: rewrite < H2; assumption;
 166                 |4: cases (cmp_nat (\fst p) (len (bars f)));
 167                     [1:apply lt_to_le;rewrite <H2; assumption|rewrite > H3;rewrite < H2;apply le_n]
 168                     cases (?:False); cases (\fst p) in H3 H4 H6; clear H5;
 169                     [1: intros; apply (not_le_Sn_O ? H5);
 170                     |2: rewrite > q_d_sym; rewrite > q_d_noabs; [2: apply q_lt_to_le; assumption]
 171                         intros; lapply (q_lt_inj_plus_r ?? (Qopp (start f)) H1); clear H1;
 172                         generalize in match Hletin;
 173                         rewrite > (q_plus_sym (start f)); rewrite < q_plus_assoc;
 174                         do 2 rewrite < q_elim_minus; rewrite > q_plus_minus;
 175                         rewrite > q_plus_OQ; intro K; apply (q_lt_corefl (i-start f));
 176                         apply (q_lt_le_trans ???? H3); rewrite < H2;
 177                         apply (q_lt_trans ??? K); apply sum_bases_increasing;
 178                         assumption;]]]]]
 179 |1,3: intros; right; split;
 180      [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1);
 181            cases (H2 (q_le_to_diff_ge_OQ ?? (? H1)));
 182            [1: intro; apply q_lt_to_le;assumption;
 183            |3: simplify; cases H4; apply q_le_minus; assumption;
 184            |2,5: simplify; cases H4; rewrite > H5; rewrite > H6;
 185                  apply q_le_minus; apply sum_bases_empty_nat_of_q_le_q;
 186            |4: intro X; rewrite > X; apply q_eq_to_le; reflexivity;
 187            |*: simplify; apply q_le_minus; cases H4; assumption;]
 188     |2,5: cases (value (q-Qpos (\fst b)) l1);
 189           cases (H4 (q_le_to_diff_ge_OQ ?? (? H1)));
 190           [1,4: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption;
 191           |3,6: cases H5; simplify; change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b));
 192                 apply q_lt_plus; assumption;
 193           |2,5: simplify; cases H5; rewrite > H6; simplify; rewrite > H7;
 194                 apply q_lt_plus; apply sum_bases_empty_nat_of_q_le_q_one;]
 195     |*: cases (value (q-Qpos (\fst b)) l1); simplify;
 196         cases (H4 (q_le_to_diff_ge_OQ ?? (? H1)));
 197         [1,4: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption;
 198         |3,6: cases H5; assumption;
 199         |*: cases H5; rewrite > H6; rewrite > H8;
 200             elim (\fst w); [1,3:reflexivity;] simplify; assumption;]]
 201 |2: clear value H2; simplify; intros; right; split; [assumption|3:reflexivity]
 202     rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption;
 203 |4: intros; left; split; reflexivity;]
 204 qed.
 205
 206 lemma value_OQ_l:
 207   ∀l,i.i < start l → \snd (\fst (value l i)) = OQ.
 208 intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1;
 209 try assumption; cases H2; cases (?:False); apply (q_lt_le_incompat ?? H H6);
 210 qed.
 211
 212 lemma value_OQ_r:
 213   ∀l,i.start l + sum_bases (bars l) (len (bars l)) ≤ i → \snd (\fst (value l i)) = OQ.
 214 intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1;
 215 try assumption; cases H2; cases (?:False); apply (q_lt_le_incompat ?? H7 H);
 216 qed.
 217
 218 lemma value_OQ_e:
 219   ∀l,i.bars l = [] → \snd (\fst (value l i)) = OQ.
 220 intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1;
 221 try assumption; cases H2; cases (?:False); apply (H1 H);
 222 qed.
 223
 224 lemma value_ok:
 225   ∀f,i. bars f ≠ [] → start f ≤ i → i < start f + sum_bases (bars f) (len (bars f)) →
 226      And4
 227       (\fst (\fst (value f i)) ≤ (len (bars f)))
 228       (\snd (\fst (value f i)) = \snd (nth (bars f) ▭ (\fst (\fst (value f i)))))
 229       (sum_bases (bars f) (\fst (\fst (value f i))) ≤ ⅆ[i,start f])
 230       (ⅆ[i, start f] < sum_bases (bars f) (S (\fst (\fst (value f i))))).
 231 intros; cases (value f i); cases H3; simplify; clear H3; cases H4;
 232 [1,2,3: cases (?:False);
 233   [1: apply (q_lt_le_incompat ?? H3 H1);
 234   |2: apply (q_lt_le_incompat ?? H2 H3);
 235   |3: apply (H H3);]
 236 |4: split; cases H7; try assumption;]
 237 qed.
 238
 239 definition same_values ≝
 240   λl1,l2:q_f.
 241    ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)).
 242
 243 definition same_bases ≝
 244   λl1,l2:q_f.
 245     (∀i.\fst (nth (bars l1) ▭ i) = \fst (nth (bars l2) ▭ i)).
 246
 247 alias symbol "lt" = "Q less than".
 248 lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.
 249 intro; cases x; intros; [2:exists [apply r] reflexivity]
 250 cases (?:False);
 251 [ apply (q_lt_corefl ? H)|apply (q_neg_gt ? H)]
 252 qed.