helm/software/matita/contribs/dama/dama/models/q_shift.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_bars.ma".
  16
  17 lemma initial_shift_same_values:
  18   ∀l1:q_f.∀init.init < start l1 →
  19    same_values l1
  20      (mk_q_f init (〈\fst (unpos (start l1 - init) ?),OQ〉:: bars l1)).
  21 [apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption]
  22 intros; generalize in ⊢ (? ? (? ? (? ? (? ? ? (? ? ? (? ? %)) ?) ?))); intro;
  23 cases (unpos (start l1-init) H1); intro input;
  24 simplify in ⊢ (? ? ? (? ? ? (? ? ? (? (? ? (? ? (? ? ? % ?) ?)) ?))));
  25 cases (value (mk_q_f init (〈w,OQ〉::bars l1)) input) (v1 Hv1);
  26 cases Hv1 (HV1 HV1 HV1 HV1); cases HV1 (Hi1 Hv11 Hv12); clear HV1 Hv1;
  27 [1: cut (input < start l1) as K;[2: apply (q_lt_trans ??? Hi1 H)]
  28     simplify in ⊢ (? ? ? (? ? ? %));
  29     rewrite > (value_OQ_l ?? K); simplify; symmetry; assumption;
  30 |2: cut (start l1 + sum_bases (bars l1) (len (bars l1)) ≤ input) as K;[2:
  31       simplify in Hi1; apply (q_le_trans ???? Hi1); rewrite > H2;
  32       rewrite > q_plus_sym in ⊢ (? ? (? ? %));
  33       rewrite > q_plus_assoc; rewrite > q_elim_minus;
  34       rewrite > q_plus_sym in ⊢ (? ? (? (? ? %) ?));
  35       rewrite > q_plus_assoc; rewrite < q_elim_minus;
  36       rewrite > q_plus_minus; rewrite > q_plus_sym in ⊢ (? ? (? % ?));
  37       rewrite > q_plus_OQ; apply q_eq_to_le; reflexivity;]
  38     simplify in ⊢ (? ? ? (? ? ? %));
  39     rewrite > (value_OQ_r ?? K); simplify; symmetry; assumption;
  40 |3: simplify in Hi1; destruct Hi1;
  41 |4: cut (start l1 ≤ input → \snd (\fst (value l1 input))=\snd v1) as solution;[2:
  42       intro H4; cases Hi1; clear Hi1; cases H3; clear H3;
  43       simplify in H5 H6 H8 H9 H7:(? ? (? % %)) ⊢ (? ? ? (? ? ? %));
  44       generalize in match (refl_eq ? (bars l1):bars l1 = bars l1);
  45       generalize in ⊢ (???% → ?); intro X; cases X; clear X; intro Hb;
  46       [1: rewrite > (value_OQ_e ?? Hb); rewrite > Hv12; rewrite > Hb in Hv11 ⊢ %;
  47           simplify in Hv11 ⊢ %; cases (\fst v1) in Hv11; [intros; reflexivity]
  48           cases n; [intros; reflexivity] intro X; cases (not_le_Sn_O ? (le_S_S_to_le ?? X));
  49       |2: cases (value_ok l1 input);
  50           [2: rewrite > Hb; intro W; destruct W;
  51           |3: assumption;
  52           |4: apply (q_lt_le_trans ??? H7); rewrite > H2;
  53                 rewrite > q_plus_sym; rewrite < q_plus_assoc;
  54                 rewrite > q_plus_sym; apply q_le_inj_plus_r;
  55                 apply q_le_minus; apply q_eq_to_le; reflexivity;
  56           |1: rewrite > Hv12; rewrite > Hb; clear Hv12; simplify;
  57               rewrite > H10; rewrite > Hb;
  58               cut (O < \fst v1);[2: cases (\fst v1) in H9; intros; [2: autobatch]
  59               cases (?:False); generalize in match H9;
  60                 rewrite > q_d_sym; rewrite > q_d_noabs; [2,4: assumption]
  61                 rewrite > H2; simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ;
  62                 repeat rewrite > q_elim_minus;
  63                 intro X; lapply (q_lt_canc_plus_r ??? X) as Y;
  64                 apply (q_lt_le_incompat ?? Y); assumption;]
  65               cases (\fst v1) in H8 H9 Hcut; [1:intros (_ _ X); cases (not_le_Sn_O ? X)]
  66               intros; clear H13; simplify;
  67               rewrite > (sum_bases_n_m n n1 (b::l)); [1,4: reflexivity] rewrite < Hb;
  68               [2: simplify in H8; apply (q_le_lt_trans ??? (q_le_plus_r ??? H8));
  69                     apply (q_le_lt_trans ???? H12); rewrite > H2;
  70                     rewrite > q_d_sym; rewrite > q_d_noabs; [2: assumption]
  71                     rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib;
  72                     rewrite > q_elim_opp; repeat rewrite > q_elim_minus;
  73                     rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init);
  74                     rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? (? % ?) ?);
  75                     rewrite > (q_plus_sym ? init); do 2 rewrite < q_elim_minus;
  76                     rewrite > q_plus_minus; rewrite > q_plus_OQ;
  77                     rewrite > q_d_sym; rewrite > q_d_noabs; [2:assumption]
  78                     apply q_eq_to_le; reflexivity;
  79               |*: apply (q_le_lt_trans ??? H11);
  80                   rewrite > q_d_sym; rewrite > q_d_noabs; [2:assumption;]
  81                   generalize in match H9; rewrite > q_d_sym; rewrite > q_d_noabs; [2: assumption]
  82                   rewrite > H2; intro X;
  83                   lapply (q_lt_inj_plus_r ?? (Qopp (start l1-init)) X) as Y; clear X;
  84                   rewrite < q_plus_assoc in Y; repeat rewrite < q_elim_minus in Y;
  85                   rewrite > q_plus_minus in Y; rewrite > q_plus_OQ in Y;
  86                   apply (q_le_lt_trans ???? Y);
  87                   rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib;
  88                   rewrite > q_elim_opp; repeat rewrite > q_elim_minus;
  89                   rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init);
  90                   rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? ? (? % ?));
  91                   rewrite > (q_plus_sym ? init); rewrite < (q_elim_minus init);
  92                   rewrite > q_plus_minus; rewrite > q_plus_OQ;
  93                   apply q_eq_to_le; reflexivity;]]]]]
  94     cases (q_cmp input (start l1));
  95       [2: simplify in ⊢ (? ? ? (? ? ? %)); rewrite > (value_OQ_l ?? H4);
  96         change with (OQ = \snd v1); rewrite > Hv12;
  97         cases H3; clear H3; simplify in H5; cases (\fst v1) in H5;[intros;reflexivity]
  98         simplify; rewrite > q_d_sym; rewrite > q_d_noabs; [2:cases Hi1; apply H5]
  99         rewrite > H2; do 2 rewrite > q_elim_minus;rewrite > q_plus_assoc;
 100         intro X; lapply (q_le_canc_plus_r ??? X) as Y; clear X;
 101         cases (?:False); apply (q_lt_le_incompat input (start l1)); try assumption;
 102         apply (q_le_S ???? Y); try assumption; apply sum_bases_ge_OQ;
 103       |1: apply solution; apply (q_eq_to_le ?? (sym_eq ??? H4));
 104       |3: apply solution; apply (q_lt_to_le ?? H4);]
 105 qed.