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 lemma sum_bases_n_m:
  93   ∀n,m,l.
  94     sum_bases l n < sum_bases l (S m) →
  95     sum_bases l m < sum_bases l (S n) →
  96     n = m.
  97 intros 2; apply (nat_elim2 ???? n m);
  98 [1: intro X; cases X; intros; [reflexivity] cases (?:False);
  99     cases l in H H1; simplify; intros;
 100     apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1));
 101     apply (q_lt_canc_plus_r ??? H1);
 102 |2: intros 2; cases l; simplify; intros; cases (?:False);
 103     apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1));
 104     apply (q_lt_canc_plus_r ??? H); (* magia ... *)
 105 |3: intros 4; cases l; simplify; intros;
 106     [1: rewrite > (H []); [reflexivity]
 107         apply (q_lt_canc_plus_r ??(Qpos one)); assumption;
 108     |2: rewrite > (H l1); [reflexivity]
 109         apply (q_lt_canc_plus_r ??(Qpos (\fst b))); assumption;]]
 110 qed.
 111
 112 definition eject1 ≝
 113   λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p].
 114 coercion eject1.
 115 definition inject1 ≝ λP.λp:nat × ℚ.λh:P p. ex_introT ? P p h.
 116 coercion inject1 with 0 1 nocomposites.
 117
 118 definition value :
 119   ∀f:q_f.∀i:ℚ.∃p:nat × ℚ.
 120    Or4
 121     (And3 (i < start f) (\fst p = O) (\snd p = OQ))
 122     (And3
 123      (start f + sum_bases (bars f) (len (bars f)) ≤ i)
 124      (\fst p = O) (\snd p = OQ))
 125     (And3 (bars f = []) (\fst p = O) (\snd p = OQ))
 126     (And4
 127      (And3 (bars f ≠ []) (start f ≤ i) (i < start f + sum_bases (bars f) (len (bars f))))
 128      (\fst p ≤ (len (bars f)))
 129      (\snd p = \snd (nth (bars f) ▭ (\fst p)))
 130      (sum_bases (bars f) (\fst p) ≤ ⅆ[i,start f] ∧
 131        (ⅆ[i, start f] < sum_bases (bars f) (S (\fst p))))).
 132 intros;
 133 letin value ≝ (
 134   let rec value (p: ℚ) (l : list bar) on l ≝
 135     match l with
 136     [ nil ⇒ 〈nat_of_q p,OQ〉
 137     | cons x tl ⇒
 138         match q_cmp p (Qpos (\fst x)) with
 139         [ q_lt _ ⇒ 〈O, \snd x〉
 140         | _ ⇒
 141            let rc ≝ value (p - Qpos (\fst x)) tl in
 142            〈S (\fst rc),\snd rc〉]]
 143   in value :
 144   ∀acc,l.∃p:nat × ℚ.OQ ≤ acc →
 145      Or
 146       (And3 (l = []) (\fst p = nat_of_q acc) (\snd p = OQ))
 147       (And3
 148        (sum_bases l (\fst p) ≤ acc)
 149        (acc < sum_bases l (S (\fst p)))
 150        (\snd p = \snd (nth l ▭ (\fst p)))));
 151 [5: clearbody value;
 152     cases (q_cmp i (start f));
 153     [2: exists [apply 〈O,OQ〉] simplify; constructor 1; split; try assumption;
 154         try reflexivity; apply q_lt_to_le; assumption;
 155     |1: cases (bars f); [exists [apply 〈O,OQ〉] simplify; constructor 3; split;try assumption;reflexivity;]
 156         cases (value ⅆ[i,start f] (b::l)) (p Hp);
 157         cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; [cases H1; destruct H2]
 158         cases H1; clear H1; lapply (sum_bases_O (b::l) (\fst p)) as H1;
 159         [2: apply (q_le_trans ??? H2); rewrite > H; apply q_eq_to_le;
 160             rewrite > q_d_x_x; reflexivity;
 161         |1: exists [apply p] simplify; constructor 4; rewrite > H1; split;
 162             try split; try rewrite > q_d_x_x; try autobatch depth=2;
 163             [1: rewrite > H; rewrite > q_plus_sym; apply q_lt_plus;
 164                 rewrite > q_plus_minus; apply q_lt_plus_trans; [apply sum_bases_ge_OQ]
 165                 apply q_pos_lt_OQ;
 166             |2: rewrite > H; rewrite > q_d_x_x; apply q_eq_to_le; reflexivity;
 167             |3: rewrite > H; rewrite > q_d_x_x; apply q_lt_plus_trans;
 168                 try apply sum_bases_ge_OQ; apply q_pos_lt_OQ;]]
 169     |3: cases (q_cmp i (start f+sum_bases (bars f) (len (bars f))));
 170         [1: exists [apply 〈O,OQ〉] simplify; constructor 2; split; try assumption;
 171             try reflexivity; rewrite > H1; apply q_eq_to_le; reflexivity;
 172         |3: exists [apply 〈O,OQ〉] simplify; constructor 2; split; try assumption;
 173             try reflexivity; apply q_lt_to_le; assumption;
 174         |2: generalize in match (refl_eq ? (bars f): bars f = bars f);
 175             generalize in match (bars f) in ⊢ (??? % → %); intro X; cases X; clear X;
 176             intros;
 177             [1: exists [apply 〈O,OQ〉] simplify; constructor 3; split; reflexivity;
 178             |2: cases (value ⅆ[i,start f] (b::l)) (p Hp);
 179                 cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; [cases H3;destruct H4]
 180                 cases H3; clear H3;
 181                 exists [apply p]; constructor 4; split; try split; try assumption;
 182                 [1: intro X; destruct X;
 183                 |2: apply q_lt_to_le; assumption;
 184                 |3: rewrite < H2; assumption;
 185                 |4: cases (cmp_nat (\fst p) (len (bars f)));
 186                     [1:apply lt_to_le;rewrite <H2; assumption|rewrite > H3;rewrite < H2;apply le_n]
 187                     cases (?:False); cases (\fst p) in H3 H4 H6; clear H5;
 188                     [1: intros; apply (not_le_Sn_O ? H5);
 189                     |2: rewrite > q_d_sym; rewrite > q_d_noabs; [2: apply q_lt_to_le; assumption]
 190                         intros; lapply (q_lt_inj_plus_r ?? (Qopp (start f)) H1); clear H1;
 191                         generalize in match Hletin;
 192                         rewrite > (q_plus_sym (start f)); rewrite < q_plus_assoc;
 193                         do 2 rewrite < q_elim_minus; rewrite > q_plus_minus;
 194                         rewrite > q_plus_OQ; intro K; apply (q_lt_corefl (i-start f));
 195                         apply (q_lt_le_trans ???? H3); rewrite < H2;
 196                         apply (q_lt_trans ??? K); apply sum_bases_increasing;
 197                         assumption;]]]]]
 198 |1,3: intros; right; split;
 199      [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1);
 200            cases (H2 (q_le_to_diff_ge_OQ ?? (? H1)));
 201            [1: intro; apply q_lt_to_le;assumption;
 202            |3: simplify; cases H4; apply q_le_minus; assumption;
 203            |2,5: simplify; cases H4; rewrite > H5; rewrite > H6;
 204                  apply q_le_minus; apply sum_bases_empty_nat_of_q_le_q;
 205            |4: intro X; rewrite > X; apply q_eq_to_le; reflexivity;
 206            |*: simplify; apply q_le_minus; cases H4; assumption;]
 207     |2,5: cases (value (q-Qpos (\fst b)) l1);
 208           cases (H4 (q_le_to_diff_ge_OQ ?? (? H1)));
 209           [1,4: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption;
 210           |3,6: cases H5; simplify; change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b));
 211                 apply q_lt_plus; assumption;
 212           |2,5: simplify; cases H5; rewrite > H6; simplify; rewrite > H7;
 213                 apply q_lt_plus; apply sum_bases_empty_nat_of_q_le_q_one;]
 214     |*: cases (value (q-Qpos (\fst b)) l1); simplify;
 215         cases (H4 (q_le_to_diff_ge_OQ ?? (? H1)));
 216         [1,4: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption;
 217         |3,6: cases H5; assumption;
 218         |*: cases H5; rewrite > H6; rewrite > H8;
 219             elim (\fst w); [1,3:reflexivity;] simplify; assumption;]]
 220 |2: clear value H2; simplify; intros; right; split; [assumption|3:reflexivity]
 221     rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption;
 222 |4: intros; left; split; reflexivity;]
 223 qed.
 224
 225 lemma value_OQ_l:
 226   ∀l,i.i < start l → \snd (\fst (value l i)) = OQ.
 227 intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1;
 228 try assumption; cases H2; cases (?:False); apply (q_lt_le_incompat ?? H H6);
 229 qed.
 230
 231 lemma value_OQ_r:
 232   ∀l,i.start l + sum_bases (bars l) (len (bars l)) ≤ i → \snd (\fst (value l i)) = OQ.
 233 intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1;
 234 try assumption; cases H2; cases (?:False); apply (q_lt_le_incompat ?? H7 H);
 235 qed.
 236
 237 lemma value_OQ_e:
 238   ∀l,i.bars l = [] → \snd (\fst (value l i)) = OQ.
 239 intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1;
 240 try assumption; cases H2; cases (?:False); apply (H1 H);
 241 qed.
 242
 243 inductive value_ok_spec (f : q_f) (i : ℚ) : nat × ℚ → Type ≝
 244  | value_ok : ∀n,q. n ≤ (len (bars f)) →
 245       q = \snd (nth (bars f) ▭ n) →
 246       sum_bases (bars f) n ≤ ⅆ[i,start f] →
 247            ⅆ[i, start f] < sum_bases (bars f) (S n) → value_ok_spec f i 〈n,q〉.
 248
 249 lemma value_ok:
 250   ∀f,i.bars f ≠ [] → start f ≤ i → i < start f + sum_bases (bars f) (len (bars f)) →
 251     value_ok_spec f i (\fst (value f i)).
 252 intros; cases (value f i); simplify;
 253 cases H3; simplify; clear H3; cases H4; clear H4;
 254 [1,2,3: cases (?:False);
 255   [1: apply (q_lt_le_incompat ?? H3 H1);
 256   |2: apply (q_lt_le_incompat ?? H2 H3);
 257   |3: apply (H H3);]
 258 |4: cases H7; clear H7; cases w in H3 H4 H5 H6 H8; simplify; intros;
 259     constructor 1; assumption;]
 260 qed.
 261
 262 definition same_values ≝
 263   λl1,l2:q_f.
 264    ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)).
 265
 266 definition same_bases ≝
 267   λl1,l2:list bar. (∀i.\fst (nth l1 ▭ i) = \fst (nth l2 ▭ i)).
 268
 269 alias symbol "lt" = "Q less than".
 270 lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.
 271 intro; cases x; intros; [2:exists [apply r] reflexivity]
 272 cases (?:False);
 273 [ apply (q_lt_corefl ? H)|apply (q_neg_gt ? H)]
 274 qed.
 275
 276 notation < "x \blacksquare" non associative with precedence 50 for @{'unpos $x}.
 277 interpretation "hide unpos proof" 'unpos x = (unpos x _).
 278