1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "models/q_bars.ma".
17 lemma initial_shift_same_values:
18 ∀l1:q_f.∀init.init < start 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;
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);]