helm/software/matita/contribs/dama/dama/models/q_rebase.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_function.ma".
  16
  17 definition eject ≝
  18   λP.λp:∃x:(list bar) × (list bar).P x.match p with [ex_introT p _ ⇒ p].
  19 coercion eject.
  20 definition inject ≝ λP.λp:(list bar) × (list bar).λh:P p. ex_introT ? P p h.
  21 coercion inject with 0 1 nocomposites.
  22
  23 definition rebase: ∀l1,l2:q_f.∃p:q_f × q_f.rebase_spec l1 l2 p.
  24 intros 2 (f1 f2); cases f1 (b1 Hs1 Hb1 He1); cases f2 (b2 Hs2 Hb2 He2); clear f1 f2;
  25 alias symbol "leq" = "natural 'less or equal to'".
  26 alias symbol "minus" = "Q minus".
  27 letin aux ≝ (
  28 let rec aux (l1,l2:list bar) (n : nat) on n : (list bar) × (list bar) ≝
  29 match n with
  30 [ O ⇒ 〈[], []〉
  31 | S m ⇒
  32   match l1 with
  33   [ nil ⇒ 〈copy l2, l2〉
  34   | cons he1 tl1 ⇒
  35      match l2 with
  36      [ nil ⇒ 〈l1, copy l1〉
  37      | cons he2 tl2 ⇒
  38          let base1 ≝ \fst he1 in
  39          let base2 ≝ \fst he2 in
  40          let height1 ≝ \snd he1 in
  41          let height2 ≝ \snd he2 in
  42          match q_cmp base1 base2 with
  43          [ q_leq Hp1 ⇒
  44              match q_cmp base2 base1 with
  45              [ q_leq Hp2 ⇒
  46                  let rc ≝ aux tl1 tl2 m in
  47                  〈he1 :: \fst rc,he2 :: \snd rc〉
  48              | q_gt Hp ⇒
  49                  let rest ≝ base2 - base1 in
  50                  let rc ≝ aux tl1 (〈rest,height2〉 :: tl2) m in
  51                  〈〈base1,height1〉 :: \fst rc,〈base1,height2〉 :: \snd rc〉]
  52          | q_gt Hp ⇒
  53              let rest ≝ base1 - base2 in
  54              let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in
  55              〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉]]]]
  56 in aux : ∀l1,l2,m.∃z.\len l1 + \len l2 ≤ m → rebase_spec_aux l1 l2 z);
  57 [7: clearbody aux; cases (aux b1 b2 (\len b1 + \len b2)) (res Hres);
  58     exists; [split; constructor 1; [apply (\fst res)|5:apply (\snd res)]]
  59     [1,4: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); assumption;
  60     |2,5: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); lapply (H5 O) as K;
  61           clear H1 H2 H3 H4 H5 H6 H7 Hres aux; unfold nth_base;
  62           cases H in K He1 He2 Hb1 Hb2; simplify; intros; assumption;
  63     |3,6: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2);
  64           cases H in He1 He2; simplify; intros;
  65           [1,6,8,12: assumption;
  66           |2,7: rewrite > len_copy; generalize in match (\len ?); intro X;
  67                 cases X; [1,3: reflexivity] simplify;
  68                 [apply (copy_OQ ys n);|apply (copy_OQ xs n);]
  69           |3,4,5: rewrite < H8; assumption;
  70           |9,10,11: rewrite < H9; assumption]]
  71     split; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); unfold same_values; intros;
  72     [1: assumption
  73     |2,3: simplify in match (\snd 〈?,?〉); simplify in match (\fst 〈?,?〉);
  74         apply same_values_simpl_to_same_values; assumption]
  75 |3: cut (\fst b3 = \fst b) as E; [2: apply q_le_to_le_to_eq; assumption]
  76     clear H6 H5 H4 H3 He2 Hb2 Hs2 b2 He1 Hb1 Hs1 b1; cases (aux l2 l3 n1);
  77     clear aux; intro K; simplify in K; rewrite <plus_n_Sm in K;
  78     lapply le_S_S_to_le to K as W; lapply lt_to_le to W as R;
  79     simplify in match (? ≪w,H3≫); intros; cases (H3 R); clear H3 R W K;
  80       [2,4: apply (sorted_tail q2_lt);[apply b|3:apply b3]assumption;
  81       |3: cases l2 in H5; simplify; intros; try reflexivity; assumption;
  82       |5: cases l3 in H7; simplify; intros; try reflexivity; assumption;]
  83     constructor 1; simplify in match (\fst 〈?,?〉); simplify in match (\snd 〈?,?〉);
  84     [1: cases b in E H5 H7 H11 H14; cases b3; intros (E H5 H7 H11 H14); simplify in E;
  85         destruct E; constructor 3;
  86         [ cases H8 in H5 H7; intros; [1,6:reflexivity|3,4,5: assumption;]
  87           simplify; rewrite > H3; rewrite > len_copy; elim (\len ys); [reflexivity]
  88           symmetry; apply (copy_OQ ys n2);
  89         | cases H8 in H5 H7; simplify; intros; [2,6:reflexivity|3,4,5: assumption]
  90           simplify; rewrite > H5; rewrite > len_copy; elim (\len xs); [reflexivity]
  91           symmetry; apply (copy_OQ xs n2);]
  92     |2: apply (aux_preserves_sorting ? b3 ??? H8); assumption;
  93     |3: apply (aux_preserves_sorting2 ? b3 ??? H8); try assumption;
  94         try reflexivity; cases (inversion_sorted ?? H4);[2:rewrite >H3; apply (sorted_one q2_lt);]
  95         cases l2 in H3 H4; intros; [apply (sorted_one q2_lt)]
  96         apply (sorted_cons q2_lt);[2:apply (sorted_tail q2_lt ?? H3);] whd;
  97         rewrite > E; assumption;
  98     |4: apply I
  99     |5: apply I
 100     |6: intro; elim i; intros; simplify; solve [symmetry;assumption|apply H13]
 101     |7: unfold; intros; cases H8 in H13 H14 H15 Hi1 Hi2 H17 H18 H3 H16; intros;
 102         [1: simplify in match (\fst 〈?,?〉) in H16 H17 H20 H21 H22 H23 ⊢ %;
 103             cases (q_cmp (Qpos input) b1);
 104             [1: do 2 (rewrite > value_head; [id|assumption]); reflexivity;
 105             |2: do 2 (rewrite > value_tail;[id|assumption]); apply H16;]
 106         |2: simplify in match (\fst 〈?,?〉) in H16 H17 H20 H21 H22 H23 ⊢ %;
 107             cases (q_cmp (Qpos input) b1);
 108             [1: rewrite > value_head; [2:assumption]
 109             |2: rewrite > value_tail;[2:assumption]
 110                 simplify in H15;
 111             ]
 112     |8:
 113
 114
 115 include "Q/q/qtimes.ma".
 116
 117 let rec area (l:list bar) on l ≝
 118   match l with
 119   [ nil ⇒ OQ
 120   | cons he tl ⇒ area tl + Qpos (\fst he) * ⅆ[OQ,\snd he]].
 121
 122 alias symbol "pi1" = "exT \fst".
 123 alias symbol "minus" = "Q minus".
 124 alias symbol "exists" = "CProp exists".
 125 definition minus_spec_bar ≝
 126  λf,g,h:list bar.
 127    same_bases f g → len f = len g →
 128      ∀s,i:ℚ. \snd (\fst (value (mk_q_f s h) i)) =
 129        \snd (\fst (value (mk_q_f s f) i)) - \snd (\fst (value (mk_q_f s g) i)).
 130
 131 definition minus_spec ≝
 132  λf,g:q_f.
 133    ∃h:q_f.
 134      ∀i:ℚ. \snd (\fst (value h i)) =
 135        \snd (\fst (value f i)) - \snd (\fst (value g i)).
 136
 137 definition eject_bar : ∀P:list bar → CProp.(∃l:list bar.P l) → list bar ≝
 138  λP.λp.match p with [ex_introT x _ ⇒ x].
 139 definition inject_bar ≝ ex_introT (list bar).
 140
 141 coercion inject_bar with 0 1 nocomposites.
 142 coercion eject_bar with 0 0 nocomposites.
 143
 144 lemma minus_q_f : ∀f,g. minus_spec f g.
 145 intros;
 146 letin aux ≝ (
 147   let rec aux (l1, l2 : list bar) on l1 ≝
 148     match l1 with
 149     [ nil ⇒ []
 150     | cons he1 tl1 ⇒
 151         match l2 with
 152         [ nil ⇒ []
 153         | cons he2 tl2 ⇒ 〈\fst he1, \snd he1 - \snd he2〉 :: aux tl1 tl2]]
 154   in aux : ∀l1,l2 : list bar.∃h.minus_spec_bar l1 l2 h);
 155 [2: intros 4; simplify in H3; destruct H3;
 156 |3: intros 4; simplify in H3; cases l1 in H2; [2: intro X; simplify in X; destruct X]
 157     intros; rewrite > (value_OQ_e (mk_q_f s []) i); [2: reflexivity]
 158     rewrite > q_elim_minus; rewrite > q_plus_OQ; reflexivity;
 159 |1: cases (aux l2 l3); unfold in H2; intros 4;
 160     simplify in ⊢ (? ? (? ? ? (? ? ? (? % ?))) ?);
 161     cases (q_cmp i (s + Qpos (\fst b)));
 162
 163
 164
 165 definition excess ≝
 166   λf,g.∃i.\snd (\fst (value f i)) < \snd (\fst (value g i)).
 167