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 ≝ ℚ × ℚ.
  21
  22 notation < "\rationals \sup 2" non associative with precedence 90 for @{'q2}.
  23 interpretation "Q x Q" 'q2 = (Prod Q Q).
  24
  25 definition empty_bar : bar ≝ 〈Qpos one,OQ〉.
  26 notation "\rect" with precedence 90 for @{'empty_bar}.
  27 interpretation "q0" 'empty_bar = empty_bar.
  28
  29 notation < "\ldots\rect\square\EmptySmallSquare\ldots" with precedence 90 for @{'lq2}.
  30 interpretation "lq2" 'lq2 = (list bar).
  31
  32 inductive sorted : list bar → Prop ≝
  33 | sorted_nil : sorted []
  34 | sorted_one : ∀x. sorted [x]
  35 | sorted_cons : ∀x,y,tl. \fst x < \fst y → sorted (y::tl) → sorted (x::y::tl).
  36
  37 definition nth_base ≝ λf,n. \fst (nth f ▭ n).
  38 definition nth_height ≝ λf,n. \snd (nth f ▭ n).
  39
  40 record q_f : Type ≝ {
  41  bars: list bar;
  42  increasing_bars : sorted bars;
  43  bars_begin_OQ : nth_base bars O = OQ;
  44  bars_tail_OQ : nth_height bars (pred (len bars)) = OQ
  45 }.
  46
  47 lemma nth_nil: ∀T,i.∀def:T. nth [] def i = def.
  48 intros; elim i; simplify; [reflexivity;] assumption; qed.
  49
  50 lemma all_bases_positives : ∀f:q_f.∀i.i < len (bars f) → OQ < nth_base (bars f) i.
  51 intro f; elim (increasing_bars f);
  52 [1: unfold nth_base; rewrite > nth_nil; apply (q_pos_OQ one);
  53 |2: cases i in H; [2: cases (?:False);
  54 qed.
  55
  56 definition eject_Q ≝
  57   λP.λp:∃x:ℚ.P x.match p with [ex_introT p _ ⇒ p].
  58 coercion eject_Q.
  59 definition inject_Q ≝ λP.λp:ℚ.λh:P p. ex_introT ? P p h.
  60 coercion inject_Q with 0 1 nocomposites.
  61
  62 definition value_spec : q_f → ℚ → ℚ → Prop ≝
  63   λf,i,q.
  64    ∃j.  q = nth_height (bars f) j ∧
  65         (nth_base (bars f) j < i ∧
  66          ∀n.j < n → n < len (bars f) → i ≤ nth_base (bars f) n).
  67
  68 definition value :  ∀f:q_f.∀i:ratio.∃p:ℚ.value_spec f (Qpos i) p.
  69 intros;
  70 alias symbol "lt" (instance 5) = "Q less than".
  71 alias symbol "leq" = "Q less or equal than".
  72 letin value_spec_aux ≝ (
  73   λf,i,q.∃j.  q = nth_height f j ∧
  74     (nth_base f j < i ∧ ∀n.j < n → n < len f → i ≤ nth_base f n));
  75 letin value ≝ (
  76   let rec value (acc: ℚ) (l : list bar) on l : ℚ ≝
  77     match l with
  78     [ nil ⇒ acc
  79     | cons x tl ⇒
  80         match q_cmp (\fst x) (Qpos i) with
  81         [ q_leq _ ⇒ value (\snd x) tl
  82         | q_gt _ ⇒ acc]]
  83   in value :
  84   ∀acc,l.∃p:ℚ. OQ ≤ acc → value_spec_aux l (Qpos i) p);
  85 [4: clearbody value; cases (value OQ (bars f)) (p Hp); exists[apply p];
  86     cases (Hp (q_le_n ?)) (j Hj); cases Hj (Hjp H); cases H (Hin Hmax);
  87     clear Hp value value_spec_aux Hj H; exists [apply j]; split[2:split;intros;]
  88     try apply Hmax; assumption;
  89 |1: intro Hacc; clear H2; cases (value (\snd b) l1) (j Hj);
  90     cases (q_cmp (\snd b) (Qpos i)) (Hib Hib);
  91     [1: cases (Hj Hib) (w Hw); simplify in ⊢ (? ? ? %); clear Hib Hj;
  92         exists [apply (S w)] cases Hw; cases H3; clear Hw H3;
  93         split; try assumption; split; try assumption; intros;
  94         apply (q_le_trans ??? (H5 (pred n) ??)); [3: apply q_le_n]
  95
  96
  97
  98
  99 [5: clearbody value;
 100     cases (q_cmp i (start f));
 101     [2: exists [apply 〈O,OQ〉] simplify; constructor 1; split; try assumption;
 102         try reflexivity; apply q_lt_to_le; assumption;
 103     |1: cases (bars f); [exists [apply 〈O,OQ〉] simplify; constructor 3; split;try assumption;reflexivity;]
 104         cases (value ⅆ[i,start f] (b::l)) (p Hp);
 105         cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; [cases H1; destruct H2]
 106         cases H1; clear H1; lapply (sum_bases_O (b::l) (\fst p)) as H1;
 107         [2: apply (q_le_trans ??? H2); rewrite > H; apply q_eq_to_le;
 108             rewrite > q_d_x_x; reflexivity;
 109         |1: exists [apply p] simplify; constructor 4; rewrite > H1; split;
 110             try split; try rewrite > q_d_x_x; try autobatch depth=2;
 111             [1: rewrite > H; rewrite > q_plus_sym; apply q_lt_plus;
 112                 rewrite > q_plus_minus; apply q_lt_plus_trans; [apply sum_bases_ge_OQ]
 113                 apply q_pos_lt_OQ;
 114             |2: rewrite > H; rewrite > q_d_x_x; apply q_eq_to_le; reflexivity;
 115             |3: rewrite > H; rewrite > q_d_x_x; apply q_lt_plus_trans;
 116                 try apply sum_bases_ge_OQ; apply q_pos_lt_OQ;]]
 117     |3: cases (q_cmp i (start f+sum_bases (bars f) (len (bars f))));
 118         [1: exists [apply 〈O,OQ〉] simplify; constructor 2; split; try assumption;
 119             try reflexivity; rewrite > H1; apply q_eq_to_le; reflexivity;
 120         |3: exists [apply 〈O,OQ〉] simplify; constructor 2; split; try assumption;
 121             try reflexivity; apply q_lt_to_le; assumption;
 122         |2: generalize in match (refl_eq ? (bars f): bars f = bars f);
 123             generalize in match (bars f) in ⊢ (??? % → %); intro X; cases X; clear X;
 124             intros;
 125             [1: exists [apply 〈O,OQ〉] simplify; constructor 3; split; reflexivity;
 126             |2: cases (value ⅆ[i,start f] (b::l)) (p Hp);
 127                 cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; [cases H3;destruct H4]
 128                 cases H3; clear H3;
 129                 exists [apply p]; constructor 4; split; try split; try assumption;
 130                 [1: intro X; destruct X;
 131                 |2: apply q_lt_to_le; assumption;
 132                 |3: rewrite < H2; assumption;
 133                 |4: cases (cmp_nat (\fst p) (len (bars f)));
 134                     [1:apply lt_to_le;rewrite <H2; assumption|rewrite > H3;rewrite < H2;apply le_n]
 135                     cases (?:False); cases (\fst p) in H3 H4 H6; clear H5;
 136                     [1: intros; apply (not_le_Sn_O ? H5);
 137                     |2: rewrite > q_d_sym; rewrite > q_d_noabs; [2: apply q_lt_to_le; assumption]
 138                         intros; lapply (q_lt_inj_plus_r ?? (Qopp (start f)) H1); clear H1;
 139                         generalize in match Hletin;
 140                         rewrite > (q_plus_sym (start f)); rewrite < q_plus_assoc;
 141                         do 2 rewrite < q_elim_minus; rewrite > q_plus_minus;
 142                         rewrite > q_plus_OQ; intro K; apply (q_lt_corefl (i-start f));
 143                         apply (q_lt_le_trans ???? H3); rewrite < H2;
 144                         apply (q_lt_trans ??? K); apply sum_bases_increasing;
 145                         assumption;]]]]]
 146 |1,3: intros; right; split;
 147      [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1);
 148            cases (H2 (q_le_to_diff_ge_OQ ?? (? H1)));
 149            [1: intro; apply q_lt_to_le;assumption;
 150            |3: simplify; cases H4; apply q_le_minus; assumption;
 151            |2,5: simplify; cases H4; rewrite > H5; rewrite > H6;
 152                  apply q_le_minus; apply sum_bases_empty_nat_of_q_le_q;
 153            |4: intro X; rewrite > X; apply q_eq_to_le; reflexivity;
 154            |*: simplify; apply q_le_minus; cases H4; assumption;]
 155     |2,5: cases (value (q-Qpos (\fst b)) l1);
 156           cases (H4 (q_le_to_diff_ge_OQ ?? (? H1)));
 157           [1,4: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption;
 158           |3,6: cases H5; simplify; change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b));
 159                 apply q_lt_plus; assumption;
 160           |2,5: simplify; cases H5; rewrite > H6; simplify; rewrite > H7;
 161                 apply q_lt_plus; apply sum_bases_empty_nat_of_q_le_q_one;]
 162     |*: cases (value (q-Qpos (\fst b)) l1); simplify;
 163         cases (H4 (q_le_to_diff_ge_OQ ?? (? H1)));
 164         [1,4: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption;
 165         |3,6: cases H5; assumption;
 166         |*: cases H5; rewrite > H6; rewrite > H8;
 167             elim (\fst w); [1,3:reflexivity;] simplify; assumption;]]
 168 |2: clear value H2; simplify; intros; right; split; [assumption|3:reflexivity]
 169     rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption;
 170 |4: intros; left; split; reflexivity;]
 171 qed.
 172
 173 lemma value_OQ_l:
 174   ∀l,i.i < start l → \snd (\fst (value l i)) = OQ.
 175 intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1;
 176 try assumption; cases H2; cases (?:False); apply (q_lt_le_incompat ?? H H6);
 177 qed.
 178
 179 lemma value_OQ_r:
 180   ∀l,i.start l + sum_bases (bars l) (len (bars l)) ≤ i → \snd (\fst (value l i)) = OQ.
 181 intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1;
 182 try assumption; cases H2; cases (?:False); apply (q_lt_le_incompat ?? H7 H);
 183 qed.
 184
 185 lemma value_OQ_e:
 186   ∀l,i.bars l = [] → \snd (\fst (value l i)) = OQ.
 187 intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1;
 188 try assumption; cases H2; cases (?:False); apply (H1 H);
 189 qed.
 190
 191 inductive value_ok_spec (f : q_f) (i : ℚ) : nat × ℚ → Type ≝
 192  | value_ok : ∀n,q. n ≤ (len (bars f)) →
 193       q = \snd (nth (bars f) ▭ n) →
 194       sum_bases (bars f) n ≤ ⅆ[i,start f] →
 195            ⅆ[i, start f] < sum_bases (bars f) (S n) → value_ok_spec f i 〈n,q〉.
 196
 197 lemma value_ok:
 198   ∀f,i.bars f ≠ [] → start f ≤ i → i < start f + sum_bases (bars f) (len (bars f)) →
 199     value_ok_spec f i (\fst (value f i)).
 200 intros; cases (value f i); simplify;
 201 cases H3; simplify; clear H3; cases H4; clear H4;
 202 [1,2,3: cases (?:False);
 203   [1: apply (q_lt_le_incompat ?? H3 H1);
 204   |2: apply (q_lt_le_incompat ?? H2 H3);
 205   |3: apply (H H3);]
 206 |4: cases H7; clear H7; cases w in H3 H4 H5 H6 H8; simplify; intros;
 207     constructor 1; assumption;]
 208 qed.
 209
 210 definition same_values ≝
 211   λl1,l2:q_f.
 212    ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)).
 213
 214 definition same_bases ≝
 215   λl1,l2:list bar. (∀i.\fst (nth l1 ▭ i) = \fst (nth l2 ▭ i)).
 216
 217 alias symbol "lt" = "Q less than".
 218 lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.
 219 intro; cases x; intros; [2:exists [apply r] reflexivity]
 220 cases (?:False);
 221 [ apply (q_lt_corefl ? H)|apply (q_neg_gt ? H)]
 222 qed.
 223
 224 notation < "x \blacksquare" non associative with precedence 50 for @{'unpos $x}.
 225 interpretation "hide unpos proof" 'unpos x = (unpos x _).
 226