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 "models/q_support.ma".
  16 include "models/list_support.ma".
  17 include "cprop_connectives.ma".
  18
  19 definition bar ≝ ratio × ℚ. (* base (Qpos) , height *)
  20 record q_f : Type ≝ { start : ℚ; bars: list 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 ≝ 〈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 let rec sum_bases (l:list bar) (i:nat)on i ≝
  33     match i with
  34     [ O ⇒ OQ
  35     | S m ⇒
  36          match l with
  37          [ nil ⇒ sum_bases l m + Qpos one
  38          | cons x tl ⇒ sum_bases tl m + Qpos (\fst x)]].
  39
  40 axiom sum_bases_empty_nat_of_q_ge_OQ:
  41   ∀q:ℚ.OQ ≤ sum_bases [] (nat_of_q q).
  42 axiom sum_bases_empty_nat_of_q_le_q:
  43   ∀q:ℚ.sum_bases [] (nat_of_q q) ≤ q.
  44 axiom sum_bases_empty_nat_of_q_le_q_one:
  45   ∀q:ℚ.q < sum_bases [] (nat_of_q q) + Qpos one.
  46
  47 definition eject1 ≝
  48   λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p].
  49 coercion eject1.
  50 definition inject1 ≝ λP.λp:nat × ℚ.λh:P p. ex_introT ? P p h.
  51 coercion inject1 with 0 1 nocomposites.
  52
  53 definition value :
  54   ∀f:q_f.∀i:ℚ.∃p:nat × ℚ.
  55    match q_cmp i (start f) with
  56    [ q_lt _ ⇒ \snd p = OQ
  57    | _ ⇒
  58         And3
  59          (sum_bases (bars f) (\fst p) ≤ ⅆ[i,start f])
  60          (ⅆ[i, start f] < sum_bases (bars f) (S (\fst p)))
  61          (\snd p = \snd (nth (bars f) ▭ (\fst p)))].
  62 intros;
  63 alias symbol "pi2" = "pair pi2".
  64 alias symbol "pi1" = "pair pi1".
  65 letin value ≝ (
  66   let rec value (p: ℚ) (l : list bar) on l ≝
  67     match l with
  68     [ nil ⇒ 〈nat_of_q p,OQ〉
  69     | cons x tl ⇒
  70         match q_cmp p (Qpos (\fst x)) with
  71         [ q_lt _ ⇒ 〈O, \snd x〉
  72         | _ ⇒
  73            let rc ≝ value (p - Qpos (\fst x)) tl in
  74            〈S (\fst rc),\snd rc〉]]
  75   in value :
  76   ∀acc,l.∃p:nat × ℚ. OQ ≤ acc →
  77      And3
  78        (sum_bases l (\fst p) ≤ acc)
  79        (acc < sum_bases l (S (\fst p)))
  80        (\snd p = \snd (nth l ▭ (\fst p))));
  81 [5: clearbody value;
  82     cases (q_cmp i (start f));
  83     [2: exists [apply 〈O,OQ〉] simplify; reflexivity;
  84     |*: cases (value ⅆ[i,start f] (bars f)) (p Hp);
  85         cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value;
  86         exists[1,3:apply p]; simplify; split; assumption;]
  87 |1,3: intros; split;
  88     [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1);
  89            cases (H2 (q_le_to_diff_ge_OQ ?? (? H1)));
  90           [1,3: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption]
  91           simplify; apply q_le_minus; assumption;
  92     |2,5: cases (value (q-Qpos (\fst b)) l1);
  93           cases (H4 (q_le_to_diff_ge_OQ ?? (? H1)));
  94           [1,3: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption]
  95           clear H3 H2 value;
  96           change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b));
  97           apply q_lt_plus; assumption;
  98     |*: cases (value (q-Qpos (\fst b)) l1); simplify;
  99         cases (H4 (q_le_to_diff_ge_OQ ?? (? H1)));
 100         [1,3: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption]
 101         assumption;]
 102 |2: clear value H2; simplify; intros; split; [assumption|3:reflexivity]
 103     rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption;
 104 |4: simplify; intros; split;
 105     [1: apply sum_bases_empty_nat_of_q_le_q;
 106     |2: apply sum_bases_empty_nat_of_q_le_q_one;
 107     |3: elim (nat_of_q q); [reflexivity] simplify; assumption]]
 108 qed.
 109
 110
 111 definition same_values ≝
 112   λl1,l2:q_f.
 113    ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)).
 114
 115 definition same_bases ≝
 116   λl1,l2:q_f.
 117     (∀i.\fst (nth (bars l1) ▭ i) = \fst (nth (bars l2) ▭ i)).
 118
 119 alias symbol "lt" = "Q less than".
 120 lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.
 121 intro; cases x; intros; [2:exists [apply r] reflexivity]
 122 cases (?:False);
 123 [ apply (q_lt_corefl ? H)|apply (q_neg_gt ? H)]
 124 qed.
 125
 126 notation < "\blacksquare" non associative with precedence 90 for @{'hide}.
 127 definition hide ≝ λT:Type.λx:T.x.
 128 interpretation "hide" 'hide = (hide _ _).
 129
 130 lemma sum_bases_ge_OQ:
 131   ∀l,n. OQ ≤ sum_bases l n.
 132 intro; elim l; simplify; intros;
 133 [1: elim n; [apply q_eq_to_le;reflexivity] simplify;
 134     apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ;
 135 |2: cases n; [apply q_eq_to_le;reflexivity] simplify;
 136     apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]]
 137 qed.
 138
 139 lemma sum_bases_O:
 140   ∀l:q_f.∀x.sum_bases (bars l) x ≤ OQ → x = O.
 141 intros; cases x in H; [intros; reflexivity] intro; cases (?:False);
 142 cases (q_le_cases ?? H);
 143 [1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %);
 144 |2: apply (q_lt_antisym ??? H1);] clear H H1; cases (bars l);
 145 simplify; apply q_lt_plus_trans;
 146 try apply q_pos_lt_OQ;
 147 try apply (sum_bases_ge_OQ []);
 148 apply (sum_bases_ge_OQ l1);
 149 qed.
 150