X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_shift.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_shift.ma;h=e69de29bb2d1d6434b8b29ae775ad8c2e48c5391;hb=8d367045e504f594c280d2c87f906695ef9671ee;hp=a630666595aaee63616e187c98b7bedb54917980;hpb=fa3ef782b1336310a78868e7dfc900fa988ee2ab;p=helm.git diff --git a/helm/software/matita/contribs/dama/dama/models/q_shift.ma b/helm/software/matita/contribs/dama/dama/models/q_shift.ma index a63066659..e69de29bb 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_shift.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_shift.ma @@ -1,106 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "models/q_bars.ma". - -lemma initial_shift_same_values: - ∀l1:q_f.∀init.init < start l1 → - same_values l1 - (mk_q_f init (〈\fst (unpos (start l1 - init) ?),OQ〉:: bars l1)). -[apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption] -intros; generalize in ⊢ (? ? (? ? (? ? (? ? ? (? ? ? (? ? %)) ?) ?))); intro; -cases (unpos (start l1-init) H1); intro input; -simplify in ⊢ (? ? ? (? ? ? (? ? ? (? (? ? (? ? (? ? ? % ?) ?)) ?)))); -cases (value (mk_q_f init (〈w,OQ〉::bars l1)) input) (v1 Hv1); -cases Hv1 (HV1 HV1 HV1 HV1); cases HV1 (Hi1 Hv11 Hv12); clear HV1 Hv1; -[1: cut (input < start l1) as K;[2: apply (q_lt_trans ??? Hi1 H)] - simplify in ⊢ (? ? ? (? ? ? %)); - rewrite > (value_OQ_l ?? K); simplify; symmetry; assumption; -|2: cut (start l1 + sum_bases (bars l1) (len (bars l1)) ≤ input) as K;[2: - simplify in Hi1; apply (q_le_trans ???? Hi1); rewrite > H2; - rewrite > q_plus_sym in ⊢ (? ? (? ? %)); - rewrite > q_plus_assoc; rewrite > q_elim_minus; - rewrite > q_plus_sym in ⊢ (? ? (? (? ? %) ?)); - rewrite > q_plus_assoc; rewrite < q_elim_minus; - rewrite > q_plus_minus; rewrite > q_plus_sym in ⊢ (? ? (? % ?)); - rewrite > q_plus_OQ; apply q_eq_to_le; reflexivity;] - simplify in ⊢ (? ? ? (? ? ? %)); - rewrite > (value_OQ_r ?? K); simplify; symmetry; assumption; -|3: simplify in Hi1; destruct Hi1; -|4: cut (start l1 ≤ input → \snd (\fst (value l1 input))=\snd v1) as solution;[2: - intro H4; cases Hi1; clear Hi1; cases H3; clear H3; - simplify in H5 H6 H8 H9 H7:(? ? (? % %)) ⊢ (? ? ? (? ? ? %)); - generalize in match (refl_eq ? (bars l1):bars l1 = bars l1); - generalize in ⊢ (???% → ?); intro X; cases X; clear X; intro Hb; - [1: rewrite > (value_OQ_e ?? Hb); rewrite > Hv12; rewrite > Hb in Hv11 ⊢ %; - simplify in Hv11 ⊢ %; cases (\fst v1) in Hv11; [intros; reflexivity] - cases n; [intros; reflexivity] intro X; cases (not_le_Sn_O ? (le_S_S_to_le ?? X)); - |2: cases (value_ok l1 input); - [2: rewrite > Hb; intro W; destruct W; - |3: assumption; - |4: apply (q_lt_le_trans ??? H7); rewrite > H2; - rewrite > q_plus_sym; rewrite < q_plus_assoc; - rewrite > q_plus_sym; apply q_le_inj_plus_r; - apply q_le_minus; apply q_eq_to_le; reflexivity; - |1: rewrite > Hv12; rewrite > Hb; clear Hv12; simplify; - rewrite > H10; rewrite > Hb; - cut (O < \fst v1);[2: cases (\fst v1) in H9; intros; [2: autobatch] - cases (?:False); generalize in match H9; - rewrite > q_d_sym; rewrite > q_d_noabs; [2,4: assumption] - rewrite > H2; simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ; - repeat rewrite > q_elim_minus; - intro X; lapply (q_lt_canc_plus_r ??? X) as Y; - apply (q_lt_le_incompat ?? Y); assumption;] - cases (\fst v1) in H8 H9 Hcut; [1:intros (_ _ X); cases (not_le_Sn_O ? X)] - intros; clear H13; simplify; - rewrite > (sum_bases_n_m n n1 (b::l)); [1,4: reflexivity] rewrite < Hb; - [2: simplify in H8; apply (q_le_lt_trans ??? (q_le_plus_r ??? H8)); - apply (q_le_lt_trans ???? H12); rewrite > H2; - rewrite > q_d_sym; rewrite > q_d_noabs; [2: assumption] - rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib; - rewrite > q_elim_opp; repeat rewrite > q_elim_minus; - rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init); - rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? (? % ?) ?); - rewrite > (q_plus_sym ? init); do 2 rewrite < q_elim_minus; - rewrite > q_plus_minus; rewrite > q_plus_OQ; - rewrite > q_d_sym; rewrite > q_d_noabs; [2:assumption] - apply q_eq_to_le; reflexivity; - |*: apply (q_le_lt_trans ??? H11); - rewrite > q_d_sym; rewrite > q_d_noabs; [2:assumption;] - generalize in match H9; rewrite > q_d_sym; rewrite > q_d_noabs; [2: assumption] - rewrite > H2; intro X; - lapply (q_lt_inj_plus_r ?? (Qopp (start l1-init)) X) as Y; clear X; - rewrite < q_plus_assoc in Y; repeat rewrite < q_elim_minus in Y; - rewrite > q_plus_minus in Y; rewrite > q_plus_OQ in Y; - apply (q_le_lt_trans ???? Y); - rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib; - rewrite > q_elim_opp; repeat rewrite > q_elim_minus; - rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init); - rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? ? (? % ?)); - rewrite > (q_plus_sym ? init); rewrite < (q_elim_minus init); - rewrite > q_plus_minus; rewrite > q_plus_OQ; - apply q_eq_to_le; reflexivity;]]]]] - cases (q_cmp input (start l1)); - [2: simplify in ⊢ (? ? ? (? ? ? %)); rewrite > (value_OQ_l ?? H4); - change with (OQ = \snd v1); rewrite > Hv12; - cases H3; clear H3; simplify in H5; cases (\fst v1) in H5;[intros;reflexivity] - simplify; rewrite > q_d_sym; rewrite > q_d_noabs; [2:cases Hi1; apply H5] - rewrite > H2; do 2 rewrite > q_elim_minus;rewrite > q_plus_assoc; - intro X; lapply (q_le_canc_plus_r ??? X) as Y; clear X; - cases (?:False); apply (q_lt_le_incompat input (start l1)); try assumption; - apply (q_le_S ???? Y); try assumption; apply sum_bases_ge_OQ; - |1: apply solution; apply (q_eq_to_le ?? (sym_eq ??? H4)); - |3: apply solution; apply (q_lt_to_le ?? H4);] -qed. -