helm/software/matita/contribs/dama/dama/models/q_function.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_bars.ma".
  17
  18 lemma key:
  19   ∀n,m,l.
  20     sum_bases l n < sum_bases l (S m) →
  21     sum_bases l m < sum_bases l (S n) →
  22     n = m.
  23 intros 2; apply (nat_elim2 ???? n m);
  24 [1: intro X; cases X; intros; [reflexivity] cases (?:False);
  25     cases l in H H1; simplify; intros;
  26     apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1));
  27     apply (q_lt_canc_plus_r ??? H1);
  28 |2: intros 2; cases l; simplify; intros; cases (?:False);
  29     apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1));
  30     apply (q_lt_canc_plus_r ??? H); (* magia ... *)
  31 |3: intros 4; cases l; simplify; intros;
  32     [1: rewrite > (H []); [reflexivity]
  33         apply (q_lt_canc_plus_r ??(Qpos one)); assumption;
  34     |2: rewrite > (H l1); [reflexivity]
  35         apply (q_lt_canc_plus_r ??(Qpos (\fst b))); assumption;]]
  36 qed.
  37
  38 lemma initial_shift_same_values:
  39   ∀l1:q_f.∀init.init < start l1 →
  40    same_values l1
  41      (mk_q_f init (〈\fst (unpos (start l1 - init) ?),OQ〉:: bars l1)).
  42 [apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption]
  43 intros; generalize in ⊢ (? ? (? ? (? ? (? ? ? (? ? ? (? ? %)) ?) ?))); intro;
  44 cases (unpos (start l1-init) H1); intro input;
  45 simplify in ⊢ (? ? ? (? ? ? (? ? ? (? (? ? (? ? (? ? ? % ?) ?)) ?))));
  46 cases (value (mk_q_f init (〈w,OQ〉::bars l1)) input) (v1 Hv1);
  47 cases Hv1 (HV1 HV1 HV1 HV1); cases HV1 (Hi1 Hv11 Hv12); clear HV1 Hv1;
  48 [1: cut (input < start l1) as K;[2: apply (q_lt_trans ??? Hi1 H)]
  49     rewrite > (value_OQ_l ?? K); simplify; symmetry; assumption;
  50 |2: cut (start l1 + sum_bases (bars l1) (len (bars l1)) ≤ input) as K;[2:
  51       simplify in Hi1; apply (q_le_trans ???? Hi1); rewrite > H2;
  52       rewrite > q_plus_sym in ⊢ (? ? (? ? %));
  53       rewrite > q_plus_assoc; rewrite > q_elim_minus;
  54       rewrite > q_plus_sym in ⊢ (? ? (? (? ? %) ?));
  55       rewrite > q_plus_assoc; rewrite < q_elim_minus;
  56       rewrite > q_plus_minus; rewrite > q_plus_sym in ⊢ (? ? (? % ?));
  57       rewrite > q_plus_OQ; apply q_eq_to_le; reflexivity;]
  58     rewrite > (value_OQ_r ?? K); simplify; symmetry; assumption;
  59 |3: simplify in Hi1; destruct Hi1;
  60 |4: cases (q_cmp input (start l1));
  61     [2: rewrite > (value_OQ_l ?? H4);
  62         change with (OQ = \snd v1); rewrite > Hv12;
  63         cases H3; clear H3; simplify in H5; cases (\fst v1) in H5;[intros;reflexivity]
  64         simplify; rewrite > q_d_sym; rewrite > q_d_noabs; [2:cases Hi1; apply H5]
  65         rewrite > H2; do 2 rewrite > q_elim_minus;rewrite > q_plus_assoc;
  66         intro X; lapply (q_le_canc_plus_r ??? X) as Y; clear X;
  67         (* OK *)
  68     |1,3: cases Hi1; clear Hi1; cases H3; clear H3;
  69         simplify in H5 H6 H8 H9 H7:(? ? (? % %)) ⊢ (? ? ? (? ? ? %));
  70         generalize in match (refl_eq ? (bars l1):bars l1 = bars l1);
  71         generalize in ⊢ (???% → ?); intro X; cases X; clear X; intro Hb;
  72         [1,3: rewrite > (value_OQ_e ?? Hb); rewrite > Hv12; rewrite > Hb in Hv11 ⊢ %;
  73             simplify in Hv11 ⊢ %; cases (\fst v1) in Hv11; [1,3:intros; reflexivity]
  74             cases n; [1,3: intros; reflexivity] intro X; cases (not_le_Sn_O ? (le_S_S_to_le ?? X));
  75         |2,4: cases (value_ok l1 input);
  76             [1,5: rewrite > Hv12; rewrite > Hb; clear Hv12; simplify;
  77                 rewrite > H10; rewrite > Hb;
  78                 cut (O < \fst v1);[2,4: cases (\fst v1) in H9; intros; [2,4: autobatch]
  79                 cases (?:False); generalize in match H9;
  80                   rewrite > q_d_sym; rewrite > q_d_noabs; [2,4: assumption]
  81                   rewrite > H2; simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ;
  82                   repeat rewrite > q_elim_minus;
  83                   intro X; lapply (q_lt_canc_plus_r ??? X) as Y;
  84                   apply (q_lt_le_incompat ?? Y);
  85                   [apply q_eq_to_le;symmetry|apply q_lt_to_le] assumption;]
  86                 cases (\fst v1) in H8 H9 Hcut; [1,3:intros (_ _ X); cases (not_le_Sn_O ? X)]
  87                 intros; clear H13; simplify;
  88                 rewrite > (key n n1 (b::l)); [1,4: reflexivity] rewrite < Hb;
  89                 [2,4: simplify in H8; apply (q_le_lt_trans ??? (q_le_plus_r ??? H8));
  90                       apply (q_le_lt_trans ???? H12); rewrite > H2;
  91                       rewrite > q_d_sym; rewrite > q_d_noabs; [2,4: assumption]
  92                       rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib;
  93                       rewrite > q_elim_opp; repeat rewrite > q_elim_minus;
  94                       rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init);
  95                       rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? (? % ?) ?);
  96                       rewrite > (q_plus_sym ? init); do 2 rewrite < q_elim_minus;
  97                       rewrite > q_plus_minus; rewrite > q_plus_OQ;
  98                       rewrite > q_d_sym; rewrite > q_d_noabs;
  99                         [2,4: [apply q_eq_to_le; symmetry|apply q_lt_to_le] assumption]
 100                       apply q_eq_to_le; reflexivity;
 101                 |*: apply (q_le_lt_trans ??? H11);
 102                     rewrite > q_d_sym; rewrite > q_d_noabs;
 103                       [2,4: [apply q_eq_to_le; symmetry|apply q_lt_to_le] assumption]
 104                     generalize in match H9; rewrite > q_d_sym; rewrite > q_d_noabs;
 105                       [2,4: assumption]
 106                     rewrite > H2; intro X;
 107                     lapply (q_lt_inj_plus_r ?? (Qopp (start l1-init)) X) as Y; clear X;
 108                     rewrite < q_plus_assoc in Y; repeat rewrite < q_elim_minus in Y;
 109                     rewrite > q_plus_minus in Y; rewrite > q_plus_OQ in Y;
 110                     apply (q_le_lt_trans ???? Y);
 111                     rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib;
 112                     rewrite > q_elim_opp; repeat rewrite > q_elim_minus;
 113                     rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init);
 114                     rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? ? (? % ?));
 115                     rewrite > (q_plus_sym ? init); rewrite < (q_elim_minus init);
 116                     rewrite > q_plus_minus; rewrite > q_plus_OQ;
 117                     apply q_eq_to_le; reflexivity;]
 118             |2,6: rewrite > Hb; intro W; destruct W;
 119             |3,7: [apply q_eq_to_le;symmetry|apply q_lt_to_le] assumption;
 120             |4,8: apply (q_lt_le_trans ??? H7); rewrite > H2;
 121                   rewrite > q_plus_sym; rewrite < q_plus_assoc;
 122                   rewrite > q_plus_sym; apply q_le_inj_plus_r;
 123                   apply q_le_minus; apply q_eq_to_le; reflexivity;]]]
 124 qed.
 125
 126
 127
 128 alias symbol "pi2" = "pair pi2".
 129 alias symbol "pi1" = "pair pi1".
 130 definition rebase_spec ≝
 131  ∀l1,l2:q_f.∃p:q_f × q_f.
 132    And4
 133     (*len (bars (\fst p)) = len (bars (\snd p))*)
 134     (start (\fst p) = start (\snd p))
 135     (same_bases (\fst p) (\snd p))
 136     (same_values l1 (\fst p))
 137     (same_values l2 (\snd p)).
 138
 139 definition rebase_spec_simpl ≝
 140  λstart.λl1,l2:list bar.λp:(list bar) × (list bar).
 141    And3
 142     (same_bases (mk_q_f start (\fst p)) (mk_q_f start (\snd p)))
 143     (same_values (mk_q_f start l1) (mk_q_f start (\fst p)))
 144     (same_values (mk_q_f start l2) (mk_q_f start (\snd p))).
 145
 146 (* a local letin makes russell fail *)
 147 definition cb0h : list bar → list bar ≝
 148   λl.mk_list (λi.〈\fst (nth l ▭ i),OQ〉) (len l).
 149
 150 definition eject ≝
 151   λP.λp:∃x:(list bar) × (list bar).P x.match p with [ex_introT p _ ⇒ p].
 152 coercion eject.
 153 definition inject ≝ λP.λp:(list bar) × (list bar).λh:P p. ex_introT ? P p h.
 154 coercion inject with 0 1 nocomposites.
 155
 156 definition rebase: rebase_spec.
 157 intros 2 (f1 f2); cases f1 (s1 l1); cases f2 (s2 l2); clear f1 f2;
 158 letin spec ≝ (
 159   λs.λl1,l2.λm.λz.len l1 + len l2 < m → rebase_spec_simpl s l1 l2 z);
 160 alias symbol "pi1" (instance 34) = "exT \fst".
 161 alias symbol "pi1" (instance 21) = "exT \fst".
 162 letin aux ≝ (
 163 let rec aux (l1,l2:list bar) (n:nat) on n : (list bar) × (list bar) ≝
 164 match n with
 165 [ O ⇒ 〈 nil ? , nil ? 〉
 166 | S m ⇒
 167   match l1 with
 168   [ nil ⇒ 〈cb0h l2, l2〉
 169   | cons he1 tl1 ⇒
 170      match l2 with
 171      [ nil ⇒ 〈l1, cb0h l1〉
 172      | cons he2 tl2 ⇒
 173          let base1 ≝ Qpos (\fst he1) in
 174          let base2 ≝ Qpos (\fst he2) in
 175          let height1 ≝ (\snd he1) in
 176          let height2 ≝ (\snd he2) in
 177          match q_cmp base1 base2 with
 178          [ q_eq _ ⇒
 179              let rc ≝ aux tl1 tl2 m in
 180              〈he1 :: \fst rc,he2 :: \snd rc〉
 181          | q_lt Hp ⇒
 182              let rest ≝ base2 - base1 in
 183              let rc ≝ aux tl1 (〈\fst (unpos rest ?),height2〉 :: tl2) m in
 184              〈〈\fst he1,height1〉 :: \fst rc,〈\fst he1,height2〉 :: \snd rc〉
 185          | q_gt Hp ⇒
 186              let rest ≝ base1 - base2 in
 187              let rc ≝ aux (〈\fst (unpos rest ?),height1〉 :: tl1) tl2 m in
 188              〈〈\fst he2,height1〉 :: \fst rc,〈\fst he2,height2〉 :: \snd rc〉
 189 ]]]]
 190 in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec;
 191 [9: clearbody aux; unfold spec in aux; clear spec;
 192     cases (q_cmp s1 s2);
 193     [1: cases (aux l1 l2 (S (len l1 + len l2)));
 194         cases (H1 s1 (le_n ?)); clear H1;
 195         exists [apply 〈mk_q_f s1 (\fst w), mk_q_f s2 (\snd w)〉] split;
 196         [1,2: assumption;
 197         |3: intro; apply (H3 input);
 198         |4: intro; rewrite > H in H4;
 199             rewrite > (H4 input); reflexivity;]
 200     |2: letin l2' ≝ (〈\fst (unpos (s2-s1) ?),OQ〉::l2);[
 201           apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ;
 202           assumption]
 203         cases (aux l1 l2' (S (len l1 + len l2')));
 204         cases (H1 s1 (le_n ?)); clear H1 aux;
 205         exists [apply 〈mk_q_f s1 (\fst w), mk_q_f s1 (\snd w)〉] split;
 206         [1: reflexivity
 207         |2: assumption;
 208         |3: assumption;
 209         |4: intro; rewrite < (H4 input); clear H3 H4 H2 w;
 210             cases (value (mk_q_f s1 l2') input);
 211             cases (q_cmp input (start (mk_q_f s1 l2'))) in H1;
 212             whd in ⊢ (% → ?);
 213             [1: intros; cases H2; clear H2; whd in ⊢ (??? %);
 214                 cases (value (mk_q_f s2 l2) input);
 215                 cases (q_cmp input (start (mk_q_f s2 l2))) in H2;
 216                 whd in ⊢ (% → ?);
 217                 [1: intros; cases H6; clear H6; change with (w1 = w);
 218
 219             (* TODO *) ]]
 220 |1,2: unfold rest; apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ;
 221       assumption;
 222 |3:(* TODO *)
 223 |4:(* TODO *)
 224 |5:(* TODO *)
 225 |6:(* TODO *)
 226 |7:(* TODO *)
 227 |8: intros; cases (?:False); apply (not_le_Sn_O ? H1);]
 228 qed.